{-# 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)