{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
module Proarrow.Category.Equipment where
import Data.Kind (Constraint)
import Prelude (($))
import Proarrow.Category.Bicategory
( Adjunction (..)
, Bicategory (..)
, Ob'
, Ob0'
, associator'
, associatorInv'
, iObj
, leftUnitorInvWith
, leftUnitorWith
, rightUnitorInvWith
, rightUnitorWith
, (==)
, (||)
)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), obj, src, tgt, (//), (\\), type (+->))
import Proarrow.Object (Obj)
infixl 6 |||
infixl 5 ===
type HasCompanions :: forall {c}. CAT c -> CAT c -> Constraint
class (Bicategory hk, Bicategory vk, forall (k :: c). (Ob0 vk k) => Ob0' hk k) => HasCompanions (hk :: CAT c) vk | hk -> vk where
type Companion hk (f :: vk j k) :: hk j k
mapCompanion :: forall {j} {k} (f :: vk j k) g. f ~> g -> Companion hk f ~> Companion hk g
withObCompanion :: forall {j} {k} f r. (Ob (f :: vk j k)) => ((Ob (Companion hk f)) => r) -> r
compToId :: (Ob0 vk k) => Companion hk (I :: vk k k) ~> (I :: hk k k)
compFromId :: (Ob0 vk k) => (I :: hk k k) ~> Companion hk (I :: vk k k)
compToCompose
:: forall {j} {k} (f :: vk j k) g. Obj f -> Obj g -> Companion hk (f `O` g) ~> (Companion hk f `O` Companion hk g)
compFromCompose
:: forall {j} {k} (f :: vk j k) g. Obj f -> Obj g -> (Companion hk f `O` Companion hk g) ~> Companion hk (f `O` g)
class (Adjunction (Companion hk f) (Conjoint hk f)) => ComConAdjunction hk vk f
instance (Adjunction (Companion hk f) (Conjoint hk f)) => ComConAdjunction hk vk f
type Equipment :: forall {c}. CAT c -> CAT c -> Constraint
class (HasCompanions hk vk) => Equipment hk vk | hk -> vk where
{-# MINIMAL mapConjoint, withObConjoint #-}
type Conjoint hk (f :: vk j k) :: hk k j
mapConjoint :: forall {j} {k} (f :: vk j k) g. f ~> g -> Conjoint hk g ~> Conjoint hk f
withObConjoint :: forall {j} {k} f r. (Ob (f :: vk j k)) => ((Ob (Conjoint hk f)) => r) -> r
conjToId :: forall k. (Ob0 vk k) => Conjoint hk (I :: vk k k) ~> (I :: hk k k)
conjToId = Obj I -> O (Companion hk I) (Conjoint hk I) ~> I
forall {j :: c} {k :: c} (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 Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (O (Companion hk I) (Conjoint hk I) ~> I)
-> (Conjoint hk I ~> O (Companion hk I) (Conjoint hk I))
-> Conjoint hk I ~> I
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. (I ~> Companion hk I)
-> (Conjoint hk I ~> Conjoint hk I)
-> Conjoint hk I ~> O (Companion hk I) (Conjoint hk I)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O c b
leftUnitorInvWith I ~> Companion hk I
forall (k :: c). 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 (Obj I -> Conjoint hk I ~> Conjoint hk I
forall {j :: c} {k :: c} (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 Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj)
conjFromId :: forall k. (Ob0 vk k) => (I :: hk k k) ~> Conjoint hk (I :: vk k k)
conjFromId = (Companion hk I ~> I)
-> (Conjoint hk I ~> Conjoint hk I)
-> O (Conjoint hk I) (Companion hk I) ~> Conjoint hk I
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith Companion hk I ~> I
forall (k :: c). 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 ((I ~> I) -> Conjoint hk I ~> Conjoint hk I
forall {j :: c} {k :: c} (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 I ~> I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj) (O (Conjoint hk I) (Companion hk I) ~> Conjoint hk I)
-> (I ~> O (Conjoint hk I) (Companion hk I)) -> I ~> Conjoint hk I
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. (I ~> I) -> I ~> O (Conjoint hk I) (Companion hk I)
forall {j :: c} {k :: c} (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 I ~> I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
conjToCompose
:: forall {j} {k} (f :: vk j k) g. Obj f -> Obj g -> Conjoint hk (f `O` g) ~> (Conjoint hk g `O` Conjoint hk f)
conjToCompose Obj f
f Obj g
g =
( let
fg :: O f g ~> O f g
fg = Obj f
f Obj f -> Obj g -> O f g ~> O f g
forall {i :: c} (j :: c) (k :: c) (a :: vk j k) (b :: vk j k)
(c :: vk i j) (d :: vk 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` Obj g
g
comF :: Companion hk f ~> Companion hk f
comF = 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
forall (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 @hk Obj f
f
comG :: Companion hk g ~> Companion hk g
comG = 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
forall (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 @hk Obj g
g
conFG :: Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG = 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
forall (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 @hk O f g ~> O f g
fg
conF :: Conjoint hk f ~> Conjoint hk f
conF = 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
forall (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 @hk Obj f
f
conG :: Conjoint hk g ~> Conjoint hk g
conG = 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
forall (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 @hk Obj g
g
in
((O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g))
~> I)
-> (O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk g) (Conjoint hk f))
-> O (O (Conjoint hk g) (Conjoint hk f))
(O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g)))
~> O (Conjoint hk g) (Conjoint hk f)
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith ((O f g ~> O f g)
-> O (Companion hk (O f g)) (Conjoint hk (O f g)) ~> I
forall {j :: c} {k :: c} (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 O f g ~> O f g
fg (O (Companion hk (O f g)) (Conjoint hk (O f g)) ~> I)
-> (O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g))
~> O (Companion hk (O f g)) (Conjoint hk (O f g)))
-> O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g))
~> I
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. (Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {j :: c} {j :: c} {k :: c} (f :: vk j k) (g :: vk j j).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {j :: c} {k :: c}
(f :: vk j k) (g :: vk j j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose Obj f
f Obj g
g (O (Companion hk f) (Companion hk g) ~> Companion hk (O f g))
-> (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g))
~> O (Companion hk (O f g)) (Conjoint hk (O f g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG)) (Conjoint hk g ~> Conjoint hk g
conG (Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk g) (Conjoint hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF))
(O (O (Conjoint hk g) (Conjoint hk f))
(O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g)))
~> O (Conjoint hk g) (Conjoint hk f))
-> (Conjoint hk (O f g)
~> O (O (Conjoint hk g) (Conjoint hk f))
(O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g))))
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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 (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk g) (Conjoint hk f))
-> Obj (O (Companion hk f) (Companion hk g))
-> (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> O (O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
(Conjoint hk (O f g))
~> O (O (Conjoint hk g) (Conjoint hk f))
(O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g)))
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' (Conjoint hk g ~> Conjoint hk g
conG (Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk g) (Conjoint hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF) (Companion hk f ~> Companion hk f
comF (Companion hk f ~> Companion hk f)
-> (Companion hk g ~> Companion hk g)
-> Obj (O (Companion hk f) (Companion hk g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk g ~> Companion hk g
comG) Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG
(O (O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
(Conjoint hk (O f g))
~> O (O (Conjoint hk g) (Conjoint hk f))
(O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g))))
-> (Conjoint hk (O f g)
~> O (O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
(Conjoint hk (O f g)))
-> Conjoint hk (O f g)
~> O (O (Conjoint hk g) (Conjoint hk f))
(O (O (Companion hk f) (Companion hk g)) (Conjoint hk (O f g)))
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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 (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk g) (Conjoint hk f))
-> (Companion hk f ~> Companion hk f)
-> (Companion hk g ~> Companion hk g)
-> O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g)
~> O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g))
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' (Conjoint hk g ~> Conjoint hk g
conG (Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk g) (Conjoint hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF) Companion hk f ~> Companion hk f
comF Companion hk g ~> Companion hk g
comG (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g)
~> O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
-> (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> O (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
(Conjoint hk (O f g))
~> O (O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
(Conjoint hk (O f g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG)
(O (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
(Conjoint hk (O f g))
~> O (O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
(Conjoint hk (O f g)))
-> (Conjoint hk (O f g)
~> O (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
(Conjoint hk (O f g)))
-> Conjoint hk (O f g)
~> O (O (O (Conjoint hk g) (Conjoint hk f))
(O (Companion hk f) (Companion hk g)))
(Conjoint hk (O f g))
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. (((Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> (Companion hk f ~> Companion hk f)
-> O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f))
~> O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f)
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv' Conjoint hk g ~> Conjoint hk g
conG Conjoint hk f ~> Conjoint hk f
conF Companion hk f ~> Companion hk f
comF (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f))
~> O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
-> (Companion hk g ~> Companion hk g)
-> O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g)
~> O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk g ~> Companion hk g
comG) (O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g)
~> O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
-> (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> O (O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g))
(Conjoint hk (O f g))
~> O (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
(Conjoint hk (O f g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG)
(O (O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g))
(Conjoint hk (O f g))
~> O (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
(Conjoint hk (O f g)))
-> (Conjoint hk (O f g)
~> O (O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g))
(Conjoint hk (O f g)))
-> Conjoint hk (O f g)
~> O (O (O (O (Conjoint hk g) (Conjoint hk f)) (Companion hk f))
(Companion hk g))
(Conjoint hk (O f g))
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. ((I
~> O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g))
-> (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> Conjoint hk (O f g)
~> O (O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g))
(Conjoint hk (O f g))
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O c b
leftUnitorInvWith (((I ~> O (Conjoint hk f) (Companion hk f))
-> (Conjoint hk g ~> Conjoint hk g)
-> Conjoint hk g
~> O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f))
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O b c
rightUnitorInvWith (Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {j :: c} {k :: c} (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 Obj f
f) Conjoint hk g ~> Conjoint hk g
conG (Conjoint hk g
~> O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
-> (Companion hk g ~> Companion hk g)
-> O (Conjoint hk g) (Companion hk g)
~> O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk g ~> Companion hk g
comG) (O (Conjoint hk g) (Companion hk g)
~> O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g))
-> (I ~> O (Conjoint hk g) (Companion hk g))
-> I
~> O (O (Conjoint hk g) (O (Conjoint hk f) (Companion hk f)))
(Companion hk g)
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. Obj g -> I ~> O (Conjoint hk g) (Companion hk g)
forall {j :: c} {k :: c} (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 Obj g
g) Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG)
)
((Ob0 vk j, Ob0 vk k, Ob f, Ob f) =>
Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f))
-> Obj f
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
((Ob0 vk k, Ob0 vk j, Ob g, Ob g) =>
Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f))
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 g
g
conjFromCompose
:: forall {j} {k} (f :: vk j k) g. Obj f -> Obj g -> (Conjoint hk g `O` Conjoint hk f) ~> Conjoint hk (f `O` g)
conjFromCompose Obj f
f Obj g
g =
( let
fg :: O f g ~> O f g
fg = Obj f
f Obj f -> Obj g -> O f g ~> O f g
forall {i :: c} (j :: c) (k :: c) (a :: vk j k) (b :: vk j k)
(c :: vk i j) (d :: vk 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` Obj g
g
comF :: Companion hk f ~> Companion hk f
comF = 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
forall (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 @hk Obj f
f
comG :: Companion hk g ~> Companion hk g
comG = 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
forall (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 @hk Obj g
g
conFG :: Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG = 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
forall (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 @hk O f g ~> O f g
fg
conF :: Conjoint hk f ~> Conjoint hk f
conF = 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
forall (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 @hk Obj f
f
conG :: Conjoint hk g ~> Conjoint hk g
conG = 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
forall (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 @hk Obj g
g
in
((O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)
~> I)
-> (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> O (Conjoint hk (O f g))
(O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f))
~> Conjoint hk (O f g)
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith (Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {j :: c} {k :: c} (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 Obj f
f (O (Companion hk f) (Conjoint hk f) ~> I)
-> (O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)
~> O (Companion hk f) (Conjoint hk f))
-> O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)
~> I
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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 (Companion hk g) (Conjoint hk g) ~> I)
-> (Companion hk f ~> Companion hk f)
-> O (Companion hk f) (O (Companion hk g) (Conjoint hk g))
~> Companion hk f
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith (Obj g -> O (Companion hk g) (Conjoint hk g) ~> I
forall {j :: c} {k :: c} (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 Obj g
g) Companion hk f ~> Companion hk f
comF (O (Companion hk f) (O (Companion hk g) (Conjoint hk g))
~> Companion hk f)
-> (Conjoint hk f ~> Conjoint hk f)
-> O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)
~> O (Companion hk f) (Conjoint hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF)) Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG)
(O (Conjoint hk (O f g))
(O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f))
~> Conjoint hk (O f g))
-> (O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)))
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
forall (b :: hk k j) (c :: hk k j) (a :: hk 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
. (Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> (O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f))
~> O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f))
-> O (Conjoint hk (O f g))
(O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f)))
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` (((Companion hk f ~> Companion hk f)
-> (Companion hk g ~> Companion hk g)
-> (Conjoint hk g ~> Conjoint hk g)
-> O (O (Companion hk f) (Companion hk g)) (Conjoint hk g)
~> O (Companion hk f) (O (Companion hk g) (Conjoint hk g))
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' Companion hk f ~> Companion hk f
comF Companion hk g ~> Companion hk g
comG Conjoint hk g ~> Conjoint hk g
conG (O (O (Companion hk f) (Companion hk g)) (Conjoint hk g)
~> O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
-> (Conjoint hk f ~> Conjoint hk f)
-> O (O (O (Companion hk f) (Companion hk g)) (Conjoint hk g))
(Conjoint hk f)
~> O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF) (O (O (O (Companion hk f) (Companion hk g)) (Conjoint hk g))
(Conjoint hk f)
~> O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f))
-> (O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f))
~> O (O (O (Companion hk f) (Companion hk g)) (Conjoint hk g))
(Conjoint hk f))
-> O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f))
~> O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. Obj (O (Companion hk f) (Companion hk g))
-> (Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f))
~> O (O (O (Companion hk f) (Companion hk g)) (Conjoint hk g))
(Conjoint hk f)
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv' (Companion hk f ~> Companion hk f
comF (Companion hk f ~> Companion hk f)
-> (Companion hk g ~> Companion hk g)
-> Obj (O (Companion hk f) (Companion hk g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk g ~> Companion hk g
comG) Conjoint hk g ~> Conjoint hk g
conG Conjoint hk f ~> Conjoint hk f
conF))
(O (Conjoint hk (O f g))
(O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f)))
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f)))
-> (O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f))))
-> O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (O (Companion hk g) (Conjoint hk g)))
(Conjoint hk f))
forall (b :: hk k j) (c :: hk k j) (a :: hk 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
. (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> Obj (O (Companion hk f) (Companion hk g))
-> Obj (O (Conjoint hk g) (Conjoint hk f))
-> O (O (Conjoint hk (O f g))
(O (Companion hk f) (Companion hk g)))
(O (Conjoint hk g) (Conjoint hk f))
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f)))
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG (Companion hk f ~> Companion hk f
comF (Companion hk f ~> Companion hk f)
-> (Companion hk g ~> Companion hk g)
-> Obj (O (Companion hk f) (Companion hk g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk g ~> Companion hk g
comG) (Conjoint hk g ~> Conjoint hk g
conG (Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> Obj (O (Conjoint hk g) (Conjoint hk f))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF)
(O (O (Conjoint hk (O f g)) (O (Companion hk f) (Companion hk g)))
(O (Conjoint hk g) (Conjoint hk f))
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f))))
-> (O (Conjoint hk g) (Conjoint hk f)
~> O (O (Conjoint hk (O f g))
(O (Companion hk f) (Companion hk g)))
(O (Conjoint hk g) (Conjoint hk f)))
-> O (Conjoint hk g) (Conjoint hk f)
~> O (Conjoint hk (O f g))
(O (O (Companion hk f) (Companion hk g))
(O (Conjoint hk g) (Conjoint hk f)))
forall (b :: hk k j) (c :: hk k j) (a :: hk 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
. ((I
~> O (Conjoint hk (O f g)) (O (Companion hk f) (Companion hk g)))
-> Obj (O (Conjoint hk g) (Conjoint hk f))
-> O (Conjoint hk g) (Conjoint hk f)
~> O (O (Conjoint hk (O f g))
(O (Companion hk f) (Companion hk g)))
(O (Conjoint hk g) (Conjoint hk f))
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O c b
leftUnitorInvWith ((Conjoint hk (O f g) ~> Conjoint hk (O f g)
conFG (Conjoint hk (O f g) ~> Conjoint hk (O f g))
-> (Companion hk (O f g) ~> O (Companion hk f) (Companion hk g))
-> O (Conjoint hk (O f g)) (Companion hk (O f g))
~> O (Conjoint hk (O f g)) (O (Companion hk f) (Companion hk g))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {i :: c} {j :: c} {k :: c} (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 Obj f
f Obj g
g) (O (Conjoint hk (O f g)) (Companion hk (O f g))
~> O (Conjoint hk (O f g)) (O (Companion hk f) (Companion hk g)))
-> (I ~> O (Conjoint hk (O f g)) (Companion hk (O f g)))
-> I
~> O (Conjoint hk (O f g)) (O (Companion hk f) (Companion hk g))
forall (b :: hk j j) (c :: hk j j) (a :: hk j 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 f g ~> O f g)
-> I ~> O (Conjoint hk (O f g)) (Companion hk (O f g))
forall {j :: c} {k :: c} (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 O f g ~> O f g
fg) (Conjoint hk g ~> Conjoint hk g
conG (Conjoint hk g ~> Conjoint hk g)
-> (Conjoint hk f ~> Conjoint hk f)
-> Obj (O (Conjoint hk g) (Conjoint hk f))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF))
)
((Ob0 vk j, Ob0 vk k, Ob f, Ob f) =>
O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g))
-> Obj f
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
((Ob0 vk j, Ob0 vk j, Ob g, Ob g) =>
O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g))
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 g
g
comConUnit :: forall {j} {k} (f :: vk j k). Obj f -> I ~> Conjoint hk f `O` Companion hk f
default comConUnit
:: forall {j} {k} (f :: vk j k). (((Ob f) => ComConAdjunction hk vk f)) => Obj f -> I ~> Conjoint hk f `O` Companion hk f
comConUnit Obj f
f = forall (l :: hk j k) (r :: hk k j). 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 @(Companion hk f) @(Conjoint hk f) ((Ob0 vk j, Ob0 vk k, Ob f, Ob f) =>
I ~> O (Conjoint hk f) (Companion hk f))
-> Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
comConCounit :: forall {j} {k} (f :: vk j k). Obj f -> Companion hk f `O` Conjoint hk f ~> I
default comConCounit
:: forall {j} {k} (f :: vk j k). ((Ob f) => ComConAdjunction hk vk f) => Obj f -> Companion hk f `O` Conjoint hk f ~> I
comConCounit Obj f
f = forall (l :: hk j k) (r :: hk k j). 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 @(Companion hk f) @(Conjoint hk f) ((Ob0 vk j, Ob0 vk k, Ob f, Ob f) =>
O (Companion hk f) (Conjoint hk f) ~> I)
-> Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
type Cart (p :: hk h j) (f :: vk h i) (g :: vk j k) = Companion hk g `O` p `O` Conjoint hk f
type SQ' (hk :: CAT c) (vk :: CAT c) h i j k = (hk k i, vk j k) +-> (hk j h, vk h i)
type SQ (hk :: CAT c) (vk :: CAT c) = forall {h} {i} {j} {k}. SQ' hk vk h i j k
type Sq :: forall {c} {hk :: CAT c} {vk :: CAT c}. SQ hk vk
data Sq pf qg where
Sq
:: forall {hk} {vk} {h} {i} {j} {k} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k)
. (Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g)
=> Companion hk f `O` p ~> q `O` Companion hk g
-> Sq '(p, f) '(q, g)
instance (HasCompanions hk vk, Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k) => Profunctor (Sq :: SQ' hk vk h i j k) where
dimap :: forall (c :: (hk j h, vk h i)) (a :: (hk j h, vk h i))
(b :: (hk k i, vk j k)) (d :: (hk k i, vk j k)).
(c ~> a) -> (b ~> d) -> Sq a b -> Sq c d
dimap (a1 ~> b1
p :**: a2 ~> b2
f) (a1 ~> b1
q :**: a2 ~> b2
g) (Sq O (Companion hk f) p ~> O q (Companion hk g)
sq) = (O (Companion hk a2) a1 ~> O b1 (Companion hk b2))
-> Sq '(a1, a2) '(b1, b2)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq ((a2 ~> b2) -> Companion hk a2 ~> Companion hk b2
forall {j :: c} {k :: c} (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 a2 ~> b2
f (Companion hk a2 ~> Companion hk b2)
-> (a1 ~> b1) -> O (Companion hk a2) a1 ~> O (Companion hk b2) b1
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
|| a1 ~> b1
p (O (Companion hk a2) a1 ~> O (Companion hk b2) b1)
-> (O (Companion hk b2) b1 ~> O a1 (Companion hk a2))
-> O (Companion hk a2) a1 ~> O a1 (Companion hk a2)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== O (Companion hk b2) b1 ~> O a1 (Companion hk a2)
O (Companion hk f) p ~> O q (Companion hk g)
sq (O (Companion hk a2) a1 ~> O a1 (Companion hk a2))
-> (O a1 (Companion hk a2) ~> O b1 (Companion hk b2))
-> O (Companion hk a2) a1 ~> O b1 (Companion hk b2)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== a1 ~> b1
q (a1 ~> b1)
-> (Companion hk a2 ~> Companion hk b2)
-> O a1 (Companion hk a2) ~> O b1 (Companion hk b2)
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
|| (a2 ~> b2) -> Companion hk a2 ~> Companion hk b2
forall {j :: c} {k :: c} (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 a2 ~> b2
g) ((Ob0 hk j, Ob0 hk h, Ob a1, Ob b1) => Sq c d)
-> (a1 ~> b1) -> Sq c d
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ a1 ~> b1
p ((Ob0 hk k, Ob0 hk i, Ob a1, Ob b1) => Sq c d)
-> (a1 ~> b1) -> Sq c d
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ a1 ~> b1
q ((Ob0 vk h, Ob0 vk i, Ob a2, Ob b2) => Sq c d)
-> (a2 ~> b2) -> Sq c d
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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
\\\ a2 ~> b2
f ((Ob0 vk j, Ob0 vk k, Ob a2, Ob b2) => Sq c d)
-> (a2 ~> b2) -> Sq c d
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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
\\\ a2 ~> b2
g
(Ob a, Ob b) => r
r \\ :: forall (a :: (hk j h, vk h i)) (b :: (hk k i, vk j k)) r.
((Ob a, Ob b) => r) -> Sq a b -> r
\\ Sq O (Companion hk f) p ~> O q (Companion hk g)
sq = r
(Ob (O (Companion hk f) p), Ob (O q (Companion hk g))) => r
(Ob a, Ob b) => r
r ((Ob (O (Companion hk f) p), Ob (O q (Companion hk g))) => r)
-> (O (Companion hk f) p ~> O q (Companion hk g)) -> r
forall (a :: hk j i) (b :: hk j i) 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
\\ O (Companion hk f) p ~> O q (Companion hk g)
sq
object :: (HasCompanions hk vk, Ob0 vk k) => Sq '(I :: hk k k, I :: vk k k) '(I, I)
object :: forall {s} (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(I, I) '(I, I)
object = (I ~> I) -> Sq '(I, I) '(I, I)
forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {j :: s}
{k :: s} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
hArr I ~> I
forall (a :: hk k k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
hArr
:: forall {hk} {vk} {j} {k} (p :: hk j k) q
. (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
=> p ~> q
-> Sq '(p, I :: vk k k) '(q, I :: vk j j)
hArr :: forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {j :: s}
{k :: s} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
hArr p ~> q
n =
(O (Companion hk I) p ~> O q (Companion hk I))
-> Sq '(p, I) '(q, I)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq ((I ~> Companion hk I) -> (q ~> q) -> q ~> O q (Companion hk I)
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O b c
rightUnitorInvWith (forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
forall (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId @hk @vk) ((p ~> q) -> q ~> q
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p ~> q
n) (q ~> O q (Companion hk I))
-> (O (Companion hk I) p ~> q)
-> O (Companion hk I) p ~> O q (Companion hk I)
forall (b :: hk j k) (c :: hk j k) (a :: hk j 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
. p ~> q
n (p ~> q)
-> (O (Companion hk I) p ~> p) -> O (Companion hk I) p ~> q
forall (b :: hk j k) (c :: hk j k) (a :: hk j 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
. (Companion hk I ~> I) -> (p ~> p) -> O (Companion hk I) p ~> p
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O c a ~> b
leftUnitorWith (forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
forall (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId @hk @vk) ((p ~> q) -> p ~> p
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p ~> q
n))
((Ob p, Ob q) => Sq '(p, I) '(q, I))
-> (p ~> q) -> Sq '(p, I) '(q, I)
forall (a :: hk j k) (b :: hk j 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
\\ p ~> q
n
hId :: (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (p :: hk k j)) => Sq '(p, I :: vk j j) '(p, I :: vk k k)
hId :: forall {s} (hk :: CAT s) (vk :: CAT s) (j :: s) (k :: s)
(p :: hk k j).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) =>
Sq '(p, I) '(p, I)
hId = (p ~> p) -> Sq '(p, I) '(p, I)
forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {j :: s}
{k :: s} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
hArr p ~> p
forall (a :: hk k j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
compId
:: forall {hk} {vk} {j} {k} f
. (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
=> Sq '(Companion hk f, I :: vk k k) '(Companion hk f, I :: vk j j)
compId :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Companion hk f, I) '(Companion hk f, I)
compId = (Companion hk f ~> Companion hk f)
-> Sq '(Companion hk f, I) '(Companion hk f, I)
forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {j :: s}
{k :: s} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
hArr (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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f))
conjId
:: forall {hk} {vk} {j} {k} f
. (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
=> Sq '(Conjoint hk f, I :: vk j j) '(Conjoint hk f, I :: vk k k)
conjId :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f, I) '(Conjoint hk f, I)
conjId = (Conjoint hk f ~> Conjoint hk f)
-> Sq '(Conjoint hk f, I) '(Conjoint hk f, I)
forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {j :: s}
{k :: s} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
hArr (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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f))
vArr
:: forall {hk} {vk} {j} {k} (f :: vk j k) g
. (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
=> f ~> g
-> Sq '(I :: hk j j, f) '(I :: hk k k, g)
vArr :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(I, f) '(I, g)
vArr f ~> g
n =
let n' :: Companion hk f ~> Companion hk g
n' = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk @vk f ~> g
n
in (O (Companion hk f) I ~> O I (Companion hk g))
-> Sq '(I, f) '(I, g)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (Companion hk g ~> O I (Companion hk g)
forall {i :: s} {j :: s} (a :: hk i j).
(Ob0 hk i, Ob0 hk 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 (Companion hk g ~> O I (Companion hk g))
-> (O (Companion hk f) I ~> Companion hk g)
-> O (Companion hk f) I ~> O I (Companion hk g)
forall (b :: hk j k) (c :: hk j k) (a :: hk j 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
. Companion hk f ~> Companion hk g
n' (Companion hk f ~> Companion hk g)
-> (O (Companion hk f) I ~> Companion hk f)
-> O (Companion hk f) I ~> Companion hk g
forall (b :: hk j k) (c :: hk j k) (a :: hk j 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 (Companion hk f) I ~> Companion hk f
forall {i :: s} {j :: s} (a :: hk i j).
(Ob0 hk i, Ob0 hk 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 f, Ob g) => Sq '(I, f) '(I, g))
-> (f ~> g) -> Sq '(I, f) '(I, g)
forall (a :: vk j k) (b :: vk j 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
\\ f ~> g
n ((Ob (Companion hk f), Ob (Companion hk g)) => Sq '(I, f) '(I, g))
-> (Companion hk f ~> Companion hk g) -> Sq '(I, f) '(I, g)
forall (a :: hk j k) (b :: hk j 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
\\ Companion hk f ~> Companion hk g
n'
vId
:: forall {hk} {vk} {j} {k} (f :: vk j k)
. (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
=> Sq '(I :: hk j j, f) '(I :: hk k k, f)
vId :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(I, f) '(I, f)
vId = (f ~> f) -> Sq '(I, f) '(I, f)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(I, f) '(I, g)
vArr f ~> f
forall (a :: vk j k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
(|||)
:: forall {hk} {vk} {h} {l} {m} (p :: hk m l) q r (d :: vk l h) e f g
. (HasCompanions hk vk)
=> Sq '(p, d) '(q, e)
-> Sq '(q, f) '(r, g)
-> Sq '(p, f `O` d) '(r, g `O` e)
Sq O (Companion hk f) p ~> O q (Companion hk g)
sqL ||| :: forall {c} {j :: c} {k :: c} {i :: c} {hk :: c -> c -> Type}
{vk :: c -> c -> Type} {h :: c} {l :: c} {m :: c} (p :: hk m l)
(q :: hk j h) (r :: hk k i) (d :: vk l h) (e :: vk m j)
(f :: vk h i) (g :: vk j k).
HasCompanions hk vk =>
Sq '(p, d) '(q, e)
-> Sq '(q, f) '(r, g) -> Sq '(p, O f d) '(r, O g e)
||| Sq O (Companion hk f) p ~> O q (Companion hk g)
sqR =
( let d :: Obj d
d = forall (a :: vk l h). (CategoryOf (vk l h), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d
e :: Obj e
e = forall (a :: vk m j). (CategoryOf (vk m j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @e
f :: Obj f
f = forall (a :: vk h i). (CategoryOf (vk h i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f
g :: Obj g
g = forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g
dc :: Companion hk d ~> Companion hk d
dc = 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
forall (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 @hk Obj d
d
ec :: Companion hk e ~> Companion hk e
ec = 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
forall (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 @hk Obj e
e
fc :: Companion hk f ~> Companion hk f
fc = 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
forall (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 @hk Obj f
f
gc :: Companion hk g ~> Companion hk g
gc = 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
forall (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 @hk Obj g
g
in 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 c) {i :: c} {j :: c} {k :: c} (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 @vk @g @e ((Ob (O g e) => Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e))
-> (Ob (O g e) => Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e)
forall a b. (a -> b) -> a -> b
$
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 c) {i :: c} {j :: c} {k :: c} (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 @vk @f @d ((Ob (O f d) => Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e))
-> (Ob (O f d) => Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e)
forall a b. (a -> b) -> a -> b
$
Companion hk d ~> Companion hk d
dc (Companion hk d ~> Companion hk d)
-> ((Ob (Companion hk d), Ob (Companion hk d)) =>
Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
Companion hk e ~> Companion hk e
ec (Companion hk e ~> Companion hk e)
-> ((Ob (Companion hk e), Ob (Companion hk e)) =>
Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
Companion hk f ~> Companion hk f
fc (Companion hk f ~> Companion hk f)
-> ((Ob (Companion hk f), Ob (Companion hk f)) =>
Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
Companion hk g ~> Companion hk g
gc (Companion hk g ~> Companion hk g)
-> ((Ob (Companion hk g), Ob (Companion hk g)) =>
Sq '(p, O f d) '(r, O g e))
-> Sq '(p, O f d) '(r, O g e)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
(O (Companion hk (O f d)) p ~> O r (Companion hk (O g e)))
-> Sq '(p, O f d) '(r, O g e)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq ((O (Companion hk (O f d)) p ~> O r (Companion hk (O g e)))
-> Sq '(p, O f d) '(r, O g e))
-> (O (Companion hk (O f d)) p ~> O r (Companion hk (O g e)))
-> Sq '(p, O f d) '(r, O g e)
forall a b. (a -> b) -> a -> b
$
(forall (a :: hk k i). (CategoryOf (hk k i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r
-> (O (Companion hk g) (Companion hk e) ~> Companion hk (O g e))
-> O r (O (Companion hk g) (Companion hk e))
~> O r (Companion hk (O g e))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Obj g
-> Obj e
-> O (Companion hk g) (Companion hk e) ~> Companion hk (O g e)
forall {j :: c} {j :: c} {k :: c} (f :: vk j k) (g :: vk j j).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {j :: c} {k :: c}
(f :: vk j k) (g :: vk j j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose Obj g
g Obj e
e)
(O r (O (Companion hk g) (Companion hk e))
~> O r (Companion hk (O g e)))
-> (O (Companion hk (O f d)) p
~> O r (O (Companion hk g) (Companion hk e)))
-> O (Companion hk (O f d)) p ~> O r (Companion hk (O g e))
forall (b :: hk m i) (c :: hk m i) (a :: hk m i).
(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 {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 c) {h :: c} {i :: c} {j :: c} {k :: c}
(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 @_ @r @(Companion hk g) @(Companion hk e)
(O (O r (Companion hk g)) (Companion hk e)
~> O r (O (Companion hk g) (Companion hk e)))
-> (O (Companion hk (O f d)) p
~> O (O r (Companion hk g)) (Companion hk e))
-> O (Companion hk (O f d)) p
~> O r (O (Companion hk g) (Companion hk e))
forall (b :: hk m i) (c :: hk m i) (a :: hk m i).
(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 (Companion hk f) q ~> O r (Companion hk g)
O (Companion hk f) p ~> O q (Companion hk g)
sqR (O (Companion hk f) q ~> O r (Companion hk g))
-> (Companion hk e ~> Companion hk e)
-> O (O (Companion hk f) q) (Companion hk e)
~> O (O r (Companion hk g)) (Companion hk e)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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 :: hk m j). (CategoryOf (hk m j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Companion hk e))
(O (O (Companion hk f) q) (Companion hk e)
~> O (O r (Companion hk g)) (Companion hk e))
-> (O (Companion hk (O f d)) p
~> O (O (Companion hk f) q) (Companion hk e))
-> O (Companion hk (O f d)) p
~> O (O r (Companion hk g)) (Companion hk e)
forall (b :: hk m i) (c :: hk m i) (a :: hk m i).
(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 {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 c) {h :: c} {i :: c} {j :: c} {k :: c}
(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 @_ @(Companion hk f) @q @(Companion hk e)
(O (Companion hk f) (O q (Companion hk e))
~> O (O (Companion hk f) q) (Companion hk e))
-> (O (Companion hk (O f d)) p
~> O (Companion hk f) (O q (Companion hk e)))
-> O (Companion hk (O f d)) p
~> O (O (Companion hk f) q) (Companion hk e)
forall (b :: hk m i) (c :: hk m i) (a :: hk m i).
(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 :: hk h i). (CategoryOf (hk h i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Companion hk f) (Companion hk f ~> Companion hk f)
-> (O (Companion hk d) p ~> O q (Companion hk e))
-> O (Companion hk f) (O (Companion hk d) p)
~> O (Companion hk f) (O q (Companion hk e))
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` O (Companion hk d) p ~> O q (Companion hk e)
O (Companion hk f) p ~> O q (Companion hk g)
sqL)
(O (Companion hk f) (O (Companion hk d) p)
~> O (Companion hk f) (O q (Companion hk e)))
-> (O (Companion hk (O f d)) p
~> O (Companion hk f) (O (Companion hk d) p))
-> O (Companion hk (O f d)) p
~> O (Companion hk f) (O q (Companion hk e))
forall (b :: hk m i) (c :: hk m i) (a :: hk m i).
(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 {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 c) {h :: c} {i :: c} {j :: c} {k :: c}
(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 @_ @(Companion hk f) @(Companion hk d) @p
(O (O (Companion hk f) (Companion hk d)) p
~> O (Companion hk f) (O (Companion hk d) p))
-> (O (Companion hk (O f d)) p
~> O (O (Companion hk f) (Companion hk d)) p)
-> O (Companion hk (O f d)) p
~> O (Companion hk f) (O (Companion hk d) p)
forall (b :: hk m i) (c :: hk m i) (a :: hk m i).
(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
. (Obj f
-> Obj d
-> Companion hk (O f d) ~> O (Companion hk f) (Companion hk d)
forall {i :: c} {j :: c} {k :: c} (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 Obj f
f Obj d
d (Companion hk (O f d) ~> O (Companion hk f) (Companion hk d))
-> (p ~> p)
-> O (Companion hk (O f d)) p
~> O (O (Companion hk f) (Companion hk d)) p
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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 :: hk m l). (CategoryOf (hk m l), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p)
)
((Ob0 hk m, Ob0 hk h, Ob (O (Companion hk d) p),
Ob (O q (Companion hk e))) =>
Sq '(p, O f d) '(r, O g e))
-> (O (Companion hk d) p ~> O q (Companion hk e))
-> Sq '(p, O f d) '(r, O g e)
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Companion hk d) p ~> O q (Companion hk e)
O (Companion hk f) p ~> O q (Companion hk g)
sqL
((Ob0 hk j, Ob0 hk i, Ob (O (Companion hk f) q),
Ob (O r (Companion hk g))) =>
Sq '(p, O f d) '(r, O g e))
-> (O (Companion hk f) q ~> O r (Companion hk g))
-> Sq '(p, O f d) '(r, O g e)
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Companion hk f) q ~> O r (Companion hk g)
O (Companion hk f) p ~> O q (Companion hk g)
sqR
(===)
:: forall {hk} {vk} {h} {i} {j} {l} (p :: hk l j) q r s (e :: vk h i) f g
. (HasCompanions hk vk)
=> Sq '(r, e) '(s, f)
-> Sq '(p, f) '(q, g)
-> Sq '(r `O` p, e) '(s `O` q, g)
Sq O (Companion hk f) p ~> O q (Companion hk g)
sqL === :: forall {s} {k :: s} {j :: s} {hk :: s -> s -> Type}
{vk :: s -> s -> Type} {h :: s} {i :: s} {j :: s} {l :: s}
(p :: hk l j) (q :: hk k j) (r :: hk j h) (s :: hk j i)
(e :: vk h i) (f :: vk j j) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s q, g)
=== Sq O (Companion hk f) p ~> O q (Companion hk g)
sqR =
( let p :: Obj p
p = forall (a :: hk l j). (CategoryOf (hk l j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p
s :: Obj s
s = forall (a :: hk j i). (CategoryOf (hk j i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s
ec :: Companion hk e ~> Companion hk e
ec = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk h i). (CategoryOf (vk h i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @e)
fc :: Companion hk f ~> Companion hk f
fc = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk j j). (CategoryOf (vk j j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f)
gc :: Companion hk g ~> Companion hk g
gc = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk l k). (CategoryOf (vk l k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g)
in 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 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
withOb2 @hk @r @p ((Ob (O r p) => Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g))
-> (Ob (O r p) => Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g)
forall a b. (a -> b) -> a -> b
$
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 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
withOb2 @hk @s @q ((Ob (O s q) => Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g))
-> (Ob (O s q) => Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g)
forall a b. (a -> b) -> a -> b
$
Companion hk e ~> Companion hk e
ec (Companion hk e ~> Companion hk e)
-> ((Ob (Companion hk e), Ob (Companion hk e)) =>
Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
Companion hk f ~> Companion hk f
fc (Companion hk f ~> Companion hk f)
-> ((Ob (Companion hk f), Ob (Companion hk f)) =>
Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
Companion hk g ~> Companion hk g
gc (Companion hk g ~> Companion hk g)
-> ((Ob (Companion hk g), Ob (Companion hk g)) =>
Sq '(O r p, e) '(O s q, g))
-> Sq '(O r p, e) '(O s q, g)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
(O (Companion hk e) (O r p) ~> O (O s q) (Companion hk g))
-> Sq '(O r p, e) '(O s q, g)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq ((O (Companion hk e) (O r p) ~> O (O s q) (Companion hk g))
-> Sq '(O r p, e) '(O s q, g))
-> (O (Companion hk e) (O r p) ~> O (O s q) (Companion hk g))
-> Sq '(O r p, e) '(O s q, g)
forall a b. (a -> b) -> a -> b
$
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 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
associatorInv @_ @s @q @(Companion hk g)
(O s (O q (Companion hk g)) ~> O (O s q) (Companion hk g))
-> (O (Companion hk e) (O r p) ~> O s (O q (Companion hk g)))
-> O (Companion hk e) (O r p) ~> O (O s q) (Companion hk g)
forall (b :: hk l i) (c :: hk l i) (a :: hk l i).
(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
. (Obj s
s Obj s
-> (O (Companion hk f) p ~> O q (Companion hk g))
-> O s (O (Companion hk f) p) ~> O s (O q (Companion hk g))
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` O (Companion hk f) p ~> O q (Companion hk g)
O (Companion hk f) p ~> O q (Companion hk g)
sqR)
(O s (O (Companion hk f) p) ~> O s (O q (Companion hk g)))
-> (O (Companion hk e) (O r p) ~> O s (O (Companion hk f) p))
-> O (Companion hk e) (O r p) ~> O s (O q (Companion hk g))
forall (b :: hk l i) (c :: hk l i) (a :: hk l i).
(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 {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 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)
associator @_ @s @(Companion hk f) @p
(O (O s (Companion hk f)) p ~> O s (O (Companion hk f) p))
-> (O (Companion hk e) (O r p) ~> O (O s (Companion hk f)) p)
-> O (Companion hk e) (O r p) ~> O s (O (Companion hk f) p)
forall (b :: hk l i) (c :: hk l i) (a :: hk l i).
(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 (Companion hk e) r ~> O s (Companion hk f)
O (Companion hk f) p ~> O q (Companion hk g)
sqL (O (Companion hk e) r ~> O s (Companion hk f))
-> Obj p
-> O (O (Companion hk e) r) p ~> O (O s (Companion hk f)) p
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Obj p
p)
(O (O (Companion hk e) r) p ~> O (O s (Companion hk f)) p)
-> (O (Companion hk e) (O r p) ~> O (O (Companion hk e) r) p)
-> O (Companion hk e) (O r p) ~> O (O s (Companion hk f)) p
forall (b :: hk l i) (c :: hk l i) (a :: hk l i).
(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 {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 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
associatorInv @_ @(Companion hk e) @r @p
)
((Ob0 hk j, Ob0 hk i, Ob (O (Companion hk e) r),
Ob (O s (Companion hk f))) =>
Sq '(O r p, e) '(O s q, g))
-> (O (Companion hk e) r ~> O s (Companion hk f))
-> Sq '(O r p, e) '(O s q, g)
forall (i :: s) (j :: s) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Companion hk e) r ~> O s (Companion hk f)
O (Companion hk f) p ~> O q (Companion hk g)
sqL
((Ob0 hk l, Ob0 hk j, Ob (O (Companion hk f) p),
Ob (O q (Companion hk g))) =>
Sq '(O r p, e) '(O s q, g))
-> (O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(O r p, e) '(O s q, g)
forall (i :: s) (j :: s) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Companion hk f) p ~> O q (Companion hk g)
O (Companion hk f) p ~> O q (Companion hk g)
sqR
toRight
:: forall {hk} {vk} {j} {k} f
. (HasCompanions hk vk, Ob' (f :: vk j k))
=> Sq '(I :: hk j j, f) '(Companion hk f, I :: vk j j)
toRight :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(I, f) '(Companion hk f, I)
toRight = let comp :: Companion hk f ~> Companion hk f
comp = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk @vk (forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f) in (O (Companion hk f) I ~> O (Companion hk f) (Companion hk I))
-> Sq '(I, f) '(Companion hk f, I)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (Companion hk f ~> Companion hk f
comp (Companion hk f ~> Companion hk f)
-> (I ~> Companion hk I)
-> O (Companion hk f) I ~> O (Companion hk f) (Companion hk I)
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` I ~> Companion hk I
forall (k :: s). 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) ((Ob (Companion hk f), Ob (Companion hk f)) =>
Sq '(I, f) '(Companion hk f, I))
-> (Companion hk f ~> Companion hk f)
-> Sq '(I, f) '(Companion hk f, I)
forall (a :: hk j k) (b :: hk j 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
\\ Companion hk f ~> Companion hk f
comp
fromLeft
:: forall {hk} {vk} {j} {k} f
. (HasCompanions hk vk, Ob' (f :: vk j k))
=> Sq '(Companion hk f, I :: vk k k) '(I :: hk k k, f)
fromLeft :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f, I) '(I, f)
fromLeft = let comp :: Companion hk f ~> Companion hk f
comp = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk @vk (forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f) in (O (Companion hk I) (Companion hk f) ~> O I (Companion hk f))
-> Sq '(Companion hk f, I) '(I, f)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (Companion hk I ~> I
forall (k :: s). 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 (Companion hk I ~> I)
-> (Companion hk f ~> Companion hk f)
-> O (Companion hk I) (Companion hk f) ~> O I (Companion hk f)
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk f ~> Companion hk f
comp) ((Ob (Companion hk f), Ob (Companion hk f)) =>
Sq '(Companion hk f, I) '(I, f))
-> (Companion hk f ~> Companion hk f)
-> Sq '(Companion hk f, I) '(I, f)
forall (a :: hk j k) (b :: hk j 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
\\ Companion hk f ~> Companion hk f
comp
fromRight
:: forall {hk} {vk} {j} {k} (f :: vk j k)
. (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f)
=> Sq '(I :: hk j j, I :: vk j j) '(Conjoint hk f, f)
fromRight :: forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
(f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(I, I) '(Conjoint hk f, f)
fromRight =
let f :: Obj f
f = forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f
in (O (Companion hk I) I ~> O (Conjoint hk f) (Companion hk f))
-> Sq '(I, I) '(Conjoint hk f, f)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (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)
forall (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 @hk @vk Obj f
f (I ~> O (Conjoint hk f) (Companion hk f))
-> (O (Companion hk I) I ~> I)
-> O (Companion hk I) I ~> O (Conjoint hk f) (Companion hk f)
forall (b :: hk j j) (c :: hk j j) (a :: hk j 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
. (Companion hk I ~> I) -> (I ~> I) -> O (Companion hk I) I ~> I
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O c a ~> b
leftUnitorWith (forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
forall (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId @hk @vk) I ~> I
forall (a :: hk j j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
((Ob0 hk k, Ob0 hk j, Ob (Conjoint hk f), Ob (Conjoint hk f)) =>
Sq '(I, I) '(Conjoint hk f, f))
-> (Conjoint hk f ~> Conjoint hk f)
-> Sq '(I, I) '(Conjoint hk f, f)
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ 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
forall (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 @hk @vk Obj f
f
toLeft
:: forall {hk} {vk} {j} {k} (f :: vk j k)
. (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
=> Sq '(Conjoint hk f, f) '(I :: hk k k, I :: vk k k)
toLeft :: forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
(f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f, f) '(I, I)
toLeft =
let f :: Obj f
f = forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f
in (O (Companion hk f) (Conjoint hk f) ~> O I (Companion hk I))
-> Sq '(Conjoint hk f, f) '(I, I)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {h :: c}
{i :: c} {j :: c} {k :: c} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq ((I ~> Companion hk I) -> (I ~> I) -> I ~> O I (Companion hk I)
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O b c
rightUnitorInvWith (forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
forall (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId @hk @vk) I ~> I
forall (a :: hk k k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (I ~> O I (Companion hk I))
-> (O (Companion hk f) (Conjoint hk f) ~> I)
-> O (Companion hk f) (Conjoint hk f) ~> O I (Companion hk I)
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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 {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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit @hk @vk Obj f
f)
((Ob0 hk k, Ob0 hk j, Ob (Conjoint hk f), Ob (Conjoint hk f)) =>
Sq '(Conjoint hk f, f) '(I, I))
-> (Conjoint hk f ~> Conjoint hk f)
-> Sq '(Conjoint hk f, f) '(I, I)
forall (i :: s) (j :: s) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk @vk Obj f
f
flipCompanion
:: forall {j} {k} hk vk (f :: vk j k) p q
. (Equipment hk vk, Ob p)
=> Obj f
-> Companion hk f `O` p ~> q
-> p ~> Conjoint hk f `O` q
flipCompanion :: forall {s} {i :: s} {j :: s} {k :: s} (hk :: CAT s) (vk :: CAT s)
(f :: vk j k) (p :: hk i j) (q :: hk i k).
(Equipment hk vk, Ob p) =>
Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q
flipCompanion Obj f
f O (Companion hk f) p ~> q
n =
let comF :: Companion hk f ~> Companion hk f
comF = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj f
f; conF :: Conjoint hk f ~> Conjoint hk f
conF = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj f
f
in ((Conjoint hk f ~> Conjoint hk f
conF (Conjoint hk f ~> Conjoint hk f)
-> (O (Companion hk f) p ~> q)
-> O (Conjoint hk f) (O (Companion hk f) p) ~> O (Conjoint hk f) q
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` O (Companion hk f) p ~> q
n) (O (Conjoint hk f) (O (Companion hk f) p) ~> O (Conjoint hk f) q)
-> (p ~> O (Conjoint hk f) (O (Companion hk f) p))
-> p ~> O (Conjoint hk f) q
forall (b :: hk i j) (c :: hk i j) (a :: hk 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
. (Conjoint hk f ~> Conjoint hk f)
-> (Companion hk f ~> Companion hk f)
-> Obj p
-> O (O (Conjoint hk f) (Companion hk f)) p
~> O (Conjoint hk f) (O (Companion hk f) p)
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' Conjoint hk f ~> Conjoint hk f
conF Companion hk f ~> Companion hk f
comF (forall (a :: hk i j). (CategoryOf (hk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p) (O (O (Conjoint hk f) (Companion hk f)) p
~> O (Conjoint hk f) (O (Companion hk f) p))
-> (p ~> O (O (Conjoint hk f) (Companion hk f)) p)
-> p ~> O (Conjoint hk f) (O (Companion hk f) p)
forall (b :: hk i j) (c :: hk i j) (a :: hk 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
. (I ~> O (Conjoint hk f) (Companion hk f))
-> Obj p -> p ~> O (O (Conjoint hk f) (Companion hk f)) p
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O c b
leftUnitorInvWith (Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {j :: s} {k :: s} (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 Obj f
f) Obj p
forall (a :: hk i j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob0 hk i, Ob0 hk k, Ob (O (Companion hk f) p), Ob q) =>
p ~> O (Conjoint hk f) q)
-> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q
forall (i :: s) (j :: s) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Companion hk f) p ~> q
n ((Ob0 vk j, Ob0 vk k, Ob f, Ob f) => p ~> O (Conjoint hk f) q)
-> Obj f -> p ~> O (Conjoint hk f) q
forall (i :: s) (j :: s) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
flipCompanionInv
:: forall {j} {k} hk vk (f :: vk j k) p q
. (Equipment hk vk, Ob q)
=> Obj f
-> p ~> Conjoint hk f `O` q
-> Companion hk f `O` p ~> q
flipCompanionInv :: forall {s} {i :: s} {j :: s} {k :: s} (hk :: CAT s) (vk :: CAT s)
(f :: vk j k) (p :: hk i j) (q :: hk i k).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q
flipCompanionInv Obj f
f p ~> O (Conjoint hk f) q
n =
let comF :: Companion hk f ~> Companion hk f
comF = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj f
f; conF :: Conjoint hk f ~> Conjoint hk f
conF = 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
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
(g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj f
f
in ((O (Companion hk f) (Conjoint hk f) ~> I)
-> (q ~> q) -> O (O (Companion hk f) (Conjoint hk f)) q ~> q
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
(a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O c a ~> b
leftUnitorWith (Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {j :: s} {k :: s} (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 Obj f
f) q ~> q
forall (a :: hk i k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (O (O (Companion hk f) (Conjoint hk f)) q ~> q)
-> (O (Companion hk f) p
~> O (O (Companion hk f) (Conjoint hk f)) q)
-> O (Companion hk f) p ~> q
forall (b :: hk i k) (c :: hk i k) (a :: hk i 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
. (Companion hk f ~> Companion hk f)
-> (Conjoint hk f ~> Conjoint hk f)
-> (q ~> q)
-> O (Companion hk f) (O (Conjoint hk f) q)
~> O (O (Companion hk f) (Conjoint hk f)) q
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv' Companion hk f ~> Companion hk f
comF Conjoint hk f ~> Conjoint hk f
conF (forall (a :: hk i k). (CategoryOf (hk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @q) (O (Companion hk f) (O (Conjoint hk f) q)
~> O (O (Companion hk f) (Conjoint hk f)) q)
-> (O (Companion hk f) p
~> O (Companion hk f) (O (Conjoint hk f) q))
-> O (Companion hk f) p ~> O (O (Companion hk f) (Conjoint hk f)) q
forall (b :: hk i k) (c :: hk i k) (a :: hk i 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
. (Companion hk f ~> Companion hk f
comF (Companion hk f ~> Companion hk f)
-> (p ~> O (Conjoint hk f) q)
-> O (Companion hk f) p ~> O (Companion hk f) (O (Conjoint hk f) q)
forall {i :: s} (j :: s) (k :: s) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` p ~> O (Conjoint hk f) q
n)) ((Ob0 hk i, Ob0 hk j, Ob p, Ob (O (Conjoint hk f) q)) =>
O (Companion hk f) p ~> q)
-> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q
forall (i :: s) (j :: s) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ p ~> O (Conjoint hk f) q
n ((Ob0 vk j, Ob0 vk k, Ob f, Ob f) => O (Companion hk f) p ~> q)
-> Obj f -> O (Companion hk f) p ~> q
forall (i :: s) (j :: s) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
flipConjoint
:: forall {j} {k} hk vk (f :: vk j k) p q
. (Equipment hk vk, Ob p)
=> Obj f
-> p `O` Conjoint hk f ~> q
-> p ~> q `O` Companion hk f
flipConjoint :: forall {c} {k :: c} {j :: c} {k :: c} (hk :: CAT c) (vk :: CAT c)
(f :: vk j k) (p :: hk j k) (q :: hk k k).
(Equipment hk vk, Ob p) =>
Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
flipConjoint Obj f
f O p (Conjoint hk f) ~> q
n =
let comF :: Companion hk f ~> Companion hk f
comF = 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
forall (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 @hk Obj f
f; conF :: Conjoint hk f ~> Conjoint hk f
conF = 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
forall (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 @hk Obj f
f
in ((O p (Conjoint hk f) ~> q
n (O p (Conjoint hk f) ~> q)
-> (Companion hk f ~> Companion hk f)
-> O (O p (Conjoint hk f)) (Companion hk f) ~> O q (Companion hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Companion hk f ~> Companion hk f
comF) (O (O p (Conjoint hk f)) (Companion hk f) ~> O q (Companion hk f))
-> (p ~> O (O p (Conjoint hk f)) (Companion hk f))
-> p ~> O q (Companion hk f)
forall (b :: hk j k) (c :: hk j k) (a :: hk j 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
. Obj p
-> (Conjoint hk f ~> Conjoint hk f)
-> (Companion hk f ~> Companion hk f)
-> O p (O (Conjoint hk f) (Companion hk f))
~> O (O p (Conjoint hk f)) (Companion hk f)
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv' (forall (a :: hk j k). (CategoryOf (hk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p) Conjoint hk f ~> Conjoint hk f
conF Companion hk f ~> Companion hk f
comF (O p (O (Conjoint hk f) (Companion hk f))
~> O (O p (Conjoint hk f)) (Companion hk f))
-> (p ~> O p (O (Conjoint hk f) (Companion hk f)))
-> p ~> O (O p (Conjoint hk f)) (Companion hk f)
forall (b :: hk j k) (c :: hk j k) (a :: hk j 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
. (I ~> O (Conjoint hk f) (Companion hk f))
-> Obj p -> p ~> O p (O (Conjoint hk f) (Companion hk f))
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O b c
rightUnitorInvWith (Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {j :: c} {k :: c} (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 Obj f
f) Obj p
forall (a :: hk j k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob0 hk k, Ob0 hk k, Ob (O p (Conjoint hk f)), Ob q) =>
p ~> O q (Companion hk f))
-> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O p (Conjoint hk f) ~> q
n ((Ob0 vk j, Ob0 vk k, Ob f, Ob f) => p ~> O q (Companion hk f))
-> Obj f -> p ~> O q (Companion hk f)
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
flipConjointInv
:: forall {j} {k} hk vk (f :: vk j k) p q
. (Equipment hk vk, Ob q)
=> Obj f
-> p ~> q `O` Companion hk f
-> p `O` Conjoint hk f ~> q
flipConjointInv :: forall {c} {k :: c} {j :: c} {k :: c} (hk :: CAT c) (vk :: CAT c)
(f :: vk j k) (p :: hk j k) (q :: hk k k).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q
flipConjointInv Obj f
f p ~> O q (Companion hk f)
n =
let comF :: Companion hk f ~> Companion hk f
comF = 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
forall (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 @hk Obj f
f; conF :: Conjoint hk f ~> Conjoint hk f
conF = 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
forall (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 @hk Obj f
f
in ((O (Companion hk f) (Conjoint hk f) ~> I)
-> (q ~> q) -> O q (O (Companion hk f) (Conjoint hk f)) ~> q
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
(a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith (Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {j :: c} {k :: c} (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 Obj f
f) q ~> q
forall (a :: hk k k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id (O q (O (Companion hk f) (Conjoint hk f)) ~> q)
-> (O p (Conjoint hk f)
~> O q (O (Companion hk f) (Conjoint hk f)))
-> O p (Conjoint hk f) ~> q
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. (q ~> q)
-> (Companion hk f ~> Companion hk f)
-> (Conjoint hk f ~> Conjoint hk f)
-> O (O q (Companion hk f)) (Conjoint hk f)
~> O q (O (Companion hk f) (Conjoint hk f))
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
{j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' (forall (a :: hk k k). (CategoryOf (hk k k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @q) Companion hk f ~> Companion hk f
comF Conjoint hk f ~> Conjoint hk f
conF (O (O q (Companion hk f)) (Conjoint hk f)
~> O q (O (Companion hk f) (Conjoint hk f)))
-> (O p (Conjoint hk f)
~> O (O q (Companion hk f)) (Conjoint hk f))
-> O p (Conjoint hk f) ~> O q (O (Companion hk f) (Conjoint hk f))
forall (b :: hk k k) (c :: hk k k) (a :: hk k 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
. (p ~> O q (Companion hk f)
n (p ~> O q (Companion hk f))
-> (Conjoint hk f ~> Conjoint hk f)
-> O p (Conjoint hk f) ~> O (O q (Companion hk f)) (Conjoint hk f)
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
(c :: hk i j) (d :: hk 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` Conjoint hk f ~> Conjoint hk f
conF)) ((Ob0 hk j, Ob0 hk k, Ob p, Ob (O q (Companion hk f))) =>
O p (Conjoint hk f) ~> q)
-> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ p ~> O q (Companion hk f)
n ((Ob0 vk j, Ob0 vk k, Ob f, Ob f) => O p (Conjoint hk f) ~> q)
-> Obj f -> O p (Conjoint hk f) ~> q
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 f
f
type RetroSq :: forall {c} {hk :: CAT c} {vk :: CAT c} {h} {i} {j} {k}. (hk j h, vk h i) +-> (hk k i, vk j k)
data RetroSq pf qg where
RetroSq
:: forall {hk} {vk} {h} {i} {j} {k} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k)
. (Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g)
=> (q `O` Companion hk g) ~> Companion hk f `O` p
-> RetroSq '(q, g) '(p, f)
instance
(HasCompanions hk vk, Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k)
=> Profunctor (RetroSq :: (hk j h, vk h i) +-> (hk k i, vk j k))
where
dimap :: forall (c :: (hk k i, vk j k)) (a :: (hk k i, vk j k))
(b :: (hk j h, vk h i)) (d :: (hk j h, vk h i)).
(c ~> a) -> (b ~> d) -> RetroSq a b -> RetroSq c d
dimap (a1 ~> b1
q :**: a2 ~> b2
f) (a1 ~> b1
p :**: a2 ~> b2
g) (RetroSq O q (Companion hk g) ~> O (Companion hk f) p
sq) = (O a1 (Companion hk a2) ~> O (Companion hk b2) b1)
-> RetroSq '(a1, a2) '(b1, b2)
forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {h :: s}
{i :: s} {j :: s} {k :: s} (p :: hk j h) (q :: hk k i)
(f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O q (Companion hk g) ~> O (Companion hk f) p)
-> RetroSq '(q, g) '(p, f)
RetroSq (a1 ~> b1
q (a1 ~> b1)
-> (Companion hk a2 ~> Companion hk b2)
-> O a1 (Companion hk a2) ~> O b1 (Companion hk b2)
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
|| (a2 ~> b2) -> Companion hk a2 ~> Companion hk b2
forall {j :: c} {k :: c} (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 a2 ~> b2
f (O a1 (Companion hk a2) ~> O b1 (Companion hk b2))
-> (O b1 (Companion hk b2) ~> O (Companion hk a2) a1)
-> O a1 (Companion hk a2) ~> O (Companion hk a2) a1
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== O b1 (Companion hk b2) ~> O (Companion hk a2) a1
O q (Companion hk g) ~> O (Companion hk f) p
sq (O a1 (Companion hk a2) ~> O (Companion hk a2) a1)
-> (O (Companion hk a2) a1 ~> O (Companion hk b2) b1)
-> O a1 (Companion hk a2) ~> O (Companion hk b2) b1
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== (a2 ~> b2) -> Companion hk a2 ~> Companion hk b2
forall {j :: c} {k :: c} (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 a2 ~> b2
g (Companion hk a2 ~> Companion hk b2)
-> (a1 ~> b1) -> O (Companion hk a2) a1 ~> O (Companion hk b2) b1
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
|| a1 ~> b1
p) ((Ob0 hk j, Ob0 hk h, Ob a1, Ob b1) => RetroSq c d)
-> (a1 ~> b1) -> RetroSq c d
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ a1 ~> b1
p ((Ob0 hk k, Ob0 hk i, Ob a1, Ob b1) => RetroSq c d)
-> (a1 ~> b1) -> RetroSq c d
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ a1 ~> b1
q ((Ob0 vk j, Ob0 vk k, Ob a2, Ob b2) => RetroSq c d)
-> (a2 ~> b2) -> RetroSq c d
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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
\\\ a2 ~> b2
f ((Ob0 vk h, Ob0 vk i, Ob a2, Ob b2) => RetroSq c d)
-> (a2 ~> b2) -> RetroSq c d
forall (i :: c) (j :: c) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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
\\\ a2 ~> b2
g
(Ob a, Ob b) => r
r \\ :: forall (a :: (hk k i, vk j k)) (b :: (hk j h, vk h i)) r.
((Ob a, Ob b) => r) -> RetroSq a b -> r
\\ RetroSq O q (Companion hk g) ~> O (Companion hk f) p
sq = r
(Ob (O q (Companion hk g)), Ob (O (Companion hk f) p)) => r
(Ob a, Ob b) => r
r ((Ob (O q (Companion hk g)), Ob (O (Companion hk f) p)) => r)
-> (O q (Companion hk g) ~> O (Companion hk f) p) -> r
forall (a :: hk j i) (b :: hk j i) 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
\\ O q (Companion hk g) ~> O (Companion hk f) p
sq