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

-- | A double category with companions.
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
  -- All the data needed to make an id-on-objects (pseudo)functor Companion :: vk -> hk
  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

-- | P(f, g)
type Cart (p :: hk h j) (f :: vk h i) (g :: vk j k) = Companion hk g `O` p `O` Conjoint hk f

-- | The kind of a square @'(q, f) '(p, g)@.
--
-- > h--f--i
-- > |  v  |
-- > p--@--q
-- > |  v  |
-- > j--g--k
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

-- | The empty square for an object.
--
-- > k-----k
-- > |     |
-- > |     |
-- > |     |
-- > k-----k
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

-- | Make a square from a horizontal arrow
--
-- > k-----k
-- > |     |
-- > p--@--q
-- > |     |
-- > j-----j
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

-- > j-----j
-- > |     |
-- > p-----p
-- > |     |
-- > k-----k
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

-- > k-----k
-- > |     |
-- > f>--->f
-- > |     |
-- > j-----j
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))

-- > j-----j
-- > |     |
-- > f>--->f
-- > |     |
-- > k-----k
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))

-- | Make a square from a vertical arrow
--
-- > j--f--k
-- > |  v  |
-- > |  @  |
-- > |  v  |
-- > j--g--k
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'

-- > j--f--k
-- > |  v  |
-- > |  |  |
-- > |  v  |
-- > j--f--k
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

-- | Horizontal composition
--
-- > l--d--h     h--f--i     l-f∘d-i
-- > |  v  |     |  v  |     |  v  |
-- > p--@--q ||| q--@--r  =  p--@--r
-- > |  v  |     |  v  |     |  v  |
-- > m--e--j     j--g--k     m-g∘e-k
(|||)
  :: 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

-- | Vertical composition
--
-- >  h--e--i
-- >  |  v  |
-- >  r--@--s
-- >  |  v  |
-- >  j--f--k
-- >    ===
-- >  j--f--k
-- >  |  v  |
-- >  p--@--q
-- >  |  v  |
-- >  l--g--m
-- >
-- >    v v
-- >
-- >  h--e--i
-- >  |  v  |
-- > r∘p-@-s∘q
-- >  |  v  |
-- >  j--g--k
(===)
  :: 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

-- > j--f--k
-- > |  v  |
-- > |  \->f
-- > |     |
-- > j-----j
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

-- > k-----k
-- > |     |
-- > f>-\  |
-- > |  v  |
-- > j--f--k
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

-- > j-----j
-- > |     |
-- > |  /-<f
-- > |  v  |
-- > j--f--k
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

-- > j--f--k
-- > |  v  |
-- > f<-/  |
-- > |     |
-- > k-----k
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

-- |
-- The kind of a retro square @'(q, g) '(p, f)@.
--
-- > h--f--i
-- > |  v  |
-- > p--§--q
-- > |  v  |
-- > j--g--k
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