module Proarrow.Category.Bicategory.Product where

import Prelude (type (~))

import Proarrow.Category.Instance.Product ()
import Proarrow.Category.Bicategory (Bicategory (..), Adjunction_ (..), Monad (..), Comonad (..), Adj (..))
import Proarrow.Category.Equipment (Equipment (..), TightAdjoint, CotightAdjoint, Tight, Cotight, IsOb, WithObO2 (..))
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 :: 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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) 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 :: 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 :: 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 :: 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 :: 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)
  withOb2 :: forall {i :: (j, k)} {j :: (j, k)} {k :: (j, k)}
       (a :: PRODK jj kk j k) (b :: PRODK jj kk i j) r.
(Ob a, Ob b, Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j,
 Ob0 (PRODK jj kk) k) =>
(Ob (O a b) => r) -> r
withOb2 @(PROD a b) @(PROD c d) Ob (O a b) => r
r = forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT j) {i :: j} {j :: j} {k :: j} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @jj @a @c (forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @b @d r
Ob (O (PRODSND a) (PRODSND b)) => r
Ob (O a b) => r
r)
  withOb0s :: forall {j :: (j, k)} {k :: (j, k)} (a :: PRODK jj kk j k) r.
Ob a =>
((Ob0 (PRODK jj kk) j, Ob0 (PRODK jj kk) k) => r) -> r
withOb0s @(PROD a b) (Ob0 (PRODK jj kk) j, Ob0 (PRODK jj kk) k) => r
r = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT j) {j :: j} {k :: j} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @jj @a (forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @b r
(Ob0 kk (Snd j), Ob0 kk (Snd k)) => r
(Ob0 (PRODK jj kk) j, Ob0 (PRODK jj kk) k) => r
r)
  (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
  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
  adj :: Adj l r
adj = case (forall (l :: jj (Fst c) (Fst d)) (r :: jj (Fst d) (Fst c)).
Adjunction_ l r =>
Adj l r
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction_ l r =>
Adj l r
adj @(PRODFST l) @(PRODFST r), forall (l :: kk (Snd c) (Snd d)) (r :: kk (Snd d) (Snd c)).
Adjunction_ l r =>
Adj l r
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction_ l r =>
Adj l r
adj @(PRODSND l) @(PRODSND r)) of
    (Adj I ~> O (PRODFST r) (PRODFST l)
un1 O (PRODFST l) (PRODFST r) ~> I
coun1, Adj I ~> O (PRODSND r) (PRODSND l)
un2 O (PRODSND l) (PRODSND r) ~> I
coun2) -> Adj { adjUnit :: I ~> O r l
adjUnit = (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 I ~> O (PRODFST r) (PRODFST l)
un1 I ~> O (PRODSND r) (PRODSND l)
un2, adjCounit :: O l r ~> I
adjCounit = (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 O (PRODFST l) (PRODFST r) ~> I
coun1 O (PRODSND l) (PRODSND r) ~> I
coun2 }

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

type instance IsOb Tight p = (IsOb Tight (PRODFST p), IsOb Tight (PRODSND p))
type instance IsOb Cotight p = (IsOb Cotight (PRODFST p), IsOb Cotight (PRODSND p))
type instance TightAdjoint p = PROD (TightAdjoint (PRODFST p)) (TightAdjoint (PRODSND p))
type instance CotightAdjoint p = PROD (CotightAdjoint (PRODFST p)) (CotightAdjoint (PRODSND p))
instance (WithObO2 Tight jj, WithObO2 Tight kk) => WithObO2 Tight (PRODK jj kk) where
  withObO2 :: forall {i :: (j, k)} {j :: (j, k)} {k :: (j, k)}
       (a :: PRODK jj kk j k) (b :: PRODK jj kk i j) r.
(Ob a, Ob b, IsOb Tight a, IsOb Tight b) =>
((IsOb Tight (O a b), Ob (O a b)) => r) -> r
withObO2 @p @q (IsOb Tight (O a b), Ob (O a b)) => r
r = forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: j -> j -> Type) {i :: j} {j :: j} {k :: j}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @jj @(PRODFST p) @(PRODFST q) (forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: k -> k -> Type) {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @kk @(PRODSND p) @(PRODSND q) r
(IsOb Tight (O (PRODSND a) (PRODSND b)),
 Ob (O (PRODSND a) (PRODSND b))) =>
r
(IsOb Tight (O a b), Ob (O a b)) => r
r)
instance (WithObO2 Cotight jj, WithObO2 Cotight kk) => WithObO2 Cotight (PRODK jj kk) where
  withObO2 :: forall {i :: (j, k)} {j :: (j, k)} {k :: (j, k)}
       (a :: PRODK jj kk j k) (b :: PRODK jj kk i j) r.
(Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) =>
((IsOb Cotight (O a b), Ob (O a b)) => r) -> r
withObO2 @p @q (IsOb Cotight (O a b), Ob (O a b)) => r
r = forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: j -> j -> Type) {i :: j} {j :: j} {k :: j}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Cotight @jj @(PRODFST p) @(PRODFST q) (forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: k -> k -> Type) {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Cotight @kk @(PRODSND p) @(PRODSND q) r
(IsOb Cotight (O (PRODSND a) (PRODSND b)),
 Ob (O (PRODSND a) (PRODSND b))) =>
r
(IsOb Cotight (O a b), Ob (O a b)) => r
r)
instance (Equipment jj, Equipment kk) => Equipment (PRODK jj kk) where
  withTightAdjoint :: forall {j :: (j, k)} {k1 :: (j, k)} (f :: PRODK jj kk j k1) r.
IsCotight f =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @(PROD p q) (Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r = forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
forall (kk :: CAT j) {j :: j} {k1 :: j} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @jj @p (forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
forall (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @kk @q r
(Adjunction_ (TightAdjoint (PRODSND f)) (PRODSND f),
 IsTight (TightAdjoint (PRODSND f))) =>
r
(Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r)
  withCotightAdjoint :: forall {j :: (j, k)} {k1 :: (j, k)} (f :: PRODK jj kk j k1) r.
IsTight f =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @(PROD p q) (Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r = forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
forall (kk :: CAT j) {j :: j} {k1 :: j} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @jj @p (forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
forall (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @kk @q r
(Adjunction_ (PRODSND f) (CotightAdjoint (PRODSND f)),
 IsCotight (CotightAdjoint (PRODSND f))) =>
r
(Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r)