{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares.Relative where

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Category.Bicategory.Relative qualified as Rel
import Proarrow.Category.Bicategory.Strictified (Path (..), SPath (..), Strictified (..), singleton)
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..), flipCompanion, flipConjointInv)
import Proarrow.Core (CategoryOf (..), obj)

-- | The unit square for a @j@-relative monad @t@.
--
-- > A-----A
-- > |  /-<j
-- > |  @  |
-- > |  \->t
-- > A-----A
unit
  :: forall {hk} {vk} {a} {e} {j :: vk a e} {t :: vk a e}
   . (Equipment hk vk, Rel.Monad (Conjoint hk j) (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j)
  => Sq '(Nil, Nil :: Path vk a a) '(Companion hk t ::: Conjoint hk j ::: Nil, Nil)
unit :: forall {k} {hk :: CAT k} {vk :: CAT k} {a :: k} {e :: k}
       {j :: vk a e} {t :: vk a e}.
(Equipment hk vk, Monad (Conjoint hk j) (Companion hk t), Ob0 vk a,
 Ob0 vk e, Ob t, Ob j) =>
Sq '(Nil, Nil) '(Companion hk t ::: (Conjoint hk j ::: Nil), Nil)
unit =
  let jc :: Conjoint hk j ~> Conjoint hk j
jc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j); tc :: Companion hk t ~> Companion hk t
tc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t)
  in (O (Companion (Path hk) Nil) Nil
 ~> O (Companion hk t ::: (Conjoint hk j ::: Nil))
      (Companion (Path hk) Nil))
