{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory.Sub where

import Data.Kind (Type)
import Prelude (($))

import Proarrow.Core (CAT, UN, Is, CategoryOf (..), Promonad (..), Profunctor (..), dimapDefault)
import Proarrow.Category.Bicategory (Bicategory (..))


class IsOb (tag :: Type) a

type SUBCAT :: forall k. Type -> CAT k -> CAT k
type data SUBCAT tag kk i j = SUB (kk i j)
type instance UN SUB (SUB p) = p

type Sub :: CAT (SUBCAT ob kk i j)
data Sub a b where
  Sub :: (IsOb tag a, IsOb tag b) => a ~> b -> Sub (SUB a :: SUBCAT tag kk i j) (SUB b)

instance Profunctor ((~>) :: CAT (kk i j)) => Profunctor (Sub :: CAT (SUBCAT tag kk i j)) where
  dimap :: forall (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j)
       (b :: SUBCAT tag kk i j) (d :: SUBCAT tag kk i j).
(c ~> a) -> (b ~> d) -> Sub a b -> Sub c d
dimap = (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d
Sub c a -> Sub b d -> Sub a b -> Sub c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Sub a ~> b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: kk i j) (b :: kk i j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
p

instance Promonad ((~>) :: CAT (kk i j)) => Promonad (Sub :: CAT (SUBCAT tag kk i j)) where
  id :: forall (a :: SUBCAT tag kk i j). Ob a => Sub a a
id = (UN SUB a ~> UN SUB a) -> Sub (SUB (UN SUB a)) (SUB (UN SUB a))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub UN SUB a ~> UN SUB a
forall (a :: kk i j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Sub a ~> b
f . :: forall (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk i j)
       (a :: SUBCAT tag kk i j).
Sub b c -> Sub a b -> Sub a c
. Sub a ~> b
g = (a ~> b) -> Sub (SUB a) (SUB b)
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (a ~> b
f (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: kk i j) (c :: kk i j) (a :: kk i j).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
a ~> b
g)

-- | The subcategory with objects with instances of the given constraint `IsOb tag`.
instance CategoryOf (kk i j) => CategoryOf (SUBCAT tag kk i j) where
  type (~>) = Sub
  type Ob (a :: SUBCAT tag kk i j) = (Is SUB a, Ob (UN SUB a), IsOb tag (UN SUB a))

class (IsOb tag (a `O` b)) => IsObO tag kk i j k (a :: kk i j) (b :: kk j k)
instance (IsOb tag (a `O` b)) => IsObO tag kk i j k (a :: kk i j) (b :: kk j k)

class (IsOb tag (I :: kk i i)) => IsObI tag kk i
instance (IsOb tag (I :: kk i i)) => IsObI tag kk i

instance (Bicategory kk, forall i. Ob0 kk i => IsObI tag kk i, forall i j k (a :: kk i j) (b :: kk j k). (IsOb tag a, IsOb tag b) => IsObO tag kk i j k a b)
    => Bicategory (SUBCAT tag kk) where
  type Ob0 (SUBCAT tag kk) k = Ob0 kk k
  type I = SUB I
  type p `O` q = SUB (UN SUB p `O` UN SUB q)
  Sub a ~> b
m o :: forall {k1 :: k} (i :: k) (j :: k) (a :: SUBCAT tag kk i j)
       (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk j k1)
       (d :: SUBCAT tag kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Sub a ~> b
n = (O a a ~> O b b) -> Sub (SUB (O a a)) (SUB (O b b))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub ((O a a ~> O b b) -> Sub (SUB (O a a)) (SUB (O b b)))
-> (O a a ~> O b b) -> Sub (SUB (O a a)) (SUB (O b b))
forall a b. (a -> b) -> a -> b
$ a ~> b
m (a ~> b) -> (a ~> b) -> O a a ~> O b b
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a ~> b
n
  (Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: k) (j :: k) (ps :: SUBCAT tag kk i j)
       (qs :: SUBCAT tag kk i j) r.
((Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Sub a ~> b
f = r
(Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r
(Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r
r ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r) -> (a ~> b) -> r
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall k (kk :: CAT k) (i :: k) (j :: k) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
f
  leftUnitor :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j).
Obj a -> O I a ~> a
leftUnitor (Sub a ~> b
p) = (O I b ~> b) -> Sub (SUB (O I b)) (SUB b)
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> O I b ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O I a ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O I a ~> a
leftUnitor a ~> b
Obj b
p) ((Ob0 kk i, Ob0 kk j, Ob b, Ob b) => Sub (SUB (O I b)) (SUB b))
-> Obj b -> Sub (SUB (O I b)) (SUB b)
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall k (kk :: CAT k) (i :: k) (j :: k) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
Obj b
p
  leftUnitorInv :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j).
Obj a -> a ~> O I a
leftUnitorInv (Sub a ~> b
p) = (b ~> O I b) -> Sub (SUB b) (SUB (O I b))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> b ~> O I b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O I a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O I a
leftUnitorInv a ~> b
Obj b
p) ((Ob0 kk i, Ob0 kk j, Ob b, Ob b) => Sub (SUB b) (SUB (O I b)))
-> Obj b -> Sub (SUB b) (SUB (O I b))
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall k (kk :: CAT k) (i :: k) (j :: k) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
Obj b
p
  rightUnitor :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j).
Obj a -> O a I ~> a
rightUnitor (Sub a ~> b
p) = (O b I ~> b) -> Sub (SUB (O b I)) (SUB b)
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> O b I ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O a I ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O a I ~> a
rightUnitor a ~> b
Obj b
p) ((Ob0 kk i, Ob0 kk j, Ob b, Ob b) => Sub (SUB (O b I)) (SUB b))
-> Obj b -> Sub (SUB (O b I)) (SUB b)
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall k (kk :: CAT k) (i :: k) (j :: k) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
Obj b
p
  rightUnitorInv :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j).
Obj a -> a ~> O a I
rightUnitorInv (Sub a ~> b
p) = (b ~> O b I) -> Sub (SUB b) (SUB (O b I))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> b ~> O b I
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O a I
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O a I
rightUnitorInv a ~> b
Obj b
p) ((Ob0 kk i, Ob0 kk j, Ob b, Ob b) => Sub (SUB b) (SUB (O b I)))
-> Obj b -> Sub (SUB b) (SUB (O b I))
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall k (kk :: CAT k) (i :: k) (j :: k) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
Obj b
p
  associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: SUBCAT tag kk i j2) (b :: SUBCAT tag kk j2 j1)
       (c :: SUBCAT tag kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Sub a ~> b
p) (Sub a ~> b
q) (Sub a ~> b
r) = (O (O b b) b ~> O b (O b b))
-> Sub (SUB (O (O b b) b)) (SUB (O b (O b b)))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> Obj b -> Obj b -> O (O b b) b ~> O b (O b b)
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator a ~> b
Obj b
p a ~> b
Obj b
q a ~> b
Obj b
r)
  associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: SUBCAT tag kk i j2) (b :: SUBCAT tag kk j2 j1)
       (c :: SUBCAT tag kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Sub a ~> b
p) (Sub a ~> b
q) (Sub a ~> b
r) = (O b (O b b) ~> O (O b b) b)
-> Sub (SUB (O b (O b b))) (SUB (O (O b b) b))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> Obj b -> Obj b -> O b (O b b) ~> O (O b b) b
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv a ~> b
Obj b
p a ~> b
Obj b
q a ~> b
Obj b
r)