module Proarrow.Category.Bicategory.Hom where

import Proarrow.Category.Bicategory (Bicategory (..), (==), (||))
import Proarrow.Category.Bicategory.Co (COK (..), Co (..))
import Proarrow.Category.Bicategory.Prof (LaxProfunctor (..))
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj, type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Identity (Id (..))

newtype HK kk i j = HomK {forall {k} {k} (kk :: k -> k -> Type) (i :: k) (j :: k).
HK kk i j -> kk i j
unHomK :: kk i j}
type instance UN HomK (HomK k) = k

type HomW :: CAT (HK kk i j)
data HomW a b where
  HomW :: a ~> b -> HomW (HomK a) (HomK b)
instance (Profunctor ((~>) :: CAT (kk i j))) => Profunctor (HomW :: CAT (HK kk i j)) where
  dimap :: forall (c :: HK kk i j) (a :: HK kk i j) (b :: HK kk i j)
       (d :: HK kk i j).
(c ~> a) -> (b ~> d) -> HomW a b -> HomW c d
dimap = (c ~> a) -> (b ~> d) -> HomW a b -> HomW c d
HomW c a -> HomW b d -> HomW a b -> HomW 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 :: HK kk i j) (b :: HK kk i j) r.
((Ob a, Ob b) => r) -> HomW a b -> r
\\ HomW a ~> b
f = 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
f
instance (Promonad ((~>) :: CAT (kk i j))) => Promonad (HomW :: CAT (HK kk i j)) where
  id :: forall (a :: HK kk i j). Ob a => HomW a a
id = (UN 'HomK a ~> UN 'HomK a)
-> HomW ('HomK (UN 'HomK a)) ('HomK (UN 'HomK a))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> HomW ('HomK a) ('HomK b)
HomW UN 'HomK a ~> UN 'HomK 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
  HomW a ~> b
f . :: forall (b :: HK kk i j) (c :: HK kk i j) (a :: HK kk i j).
HomW b c -> HomW a b -> HomW a c
. HomW a ~> b
g = (a ~> b) -> HomW ('HomK a) ('HomK b)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> HomW ('HomK a) ('HomK b)
HomW (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)
instance (CategoryOf (kk i j)) => CategoryOf (HK kk i j) where
  type (~>) = HomW
  type Ob k = (Is HomK k, Ob (UN HomK k))

