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


import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Core (CategoryOf(..), Profunctor(..), CAT, 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 :: a ~> b -> 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 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 ((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 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
\\\ c ~> d
g
  Prod a ~> b
f c ~> d
g o :: forall {k1 :: (j, k)} (i :: (j, k)) (j :: (j, k))
       (a :: PRODK jj kk i j) (b :: PRODK jj kk i j)
       (c :: PRODK jj kk j k1) (d :: PRODK jj kk j k1).
(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 {k1 :: j} (i :: j) (j :: j) (a :: jj i j) (b :: jj i j)
       (c :: jj j k1) (d :: jj 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
h) (c ~> d
g (c ~> d) -> (c ~> d) -> O c c ~> O d d
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` c ~> d
i)
  leftUnitor :: forall (i :: (j, k)) (j :: (j, k)) (a :: PRODK jj kk i j).
Obj a -> O I a ~> a
leftUnitor (Prod a ~> b
p c ~> d
q) = (O I b ~> b)
-> (O I d ~> d) -> Prod ('PROD (O I b) (O I d)) ('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 (Obj b -> O I b ~> b
forall (i :: j) (j :: j) (a :: jj 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) (Obj d -> O I d ~> d
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 c ~> d
Obj d
q)
  leftUnitorInv :: forall (i :: (j, k)) (j :: (j, k)) (a :: PRODK jj kk i j).
Obj a -> a ~> O I a
leftUnitorInv (Prod a ~> b
p c ~> d
q) = (b ~> O I b)
-> (d ~> O I d) -> Prod ('PROD b d) ('PROD (O I b) (O I 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 -> b ~> O I b
forall (i :: j) (j :: j) (a :: jj 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) (Obj d -> d ~> O I d
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 c ~> d
Obj d
q)
  rightUnitor :: forall (i :: (j, k)) (j :: (j, k)) (a :: PRODK jj kk i j).
Obj a -> O a I ~> a
rightUnitor (Prod a ~> b
p c ~> d
q) = (O b I ~> b)
-> (O d I ~> d) -> Prod ('PROD (O b I) (O d I)) ('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 (Obj b -> O b I ~> b
forall (i :: j) (j :: j) (a :: jj 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) (Obj d -> O d I ~> d
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 c ~> d
Obj d
q)
  rightUnitorInv :: forall (i :: (j, k)) (j :: (j, k)) (a :: PRODK jj kk i j).
Obj a -> a ~> O a I
rightUnitorInv (Prod a ~> b
p c ~> d
q) = (b ~> O b I)
-> (d ~> O d I) -> Prod ('PROD b d) ('PROD (O b I) (O d 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 -> b ~> O b I
forall (i :: j) (j :: j) (a :: jj 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) (Obj d -> d ~> O d 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 c ~> d
Obj d
q)
  associator :: forall {j1 :: (j, k)} {k1 :: (j, k)} (i :: (j, k)) (j2 :: (j, k))
       (a :: PRODK jj kk i j2) (b :: PRODK jj kk j2 j1)
       (c :: PRODK jj kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Prod a ~> b
p c ~> d
q) (Prod a ~> b
r c ~> d
s) (Prod a ~> b
t c ~> d
u) = (O (O b b) b ~> O b (O b b))
-> (O (O d d) d ~> O d (O d d))
-> Prod
     ('PROD (O (O b b) b) (O (O d d) d))
     ('PROD (O b (O b b)) (O d (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 -> Obj b -> O (O b b) b ~> O b (O b b)
forall {j1 :: j} {k1 :: j} (i :: j) (j2 :: j) (a :: jj i j2)
       (b :: jj j2 j1) (c :: jj 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
r a ~> b
Obj b
t) (Obj d -> Obj d -> Obj d -> O (O d d) d ~> O d (O d d)
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 c ~> d
Obj d
q c ~> d
Obj d
s c ~> d
Obj d
u)
  associatorInv :: forall {j1 :: (j, k)} {k1 :: (j, k)} (i :: (j, k)) (j2 :: (j, k))
       (a :: PRODK jj kk i j2) (b :: PRODK jj kk j2 j1)
       (c :: PRODK jj kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Prod a ~> b
p c ~> d
q) (Prod a ~> b
r c ~> d
s) (Prod a ~> b
t c ~> d
u) = (O b (O b b) ~> O (O b b) b)
-> (O d (O d d) ~> O (O d d) d)
-> Prod
     ('PROD (O b (O b b)) (O d (O d d)))
     ('PROD (O (O b b) b) (O (O d 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 -> Obj b -> O b (O b b) ~> O (O b b) b
forall {j1 :: j} {k1 :: j} (i :: j) (j2 :: j) (a :: jj i j2)
       (b :: jj j2 j1) (c :: jj 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
r a ~> b
Obj b
t) (Obj d -> Obj d -> Obj d -> O d (O d d) ~> O (O d d) d
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 c ~> d
Obj d
q c ~> d
Obj d
s c ~> d
Obj d
u)