module Proarrow.Category.Bicategory.Product where

import Prelude (type (~))

import Proarrow.Category.Bicategory (Bicategory (..), Adjunction (..), Monad (..), Comonad (..))
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)

type PRODK :: CAT j -> CAT k -> CAT (j, k)
data PRODK jj kk j k where
  PROD :: jj (Fst ik) (Fst jl) -> kk (Snd ik) (Snd jl) -> PRODK jj kk ik jl

type family PRODFST (p :: PRODK jj kk j k) :: jj (Fst j) (Fst k) where
  PRODFST (PROD p q) = p
type family PRODSND (p :: PRODK jj kk j k) :: kk (Snd j) (Snd k) where
  PRODSND (PROD p q) = q
type family Fst (p :: (j, k)) :: j where
  Fst '(a, b) = a
type family Snd (p :: (j, k)) :: k where
  Snd '(a, b) = b

type Prod :: CAT (PRODK jj kk j k)
data Prod a b where
  Prod :: { forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
Prod ('PROD a c) ('PROD b d) -> a ~> b
fst :: a ~> b, forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
Prod ('PROD a c) ('PROD b d) -> c ~> d
snd :: c ~> d } -> Prod (PROD a c) (PROD b d)

instance (CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => Profunctor (Prod :: CAT (PRODK jj kk ik jl)) where
  dimap :: forall (c :: PRODK jj kk ik jl) (a :: PRODK jj kk ik jl)
       (b :: PRODK jj kk ik jl) (d :: PRODK jj kk ik jl).
(c ~> a) -> (b ~> d) -> Prod a b -> Prod c d
dimap = (c ~> a) -> (b ~> d) -> Prod a b -> Prod c d
Prod c a -> Prod b d -> Prod a b -> Prod 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 :: PRODK jj kk ik jl) (b :: PRODK jj kk ik jl) r.
((Ob a, Ob b) => r) -> Prod a b -> r
\\ Prod a ~> b
f c ~> d
g = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: jj (Fst ik) (Fst jl)) (b :: jj (Fst ik) (Fst jl)) 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 c, Ob d) => r) -> (c ~> d) -> r
forall (a :: kk (Snd ik) (Snd jl)) (b :: kk (Snd ik) (Snd jl)) 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
\\ c ~> d
g
instance (CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => Promonad (Prod :: CAT (PRODK jj kk ik jl)) where
  id :: forall (a :: PRODK jj kk ik jl). Ob a => Prod a a
id = (PRODFST a ~> PRODFST a)
-> (PRODSND a ~> PRODSND a)
-> Prod
     ('PROD (PRODFST a) (PRODSND a)) ('PROD (PRODFST a) (PRODSND a))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod PRODFST a ~> PRODFST a
forall (a :: jj (Fst ik) (Fst jl)). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id PRODSND a ~> PRODSND a
forall (a :: kk (Snd ik) (Snd jl)). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Prod a ~> b
f1 c ~> d
g1 . :: forall (b :: PRODK jj kk ik jl) (c :: PRODK jj kk ik jl)
       (a :: PRODK jj kk ik jl).
Prod b c -> Prod a b -> Prod a c
. Prod a ~> b
f2 c ~> d
g2 = (a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (a ~> b
f1 (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: jj (Fst ik) (Fst jl)) (c :: jj (Fst ik) (Fst jl))
       (a :: jj (Fst ik) (Fst jl)).
(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
f2) (c ~> d
g1 (c ~> d) -> (c ~> c) -> c ~> d
forall (b :: kk (Snd ik) (Snd jl)) (c :: kk (Snd ik) (Snd jl))
       (a :: kk (Snd ik) (Snd jl)).
(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
. c ~> c
c ~> d
g2)
instance (CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => CategoryOf (PRODK jj kk ik jl) where
  type (~>) = Prod
  type Ob (p :: PRODK jj kk ik jl) = (Ob (PRODFST p), Ob (PRODSND p), p ~ PROD (PRODFST p) (PRODSND p))

instance (Bicategory jj, Bicategory kk) => Bicategory (PRODK jj kk) where
  type Ob0 (PRODK jj kk) jk = (Ob0 jj (Fst jk), Ob0 kk (Snd jk))
  type I = PROD I I
  type PROD a b `O` PROD c d = PROD (a `O` c) (b `O` d)
  (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: (j, k)) (j :: (j, k)) (ps :: PRODK jj kk i j)
       (qs :: PRODK jj kk i j) r.
((Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Prod a ~> b
f c ~> d
g = r
(Ob0 jj (Fst i), Ob0 jj (Fst j), Ob a, Ob b) => r
(Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob ps, Ob qs) => r
r ((Ob0 jj (Fst i), Ob0 jj (Fst j), Ob a, Ob b) => r)
-> (a ~> b) -> r
forall (i :: j) (j :: j) (ps :: jj i j) (qs :: jj i j) r.
((Ob0 jj i, Ob0 jj 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 (Snd i), Ob0 kk (Snd j), Ob c, Ob d) => r)
-> (c ~> d) -> 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 {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
\\\ c ~> d
g
  iObj :: forall (i :: (j, k)). Ob0 (PRODK jj kk) i => Obj I
iObj = (I ~> I) -> (I ~> I) -> Prod ('PROD I I) ('PROD I I)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod I ~> I
forall (i :: j). Ob0 jj i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj I ~> I
forall (i :: k). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  Prod a ~> b
f c ~> d
g o :: forall {i :: (j, k)} (j :: (j, k)) (k :: (j, k))
       (a :: PRODK jj kk j k) (b :: PRODK jj kk j k)
       (c :: PRODK jj kk i j) (d :: PRODK jj kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Prod a ~> b
h c ~> d
i = (O a a ~> O b b)
-> (O c c ~> O d d)
-> Prod ('PROD (O a a) (O c c)) ('PROD (O b b) (O d d))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (a ~> b
f (a ~> b) -> (a ~> b) -> O a a ~> O b b
forall {i :: j} (j :: j) (k :: j) (a :: jj j k) (b :: jj j k)
       (c :: jj i j) (d :: jj 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
h) (c ~> d
g (c ~> d) -> (c ~> d) -> O c c ~> O d d
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` c ~> d
i)
  leftUnitor :: forall {i :: (j, k)} {j :: (j, k)} (a :: PRODK jj kk i j).
(Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob a) =>
O I a ~> a
leftUnitor = (O I (PRODFST a) ~> PRODFST a)
-> (O I (PRODSND a) ~> PRODSND a)
-> Prod
     ('PROD (O I (PRODFST a)) (O I (PRODSND a)))
     ('PROD (PRODFST a) (PRODSND a))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod O I (PRODFST a) ~> PRODFST a
forall {i :: j} {j :: j} (a :: jj i j).
(Ob0 jj i, Ob0 jj j, Ob a) =>
O I a ~> 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 I a ~> a
leftUnitor O I (PRODSND a) ~> PRODSND a
forall {i :: k} {j :: k} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> 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 I a ~> a
leftUnitor
  leftUnitorInv :: forall {i :: (j, k)} {j :: (j, k)} (a :: PRODK jj kk i j).
(Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob a) =>
a ~> O I a
leftUnitorInv = (PRODFST a ~> O I (PRODFST a))
-> (PRODSND a ~> O I (PRODSND a))
-> Prod
     ('PROD (PRODFST a) (PRODSND a))
     ('PROD (O I (PRODFST a)) (O I (PRODSND a)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod PRODFST a ~> O I (PRODFST a)
forall {i :: j} {j :: j} (a :: jj i j).
(Ob0 jj i, Ob0 jj 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 PRODSND a ~> O I (PRODSND a)
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
  rightUnitor :: forall {i :: (j, k)} {j :: (j, k)} (a :: PRODK jj kk i j).
(Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob a) =>
O a I ~> a
rightUnitor = (O (PRODFST a) I ~> PRODFST a)
-> (O (PRODSND a) I ~> PRODSND a)
-> Prod
     ('PROD (O (PRODFST a) I) (O (PRODSND a) I))
     ('PROD (PRODFST a) (PRODSND a))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod O (PRODFST a) I ~> PRODFST a
forall {i :: j} {j :: j} (a :: jj i j).
(Ob0 jj i, Ob0 jj 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 O (PRODSND a) I ~> PRODSND 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
  rightUnitorInv :: forall {i :: (j, k)} {j :: (j, k)} (a :: PRODK jj kk i j).
(Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j, Ob a) =>
a ~> O a I
rightUnitorInv = (PRODFST a ~> O (PRODFST a) I)
-> (PRODSND a ~> O (PRODSND a) I)
-> Prod
     ('PROD (PRODFST a) (PRODSND a))
     ('PROD (O (PRODFST a) I) (O (PRODSND a) I))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod PRODFST a ~> O (PRODFST a) I
forall {i :: j} {j :: j} (a :: jj i j).
(Ob0 jj i, Ob0 jj j, Ob a) =>
a ~> O a I
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 a I
rightUnitorInv PRODSND a ~> O (PRODSND a) I
forall {i :: k} {j :: k} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
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 a I
rightUnitorInv
  associator :: forall {h :: (j, k)} {i :: (j, k)} {j :: (j, k)} {k :: (j, k)}
       (a :: PRODK jj kk j k) (b :: PRODK jj kk i j)
       (c :: PRODK jj kk h i).
(Ob0 (PRODK jj kk) h, Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j,
 Ob0 (PRODK jj kk) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @(PROD p q) @(PROD r s) @(PROD t u) = (O (O (PRODFST a) (PRODFST b)) (PRODFST c)
 ~> O (PRODFST a) (O (PRODFST b) (PRODFST c)))
-> (O (O (PRODSND a) (PRODSND b)) (PRODSND c)
    ~> O (PRODSND a) (O (PRODSND b) (PRODSND c)))
-> Prod
     ('PROD
        (O (O (PRODFST a) (PRODFST b)) (PRODFST c))
        (O (O (PRODSND a) (PRODSND b)) (PRODSND c)))
     ('PROD
        (O (PRODFST a) (O (PRODFST b) (PRODFST c)))
        (O (PRODSND a) (O (PRODSND b) (PRODSND c))))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (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 j) {h :: j} {i :: j} {j :: j} {k :: j}
       (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 @jj @p @r @t) (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 @kk @q @s @u)
  associatorInv :: forall {h :: (j, k)} {i :: (j, k)} {j :: (j, k)} {k :: (j, k)}
       (a :: PRODK jj kk j k) (b :: PRODK jj kk i j)
       (c :: PRODK jj kk h i).
(Ob0 (PRODK jj kk) h, Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j,
 Ob0 (PRODK jj kk) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @(PROD p q) @(PROD r s) @(PROD t u) = (O (PRODFST a) (O (PRODFST b) (PRODFST c))
 ~> O (O (PRODFST a) (PRODFST b)) (PRODFST c))
-> (O (PRODSND a) (O (PRODSND b) (PRODSND c))
    ~> O (O (PRODSND a) (PRODSND b)) (PRODSND c))
-> Prod
     ('PROD
        (O (PRODFST a) (O (PRODFST b) (PRODFST c)))
        (O (PRODSND a) (O (PRODSND b) (PRODSND c))))
     ('PROD
        (O (O (PRODFST a) (PRODFST b)) (PRODFST c))
        (O (O (PRODSND a) (PRODSND b)) (PRODSND c)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (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 j) {h :: j} {i :: j} {j :: j} {k :: j}
       (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 @jj @p @r @t) (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 @kk @q @s @u)

instance (Adjunction (PRODFST l) (PRODFST r), Adjunction (PRODSND l) (PRODSND r), Ob l, Ob r) => Adjunction l r where
  unit :: I ~> O r l
unit = (I ~> O (PRODFST r) (PRODFST l))
-> (I ~> O (PRODSND r) (PRODSND l))
-> Prod
     ('PROD I I)
     ('PROD (O (PRODFST r) (PRODFST l)) (O (PRODSND r) (PRODSND l)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (forall (l :: jj (Fst c) (Fst d)) (r :: jj (Fst d) (Fst c)).
Adjunction l r =>
I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @(PRODFST l) @(PRODFST r)) (forall (l :: kk (Snd c) (Snd d)) (r :: kk (Snd d) (Snd c)).
Adjunction l r =>
I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @(PRODSND l) @(PRODSND r))
  counit :: O l r ~> I
counit = (O (PRODFST l) (PRODFST r) ~> I)
-> (O (PRODSND l) (PRODSND r) ~> I)
-> Prod
     ('PROD (O (PRODFST l) (PRODFST r)) (O (PRODSND l) (PRODSND r)))
     ('PROD I I)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (forall (l :: jj (Fst c) (Fst d)) (r :: jj (Fst d) (Fst c)).
Adjunction l r =>
O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @(PRODFST l) @(PRODFST r)) (forall (l :: kk (Snd c) (Snd d)) (r :: kk (Snd d) (Snd c)).
Adjunction l r =>
O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @(PRODSND l) @(PRODSND r))

instance (Monad (PRODFST m), Monad (PRODSND m), Ob m) => Monad m where
  eta :: I ~> m
eta = (I ~> PRODFST m)
-> (I ~> PRODSND m)
-> Prod ('PROD I I) ('PROD (PRODFST m) (PRODSND m))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod I ~> PRODFST m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta I ~> PRODSND m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  mu :: O m m ~> m
mu = (O (PRODFST m) (PRODFST m) ~> PRODFST m)
-> (O (PRODSND m) (PRODSND m) ~> PRODSND m)
-> Prod
     ('PROD (O (PRODFST m) (PRODFST m)) (O (PRODSND m) (PRODSND m)))
     ('PROD (PRODFST m) (PRODSND m))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod O (PRODFST m) (PRODFST m) ~> PRODFST m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu O (PRODSND m) (PRODSND m) ~> PRODSND m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

instance (Comonad (PRODFST m), Comonad (PRODSND m), Ob m) => Comonad m where
  epsilon :: m ~> I
epsilon = (PRODFST m ~> I)
-> (PRODSND m ~> I)
-> Prod ('PROD (PRODFST m) (PRODSND m)) ('PROD I I)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod PRODFST m ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon PRODSND m ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon
  delta :: m ~> O m m
delta = (PRODFST m ~> O (PRODFST m) (PRODFST m))
-> (PRODSND m ~> O (PRODSND m) (PRODSND m))
-> Prod
     ('PROD (PRODFST m) (PRODSND m))
     ('PROD (O (PRODFST m) (PRODFST m)) (O (PRODSND m) (PRODSND m)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod PRODFST m ~> O (PRODFST m) (PRODFST m)
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta PRODSND m ~> O (PRODSND m) (PRODSND m)
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta

instance (HasCompanions hj vj, HasCompanions hk vk) => HasCompanions (PRODK hj hk) (PRODK vj vk) where
  type Companion (PRODK hj hk) fg = PROD (Companion hj (PRODFST fg)) (Companion hk (PRODSND fg))
  mapCompanion :: forall {j :: (j, k)} {k :: (j, k)} (f :: PRODK vj vk j k)
       (g :: PRODK vj vk j k).
(f ~> g) -> Companion (PRODK hj hk) f ~> Companion (PRODK hj hk) g
mapCompanion (Prod a ~> b
f c ~> d
g) = (Companion hj a ~> Companion hj b)
-> (Companion hk c ~> Companion hk d)
-> Prod
     ('PROD (Companion hj a) (Companion hk c))
     ('PROD (Companion hj b) (Companion hk d))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod ((a ~> b) -> Companion hj a ~> Companion hj b
forall {j :: j} {k :: j} (f :: vj j k) (g :: vj j k).
(f ~> g) -> Companion hj f ~> Companion hj g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion a ~> b
f) ((c ~> d) -> Companion hk c ~> Companion hk d
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion c ~> d
g)
  compToId :: forall (k :: (j, k)).
Ob0 (PRODK vj vk) k =>
Companion (PRODK hj hk) I ~> I
compToId = (Companion hj I ~> I)
-> (Companion hk I ~> I)
-> Prod ('PROD (Companion hj I) (Companion hk I)) ('PROD I I)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod Companion hj I ~> I
forall (k :: j). Ob0 vj k => Companion hj I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId Companion hk I ~> I
forall (k :: k). Ob0 vk k => Companion hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId
  compFromId :: forall (k :: (j, k)).
Ob0 (PRODK vj vk) k =>
I ~> Companion (PRODK hj hk) I
compFromId = (I ~> Companion hj I)
-> (I ~> Companion hk I)
-> Prod ('PROD I I) ('PROD (Companion hj I) (Companion hk I))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod I ~> Companion hj I
forall (k :: j). Ob0 vj k => I ~> Companion hj I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId I ~> Companion hk I
forall (k :: k). Ob0 vk k => I ~> Companion hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId
  compToCompose :: forall {i :: (j, k)} {j :: (j, k)} {k :: (j, k)}
       (f :: PRODK vj vk j k) (g :: PRODK vj vk i j).
Obj f
-> Obj g
-> Companion (PRODK hj hk) (O f g)
   ~> O (Companion (PRODK hj hk) f) (Companion (PRODK hj hk) g)
compToCompose (Prod a ~> b
fl c ~> d
fr) (Prod a ~> b
gl c ~> d
gr) = (Companion hj (O b b) ~> O (Companion hj b) (Companion hj b))
-> (Companion hk (O d d) ~> O (Companion hk d) (Companion hk d))
-> Prod
     ('PROD (Companion hj (O b b)) (Companion hk (O d d)))
     ('PROD
        (O (Companion hj b) (Companion hj b))
        (O (Companion hk d) (Companion hk d)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (Obj b
-> Obj b
-> Companion hj (O b b) ~> O (Companion hj b) (Companion hj b)
forall {i :: j} {j :: j} {k :: j} (f :: vj j k) (g :: vj i j).
Obj f
-> Obj g
-> Companion hj (O f g) ~> O (Companion hj f) (Companion hj g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose a ~> b
Obj b
fl a ~> b
Obj b
gl) (Obj d
-> Obj d
-> Companion hk (O d d) ~> O (Companion hk d) (Companion hk d)
forall {i :: k} {j :: k} {k :: k} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose c ~> d
Obj d
fr c ~> d
Obj d
gr)
  compFromCompose :: forall {j1 :: (j, k)} {j2 :: (j, k)} {k :: (j, k)}
       (f :: PRODK vj vk j2 k) (g :: PRODK vj vk j1 j2).
Obj f
-> Obj g
-> O (Companion (PRODK hj hk) f) (Companion (PRODK hj hk) g)
   ~> Companion (PRODK hj hk) (O f g)
compFromCompose (Prod a ~> b
fl c ~> d
fr) (Prod a ~> b
gl c ~> d
gr) = (O (Companion hj b) (Companion hj b) ~> Companion hj (O b b))
-> (O (Companion hk d) (Companion hk d) ~> Companion hk (O d d))
-> Prod
     ('PROD
        (O (Companion hj b) (Companion hj b))
        (O (Companion hk d) (Companion hk d)))
     ('PROD (Companion hj (O b b)) (Companion hk (O d d)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (Obj b
-> Obj b
-> O (Companion hj b) (Companion hj b) ~> Companion hj (O b b)
forall {j1 :: j} {j2 :: j} {k :: j} (f :: vj j2 k) (g :: vj j1 j2).
Obj f
-> Obj g
-> O (Companion hj f) (Companion hj g) ~> Companion hj (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose a ~> b
Obj b
fl a ~> b
Obj b
gl) (Obj d
-> Obj d
-> O (Companion hk d) (Companion hk d) ~> Companion hk (O d d)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose c ~> d
Obj d
fr c ~> d
Obj d
gr)

instance (Equipment hj vj, Equipment hk vk) => Equipment (PRODK hj hk) (PRODK vj vk) where
  type Conjoint (PRODK hj hk) fg = PROD (Conjoint hj (PRODFST fg)) (Conjoint hk (PRODSND fg))
  mapConjoint :: forall {j :: (j, k)} {k :: (j, k)} (f :: PRODK vj vk j k)
       (g :: PRODK vj vk j k).
(f ~> g) -> Conjoint (PRODK hj hk) g ~> Conjoint (PRODK hj hk) f
mapConjoint (Prod a ~> b
f c ~> d
g) = (Conjoint hj b ~> Conjoint hj a)
-> (Conjoint hk d ~> Conjoint hk c)
-> Prod
     ('PROD (Conjoint hj b) (Conjoint hk d))
     ('PROD (Conjoint hj a) (Conjoint hk c))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod ((a ~> b) -> Conjoint hj b ~> Conjoint hj a
forall {j :: j} {k :: j} (f :: vj j k) (g :: vj j k).
(f ~> g) -> Conjoint hj g ~> Conjoint hj f
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint a ~> b
f) ((c ~> d) -> Conjoint hk d ~> Conjoint hk c
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint c ~> d
g)
  conjToId :: forall (k :: (j, k)).
Ob0 (PRODK vj vk) k =>
Conjoint (PRODK hj hk) I ~> I
conjToId = (Conjoint hj I ~> I)
-> (Conjoint hk I ~> I)
-> Prod ('PROD (Conjoint hj I) (Conjoint hk I)) ('PROD I I)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod Conjoint hj I ~> I
forall (k :: j). Ob0 vj k => Conjoint hj I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
Conjoint hk I ~> I
conjToId Conjoint hk I ~> I
forall (k :: k). Ob0 vk k => Conjoint hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
Conjoint hk I ~> I
conjToId
  conjFromId :: forall (k :: (j, k)).
Ob0 (PRODK vj vk) k =>
I ~> Conjoint (PRODK hj hk) I
conjFromId = (I ~> Conjoint hj I)
-> (I ~> Conjoint hk I)
-> Prod ('PROD I I) ('PROD (Conjoint hj I) (Conjoint hk I))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod I ~> Conjoint hj I
forall (k :: j). Ob0 vj k => I ~> Conjoint hj I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
I ~> Conjoint hk I
conjFromId I ~> Conjoint hk I
forall (k :: k). Ob0 vk k => I ~> Conjoint hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
I ~> Conjoint hk I
conjFromId
  conjToCompose :: forall {k1 :: (j, k)} {j :: (j, k)} {k2 :: (j, k)}
       (f :: PRODK vj vk j k2) (g :: PRODK vj vk k1 j).
Obj f
-> Obj g
-> Conjoint (PRODK hj hk) (O f g)
   ~> O (Conjoint (PRODK hj hk) g) (Conjoint (PRODK hj hk) f)
conjToCompose (Prod a ~> b
fl c ~> d
fr) (Prod a ~> b
gl c ~> d
gr) = (Conjoint hj (O b b) ~> O (Conjoint hj b) (Conjoint hj b))
-> (Conjoint hk (O d d) ~> O (Conjoint hk d) (Conjoint hk d))
-> Prod
     ('PROD (Conjoint hj (O b b)) (Conjoint hk (O d d)))
     ('PROD
        (O (Conjoint hj b) (Conjoint hj b))
        (O (Conjoint hk d) (Conjoint hk d)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (Obj b
-> Obj b
-> Conjoint hj (O b b) ~> O (Conjoint hj b) (Conjoint hj b)
forall {k1 :: j} {j :: j} {k2 :: j} (f :: vj j k2) (g :: vj k1 j).
Obj f
-> Obj g
-> Conjoint hj (O f g) ~> O (Conjoint hj g) (Conjoint hj f)
forall {c} (hk :: CAT c) (vk :: CAT c) {k1 :: c} {j :: c} {k2 :: c}
       (f :: vk j k2) (g :: vk k1 j).
Equipment hk vk =>
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
conjToCompose a ~> b
Obj b
fl a ~> b
Obj b
gl) (Obj d
-> Obj d
-> Conjoint hk (O d d) ~> O (Conjoint hk d) (Conjoint hk d)
forall {k1 :: k} {j :: k} {k2 :: k} (f :: vk j k2) (g :: vk k1 j).
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {k1 :: c} {j :: c} {k2 :: c}
       (f :: vk j k2) (g :: vk k1 j).
Equipment hk vk =>
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
conjToCompose c ~> d
Obj d
fr c ~> d
Obj d
gr)
  conjFromCompose :: forall {j1 :: (j, k)} {j2 :: (j, k)} {k :: (j, k)}
       (f :: PRODK vj vk j2 k) (g :: PRODK vj vk j1 j2).
Obj f
-> Obj g
-> O (Conjoint (PRODK hj hk) g) (Conjoint (PRODK hj hk) f)
   ~> Conjoint (PRODK hj hk) (O f g)
conjFromCompose (Prod a ~> b
fl c ~> d
fr) (Prod a ~> b
gl c ~> d
gr) = (O (Conjoint hj b) (Conjoint hj b) ~> Conjoint hj (O b b))
-> (O (Conjoint hk d) (Conjoint hk d) ~> Conjoint hk (O d d))
-> Prod
     ('PROD
        (O (Conjoint hj b) (Conjoint hj b))
        (O (Conjoint hk d) (Conjoint hk d)))
     ('PROD (Conjoint hj (O b b)) (Conjoint hk (O d d)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (Obj b
-> Obj b
-> O (Conjoint hj b) (Conjoint hj b) ~> Conjoint hj (O b b)
forall {j1 :: j} {j2 :: j} {k :: j} (f :: vj j2 k) (g :: vj j1 j2).
Obj f
-> Obj g
-> O (Conjoint hj g) (Conjoint hj f) ~> Conjoint hj (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
Equipment hk vk =>
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
conjFromCompose a ~> b
Obj b
fl a ~> b
Obj b
gl) (Obj d
-> Obj d
-> O (Conjoint hk d) (Conjoint hk d) ~> Conjoint hk (O d d)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
Equipment hk vk =>
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
conjFromCompose c ~> d
Obj d
fr c ~> d
Obj d
gr)
  comConUnit :: forall {j :: (j, k)} {k :: (j, k)} (f :: PRODK vj vk j k).
Obj f
-> I ~> O (Conjoint (PRODK hj hk) f) (Companion (PRODK hj hk) f)
comConUnit (Prod a ~> b
f c ~> d
g) = (I ~> O (Conjoint hj b) (Companion hj b))
-> (I ~> O (Conjoint hk d) (Companion hk d))
-> Prod
     ('PROD I I)
     ('PROD
        (O (Conjoint hj b) (Companion hj b))
        (O (Conjoint hk d) (Companion hk d)))
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (Obj b -> I ~> O (Conjoint hj b) (Companion hj b)
forall {j :: j} {k :: j} (f :: vj j k).
Obj f -> I ~> O (Conjoint hj f) (Companion hj f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit a ~> b
Obj b
f) (Obj d -> I ~> O (Conjoint hk d) (Companion hk d)
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit c ~> d
Obj d
g)
  comConCounit :: forall {j :: (j, k)} {k :: (j, k)} (f :: PRODK vj vk j k).
Obj f
-> O (Companion (PRODK hj hk) f) (Conjoint (PRODK hj hk) f) ~> I
comConCounit (Prod a ~> b
f c ~> d
g) = (O (Companion hj b) (Conjoint hj b) ~> I)
-> (O (Companion hk d) (Conjoint hk d) ~> I)
-> Prod
     ('PROD
        (O (Companion hj b) (Conjoint hj b))
        (O (Companion hk d) (Conjoint hk d)))
     ('PROD I I)
forall {j} {jj :: CAT j} {k} {j :: (j, k)} {k :: (j, k)}
       {kk :: CAT k} (a :: jj (Fst j) (Fst k)) (b :: jj (Fst j) (Fst k))
       (c :: kk (Snd j) (Snd k)) (d :: kk (Snd j) (Snd k)).
(a ~> b) -> (c ~> d) -> Prod ('PROD a c) ('PROD b d)
Prod (Obj b -> O (Companion hj b) (Conjoint hj b) ~> I
forall {j :: j} {k :: j} (f :: vj j k).
Obj f -> O (Companion hj f) (Conjoint hj f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit a ~> b
Obj b
f) (Obj d -> O (Companion hk d) (Conjoint hk d) ~> I
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit c ~> d
Obj d
g)