instance
  (Bicategory kk, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => Profunctor (P kk kk (HK kk) (s :: COK kk h i) (t :: kk j k))
  where
  dimap :: forall (c :: HK kk i k) (a :: HK kk i k) (b :: HK kk h j)
       (d :: HK kk h j).
(c ~> a)
-> (b ~> d) -> P kk kk (HK kk) s t a b -> P kk kk (HK kk) s t c d
dimap (HomW a ~> b
f) (HomW a ~> b
g) (Hom O a s ~> O t b
n) = (O a (UN 'CO s) ~> O t b)
-> P kk kk (HK kk) ('CO (UN 'CO s)) t ('HomK a) ('HomK b)
forall {s} {h :: s} {i :: s} {j :: s} {k :: s}
       {kk :: s -> s -> Type} (a :: kk i k) (b :: kk h j) (s :: kk h i)
       (t :: kk j k).
(Ob a, Ob b, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(O a s ~> O t b) -> P kk kk (HK kk) ('CO s) t ('HomK a) ('HomK b)
Hom ((forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t Obj t -> (a ~> b) -> O t a ~> O t b
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a ~> b
g) (O t a ~> O t b)
-> (O a (UN 'CO s) ~> O t a) -> O a (UN 'CO s) ~> O t b
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(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
. O b (UN 'CO s) ~> O t a
O a s ~> O t b
n (O b (UN 'CO s) ~> O t a)
-> (O a (UN 'CO s) ~> O b (UN 'CO s)) -> O a (UN 'CO s) ~> O t a
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(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 ~> b
f (a ~> b)
-> (UN 'CO s ~> UN 'CO s) -> O a (UN 'CO s) ~> O b (UN 'CO s)
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk h i). (CategoryOf (kk h i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO s))) ((Ob0 kk i, Ob0 kk k, Ob a, Ob b) => P kk kk (HK kk) s t c d)
-> (a ~> b) -> P kk kk (HK kk) s t c d
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 {s} (kk :: CAT s) (i :: s) (j :: s) (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 ((Ob0 kk h, Ob0 kk j, Ob a, Ob b) => P kk kk (HK kk) s t c d)
-> (a ~> b) -> P kk kk (HK kk) s t c d
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 {s} (kk :: CAT s) (i :: s) (j :: s) (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
g
  (Ob a, Ob b) => r
r \\ :: forall (a :: HK kk i k) (b :: HK kk h j) r.
((Ob a, Ob b) => r) -> P kk kk (HK kk) s t a b -> r
\\ Hom{} = r
(Ob a, Ob b) => r
r
instance
  (Bicategory kk, Ob s, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => Functor (P kk kk (HK kk) (s :: COK kk h i) :: kk j k -> HK kk h j +-> HK kk i k)
  where
  map :: forall (a :: kk j k) (b :: kk j k).
(a ~> b) -> P kk kk (HK kk) s a ~> P kk kk (HK kk) s b
map a ~> b
f = ((P kk kk (HK kk) ('CO (UN 'CO s)) a
 :~> P kk kk (HK kk) ('CO (UN 'CO s)) b)
-> Prof
     (P kk kk (HK kk) ('CO (UN 'CO s)) a)
     (P kk kk (HK kk) ('CO (UN 'CO s)) b)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Hom @_ @b O a s ~> O a b
n) -> (O a (UN 'CO s) ~> O b b)
-> P kk kk (HK kk) ('CO (UN 'CO s)) b ('HomK a) ('HomK b)
forall {s} {h :: s} {i :: s} {j :: s} {k :: s}
       {kk :: s -> s -> Type} (a :: kk i k) (b :: kk h j) (s :: kk h i)
       (t :: kk j k).
(Ob a, Ob b, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(O a s ~> O t b) -> P kk kk (HK kk) ('CO s) t ('HomK a) ('HomK b)
Hom ((a ~> b
f (a ~> b) -> (b ~> b) -> O a b ~> O b b
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk h j). (CategoryOf (kk h j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (O a b ~> O b b)
-> (O a (UN 'CO s) ~> O a b) -> O a (UN 'CO s) ~> O b b
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(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
. O a s ~> O a b
O a (UN 'CO s) ~> O a b
n)) ((Ob0 kk j, Ob0 kk k, Ob a, Ob b) =>
 Prof
   (P kk kk (HK kk) ('CO (UN 'CO s)) a)
   (P kk kk (HK kk) ('CO (UN 'CO s)) b))
-> (a ~> b)
-> Prof
     (P kk kk (HK kk) ('CO (UN 'CO s)) a)
     (P kk kk (HK kk) ('CO (UN 'CO s)) 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 {s} (kk :: CAT s) (i :: s) (j :: s) (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
instance
  (Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => Functor (P kk kk (HK kk) :: COK kk h i -> kk j k -> HK kk h j +-> HK kk i k)
  where
  map :: forall (a :: COK kk h i) (b :: COK kk h i).
(a ~> b) -> P kk kk (HK kk) a ~> P kk kk (HK kk) b
map (Co b1 ~> a1
f) = ((P kk kk (HK kk) ('CO a1) .~> P kk kk (HK kk) ('CO b1))
-> Nat (P kk kk (HK kk) ('CO a1)) (P kk kk (HK kk) ('CO b1))
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((P kk kk (HK kk) ('CO a1) a :~> P kk kk (HK kk) ('CO b1) a)
-> Prof (P kk kk (HK kk) ('CO a1) a) (P kk kk (HK kk) ('CO b1) a)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Hom @a O a s ~> O a b
n) -> (O a b1 ~> O a b) -> P kk kk (HK kk) ('CO b1) a ('HomK a) ('HomK b)
forall {s} {h :: s} {i :: s} {j :: s} {k :: s}
       {kk :: s -> s -> Type} (a :: kk i k) (b :: kk h j) (s :: kk h i)
       (t :: kk j k).
(Ob a, Ob b, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(O a s ~> O t b) -> P kk kk (HK kk) ('CO s) t ('HomK a) ('HomK b)
Hom (O a a1 ~> O a b
O a s ~> O a b
n (O a a1 ~> O a b) -> (O a b1 ~> O a a1) -> O a b1 ~> O a b
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(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
. (forall (a :: kk i k). (CategoryOf (kk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b1 ~> a1) -> O a b1 ~> O a a1
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` b1 ~> a1
f)))) ((Ob0 kk h, Ob0 kk i, Ob b1, Ob a1) =>
 Nat (P kk kk (HK kk) ('CO a1)) (P kk kk (HK kk) ('CO b1)))
-> (b1 ~> a1)
-> Nat (P kk kk (HK kk) ('CO a1)) (P kk kk (HK kk) ('CO b1))
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 {s} (kk :: CAT s) (i :: s) (j :: s) (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
\\\ b1 ~> a1
f

instance (Bicategory kk) => LaxProfunctor kk kk (HK kk) where
  data P kk kk (HK kk) s t a b where
    Hom
      :: forall {h} {i} {j} {k} {kk} (a :: kk i k) (b :: kk h j) (s :: kk h i) (t :: kk j k)
       . (Ob a, Ob b, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k)
      => a `O` s ~> t `O` b
      -> P kk kk (HK kk) (CO s) t (HomK a) (HomK b)
  laxId :: forall (k :: k) (j :: k).
(Ob0 kk k, Ob0 kk j) =>
Id :~> P kk kk (HK kk) ('CO I) I
laxId (Id (HomW a ~> b
f) :: Id (a :: HK kk i j) b) = (O a I ~> O I b) -> P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b)
forall {s} {h :: s} {i :: s} {j :: s} {k :: s}
       {kk :: s -> s -> Type} (a :: kk i k) (b :: kk h j) (s :: kk h i)
       (t :: kk j k).
(Ob a, Ob b, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(O a s ~> O t b) -> P kk kk (HK kk) ('CO s) t ('HomK a) ('HomK b)
Hom (b ~> O I b
forall {i :: k} {j :: k} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv (b ~> O I b) -> (O a I ~> b) -> O a I ~> O I b
forall (b :: kk k j) (c :: kk k j) (a :: kk k 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 ~> b
f (a ~> b) -> (O a I ~> a) -> O a I ~> b
forall (b :: kk k j) (c :: kk k j) (a :: kk k 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
. O a I ~> a
forall {i :: k} {j :: k} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor) ((Ob a, Ob b) => P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b))
-> (a ~> b) -> P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b)
forall (a :: kk k j) (b :: kk k 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
f ((Ob I, Ob I) => P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b))
-> (I ~> I) -> P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b)
forall (a :: kk k k) (b :: kk k k) 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
\\ forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
forall (kk :: CAT k) (i :: k). (Bicategory kk, Ob0 kk i) => Obj I
iObj @kk @i ((Ob I, Ob I) => P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b))
-> (I ~> I) -> P kk kk (HK kk) ('CO I) I ('HomK a) ('HomK b)
forall (a :: kk j j) (b :: kk j 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
\\ forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
forall (kk :: CAT k) (i :: k). (Bicategory kk, Ob0 kk i) => Obj I
iObj @kk @j
  laxComp :: forall {j1 :: k} {i :: k} {j2 :: k} {k :: k} {h :: k} {j3 :: k}
       (s0 :: COK kk j1 i) (t0 :: kk j2 k) (s1 :: COK kk h j1)
       (t1 :: kk j3 j2).
(P kk kk (HK kk) s0 t0 :.: P kk kk (HK kk) s1 t1)
:~> P kk kk (HK kk) (O s0 s1) (O t0 t1)
laxComp (Hom @a @b @s @t O a s ~> O t0 b
n :.: Hom @_ @c @s' @t' O a s ~> O t1 b
m) =
    let s :: Obj s
s = forall (a :: kk j1 i). (CategoryOf (kk j1 i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s; t :: Obj t0
t = forall (a :: kk j2 k). (CategoryOf (kk j2 k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t; s' :: Obj s
s' = forall (a :: kk h j1). (CategoryOf (kk h j1), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s'; t' :: Obj t1
t' = forall (a :: kk j3 j2). (CategoryOf (kk j3 j2), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t'
    in (O a (O s s) ~> O (O t0 t1) b)
-> P kk kk (HK kk) ('CO (O s s)) (O t0 t1) ('HomK a) ('HomK b)
forall {s} {h :: s} {i :: s} {j :: s} {k :: s}
       {kk :: s -> s -> Type} (a :: kk i k) (b :: kk h j) (s :: kk h i)
       (t :: kk j k).
(Ob a, Ob b, Ob s, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(O a s ~> O t b) -> P kk kk (HK kk) ('CO s) t ('HomK a) ('HomK b)
Hom (forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @a @s @s' (O a (O s s) ~> O (O a s) s)
-> (O (O a s) s ~> O (O t0 b) s) -> O a (O s s) ~> O (O t0 b) s
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== O a s ~> O t0 b
n (O a s ~> O t0 b) -> Obj s -> O (O a s) s ~> O (O t0 b) s
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj s
s' (O a (O s s) ~> O (O t0 b) s)
-> (O (O t0 b) s ~> O t0 (O b s)) -> O a (O s s) ~> O t0 (O b s)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @t @b @s' (O a (O s s) ~> O t0 (O b s))
-> (O t0 (O b s) ~> O t0 (O t1 b)) -> O a (O s s) ~> O t0 (O t1 b)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj t0
t Obj t0 -> (O b s ~> O t1 b) -> O t0 (O b s) ~> O t0 (O t1 b)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| O b s ~> O t1 b
O a s ~> O t1 b
m (O a (O s s) ~> O t0 (O t1 b))
-> (O t0 (O t1 b) ~> O (O t0 t1) b) -> O a (O s s) ~> O (O t0 t1) b
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @t @t' @c)
        ((Ob0 kk h, Ob0 kk i, Ob (O s s), Ob (O s s)) =>
 P kk kk (HK kk) ('CO (O s s)) (O t0 t1) ('HomK a) ('HomK b))
-> (O s s ~> O s s)
-> P kk kk (HK kk) ('CO (O s s)) (O t0 t1) ('HomK a) ('HomK 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 {s} (kk :: CAT s) (i :: s) (j :: s) (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
\\\ (Obj s
s Obj s -> Obj s -> O s s ~> O s s
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj s
s')
        ((Ob0 kk j3, Ob0 kk k, Ob (O t0 t1), Ob (O t0 t1)) =>
 P kk kk (HK kk) ('CO (O s s)) (O t0 t1) ('HomK a) ('HomK b))
-> (O t0 t1 ~> O t0 t1)
-> P kk kk (HK kk) ('CO (O s s)) (O t0 t1) ('HomK a) ('HomK 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 {s} (kk :: CAT s) (i :: s) (j :: s) (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
\\\ (Obj t0
t Obj t0 -> Obj t1 -> O t0 t1 ~> O t0 t1
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj t1
t')