-> Sq
     '(Nil, Nil) '(Companion hk t ::: (Conjoint hk j ::: Nil), Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {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 (SPath Nil
-> SPath (Companion hk t ::: (Conjoint hk j ::: Nil))
-> (Fold Nil ~> Fold (Companion hk t ::: (Conjoint hk j ::: Nil)))
-> Strictified Nil (Companion hk t ::: (Conjoint hk j ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil ((Companion hk t ~> Companion hk t)
-> SPath (Conjoint hk j ::: Nil)
-> SPath (Companion hk t ::: (Conjoint hk j ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc ((Conjoint hk j ~> Conjoint hk j)
-> SPath Nil -> SPath (Conjoint hk j ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Conjoint hk j ~> Conjoint hk j
jc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)) (forall (j :: hk e a) (t :: hk a e). Monad j t => I ~> O j t
forall {s} {kk :: CAT s} {a :: s} {e :: s} (j :: kk e a)
       (t :: kk a e).
Monad j t =>
I ~> O j t
Rel.unit @(Conjoint hk j) @(Companion hk t)))

-- | The multiplication square for a @j@-relative monad @t@.
--
-- > E-----E
-- > t>-\  |
-- > j<-@->t
-- > t>-/  |
-- > A-----A
mult
  :: forall {hk} {vk} {a} {e} {j :: vk a e} {t :: vk a e}
   . (Equipment hk vk, Rel.Monad (Conjoint hk j) (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j)
  => Sq '(Companion hk t ::: Conjoint hk j ::: Companion hk t ::: Nil, Nil :: Path vk e e) '(Companion hk t ::: Nil, Nil)
mult :: forall {k} {hk :: CAT k} {vk :: CAT k} {a :: k} {e :: k}
       {j :: vk a e} {t :: vk a e}.
(Equipment hk vk, Monad (Conjoint hk j) (Companion hk t), Ob0 vk a,
 Ob0 vk e, Ob t, Ob j) =>
Sq
  '(Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)),
    Nil)
  '(Companion hk t ::: Nil, Nil)
mult =
  let jc :: Conjoint hk j ~> Conjoint hk j
jc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j); tc :: Companion hk t ~> Companion hk t
tc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t)
  in (O (Companion (Path hk) Nil)
   (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
 ~> O (Companion hk t ::: Nil) (Companion (Path hk) Nil))
-> Sq
     '(Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)),
       Nil)
     '(Companion hk t ::: Nil, Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {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 (SPath
  (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
-> SPath (Companion hk t ::: Nil)
-> (Fold
      (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
    ~> Fold (Companion hk t ::: Nil))
-> Strictified
     (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
     (Companion hk t ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str ((Companion hk t ~> Companion hk t)
-> SPath (Conjoint hk j ::: (Companion hk t ::: Nil))
-> SPath
     (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc ((Conjoint hk j ~> Conjoint hk j)
-> SPath (Companion hk t ::: Nil)
-> SPath (Conjoint hk j ::: (Companion hk t ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Conjoint hk j ~> Conjoint hk j
jc ((Companion hk t ~> Companion hk t)
-> SPath Nil -> SPath (Companion hk t ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))) ((Companion hk t ~> Companion hk t)
-> SPath Nil -> SPath (Companion hk t ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) (forall (j :: hk e a) (t :: hk a e). Monad j t => O (O t j) t ~> t
forall {s} {kk :: CAT s} {a :: s} {e :: s} (j :: kk e a)
       (t :: kk a e).
Monad j t =>
O (O t j) t ~> t
Rel.mult @(Conjoint hk j) @(Companion hk t)))

-- | @j@-relative adjunction
--
-- > A-----A
-- > |  /-<j
-- > l<-@  |
-- > |  \->r
-- > C-----C
leftAdjunct
  :: forall {hk} {vk} {a} {c} {e} {j :: vk a e} {l :: vk a c} {r :: vk c e}
   . ( Equipment hk vk
     , Rel.Adjunction (Conjoint hk j) (Companion hk l) (Companion hk r)
     , Ob0 vk a
     , Ob0 vk c
     , Ob0 vk e
     , Ob j
     , Ob l
     , Ob r
     )
  => Sq '(Conjoint hk l ::: Nil, Nil :: Path vk a a) '(Companion hk r ::: Conjoint hk j ::: Nil, Nil :: Path vk c c)
leftAdjunct :: forall {k} {hk :: CAT k} {vk :: CAT k} {a :: k} {c :: k} {e :: k}
       {j :: vk a e} {l :: vk a c} {r :: vk c e}.
(Equipment hk vk,
 Adjunction (Conjoint hk j) (Companion hk l) (Companion hk r),
 Ob0 vk a, Ob0 vk c, Ob0 vk e, Ob j, Ob l, Ob r) =>
Sq
  '(Conjoint hk l ::: Nil, Nil)
  '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
leftAdjunct =
  let l :: Obj l
l = forall (a :: vk a c). (CategoryOf (vk a c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @l; jc :: Conjoint hk j ~> Conjoint hk j
jc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j); lc :: Companion hk l ~> Companion hk l
lc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj l
l; rc :: Companion hk r ~> Companion hk r
rc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk c e). (CategoryOf (vk c e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r)
  in (O (Companion (Path hk) Nil) (Conjoint hk l ::: Nil)
 ~> O (Companion hk r ::: (Conjoint hk j ::: Nil))
      (Companion (Path hk) Nil))
-> Sq
     '(Conjoint hk l ::: Nil, Nil)
     '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {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
       ( Obj (l ::: Nil)
-> (Nil
    ~> O (Companion hk r ::: (Conjoint hk j ::: Nil))
         (Companion (Path hk) (l ::: Nil)))
-> O Nil (Conjoint (Path hk) (l ::: Nil))
   ~> (Companion hk r ::: (Conjoint hk j ::: Nil))
forall {c} {k1 :: c} {j :: c} {k2 :: c} (hk :: CAT c) (vk :: CAT c)
       (f :: vk j k2) (p :: hk j k1) (q :: hk k2 k1).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O q (Companion hk f)) -> O p (Conjoint hk f) ~> q
flipConjointInv
           (Obj l -> Obj (l ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton Obj l
l)
           (SPath Nil
-> SPath
     (Companion hk l ::: (Companion hk r ::: (Conjoint hk j ::: Nil)))
-> (Fold Nil
    ~> Fold
         (Companion hk l ::: (Companion hk r ::: (Conjoint hk j ::: Nil))))
-> Strictified
     Nil
     (Companion hk l ::: (Companion hk r ::: (Conjoint hk j ::: Nil)))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil ((Companion hk l ~> Companion hk l)
-> SPath (Companion hk r ::: (Conjoint hk j ::: Nil))
-> SPath
     (Companion hk l ::: (Companion hk r ::: (Conjoint hk j ::: Nil)))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk l ~> Companion hk l
lc ((Companion hk r ~> Companion hk r)
-> SPath (Conjoint hk j ::: Nil)
-> SPath (Companion hk r ::: (Conjoint hk j ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk r ~> Companion hk r
rc ((Conjoint hk j ~> Conjoint hk j)
-> SPath Nil -> SPath (Conjoint hk j ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Conjoint hk j ~> Conjoint hk j
jc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))) (forall (j :: hk e a) (l :: hk a c) (r :: hk c e).
Adjunction j l r =>
I ~> O (O j r) l
forall {s} {kk :: CAT s} {a :: s} {c :: s} {e :: s} (j :: kk e a)
       (l :: kk a c) (r :: kk c e).
Adjunction j l r =>
I ~> O (O j r) l
Rel.eta @(Conjoint hk j) @(Companion hk l) @(Companion hk r)))
       )
       ((Ob0 hk c, Ob0 hk a, Ob (Conjoint hk l), Ob (Conjoint hk l)) =>
 Sq
   '(Conjoint hk l ::: Nil, Nil)
   '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil))
-> (Conjoint hk l ~> Conjoint hk l)
-> Sq
     '(Conjoint hk l ::: Nil, Nil)
     '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
forall (i :: k) (j :: k) (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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj l
l

-- | @j@-relative adjunction, other direction
--
-- > A-----A
-- > j<-\  |
-- > |  @<-l
-- > r->/  |
-- > C-----C
rightAdjunct
  :: forall {hk} {vk} {a} {c} {e} {j :: vk a e} {l :: vk a c} {r :: vk c e}
   . ( Equipment hk vk
     , Rel.Adjunction (Conjoint hk j) (Companion hk l) (Companion hk r)
     , Ob0 vk a
     , Ob0 vk c
     , Ob0 vk e
     , Ob j
     , Ob l
     , Ob r
     )
  => Sq '(Companion hk r ::: Conjoint hk j ::: Nil, Nil :: Path vk a a) '(Conjoint hk l ::: Nil, Nil :: Path vk c c)
rightAdjunct :: forall {k} {hk :: CAT k} {vk :: CAT k} {a :: k} {c :: k} {e :: k}
       {j :: vk a e} {l :: vk a c} {r :: vk c e}.
(Equipment hk vk,
 Adjunction (Conjoint hk j) (Companion hk l) (Companion hk r),
 Ob0 vk a, Ob0 vk c, Ob0 vk e, Ob j, Ob l, Ob r) =>
Sq
  '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
  '(Conjoint hk l ::: Nil, Nil)
rightAdjunct =
  let l :: Obj l
l = forall (a :: vk a c). (CategoryOf (vk a c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @l; jc :: Conjoint hk j ~> Conjoint hk j
jc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j); lc :: Companion hk l ~> Companion hk l
lc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj l
l; rc :: Companion hk r ~> Companion hk r
rc = 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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk c e). (CategoryOf (vk c e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r)
  in (O (Companion (Path hk) Nil)
   (Companion hk r ::: (Conjoint hk j ::: Nil))
 ~> O (Conjoint hk l ::: Nil) (Companion (Path hk) Nil))
-> Sq
     '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
     '(Conjoint hk l ::: Nil, Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {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
       ( Obj (l ::: Nil)
-> (O (Companion (Path hk) (l ::: Nil))
      (Companion hk r ::: (Conjoint hk j ::: Nil))
    ~> Nil)
-> (Companion hk r ::: (Conjoint hk j ::: Nil))
   ~> O (Conjoint (Path hk) (l ::: Nil)) Nil
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 l -> Obj (l ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton Obj l
l)
           (SPath
  (Companion hk r ::: (Conjoint hk j ::: (Companion hk l ::: Nil)))
-> SPath Nil
-> (Fold
      (Companion hk r ::: (Conjoint hk j ::: (Companion hk l ::: Nil)))
    ~> Fold Nil)
-> Strictified
     (Companion hk r ::: (Conjoint hk j ::: (Companion hk l ::: Nil)))
     Nil
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str ((Companion hk r ~> Companion hk r)
-> SPath (Conjoint hk j ::: (Companion hk l ::: Nil))
-> SPath
     (Companion hk r ::: (Conjoint hk j ::: (Companion hk l ::: Nil)))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk r ~> Companion hk r
rc ((Conjoint hk j ~> Conjoint hk j)
-> SPath (Companion hk l ::: Nil)
-> SPath (Conjoint hk j ::: (Companion hk l ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Conjoint hk j ~> Conjoint hk j
jc ((Companion hk l ~> Companion hk l)
-> SPath Nil -> SPath (Companion hk l ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk l ~> Companion hk l
lc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil (forall (j :: hk e a) (l :: hk a c) (r :: hk c e).
Adjunction j l r =>
O (O l j) r ~> I
forall {s} {kk :: CAT s} {a :: s} {c :: s} {e :: s} (j :: kk e a)
       (l :: kk a c) (r :: kk c e).
Adjunction j l r =>
O (O l j) r ~> I
Rel.epsilon @(Conjoint hk j) @(Companion hk l) @(Companion hk r)))
       )
       ((Ob0 hk c, Ob0 hk a, Ob (Conjoint hk l), Ob (Conjoint hk l)) =>
 Sq
   '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
   '(Conjoint hk l ::: Nil, Nil))
-> (Conjoint hk l ~> Conjoint hk l)
-> Sq
     '(Companion hk r ::: (Conjoint hk j ::: Nil), Nil)
     '(Conjoint hk l ::: Nil, Nil)
forall (i :: k) (j :: k) (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 k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj l
l