{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares.Limit where

import Proarrow.Category.Bicategory (Adjunction, Bicategory (..))
import Proarrow.Category.Bicategory qualified as Adj
import Proarrow.Category.Bicategory.Strictified (Path (..), SPath (..), Strictified (..))
import Proarrow.Category.Equipment (HasCompanions (..), Sq (..), (===), (|||))
import Proarrow.Category.Equipment.Limit qualified as L
import Proarrow.Core (CategoryOf (..), obj, (//))
import Proarrow.Squares (vArr, vCombine, vId, vId', vSplit, vUnitor, vUnitorInv)

-- | The projection out of the @j@-weighted limit @l@ of @d@.
--
-- > A--l--K
-- > |  v  |
-- > j--@  |
-- > |  v  |
-- > I--d--K
limit
  :: forall {hk} {vk} {a} {i} {k} (j :: hk i a) (d :: vk i k)
   . (Ob0 vk i, L.HasLimits vk j k, Ob d)
  => Sq '(j ::: Nil, L.Limit j d ::: Nil) '(Nil, d ::: Nil)
limit :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk i a) (d :: vk i k).
(Ob0 vk i, HasLimits vk j k, Ob d) =>
Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
limit =
  let l :: Obj (Limit j d)
l = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
L.limitObj @vk @j @k @d
  in (O (Companion (Path hk) (Limit j d ::: Nil)) (j ::: Nil)
 ~> O Nil (Companion (Path hk) (d ::: Nil)))
-> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: 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 (j ::: (Companion hk (Limit j d) ::: Nil))
-> SPath (Companion hk d ::: Nil)
-> (Fold (j ::: (Companion hk (Limit j d) ::: Nil))
    ~> Fold (Companion hk d ::: Nil))
-> Strictified
     (j ::: (Companion hk (Limit j d) ::: Nil)) (Companion hk d ::: 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
          (Obj j
-> SPath (Companion hk (Limit j d) ::: Nil)
-> SPath (j ::: (Companion hk (Limit j d) ::: 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 (forall (a :: hk i a). (CategoryOf (hk i a), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j) (Obj (Companion hk (Limit j d))
-> SPath Nil -> SPath (Companion hk (Limit j d) ::: 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 (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 (Limit j d)
l) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))
          (Obj (Companion hk d) -> SPath Nil -> SPath (Companion hk d ::: 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 (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 i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d)) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)
          (forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
O (Companion hk (Limit j d)) j ~> Companion hk d
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
O (Companion hk (Limit j d)) j ~> Companion hk d
L.limit @vk @j @k @d)
      )
      ((Ob0 vk a, Ob0 vk k, Ob (Limit j d), Ob (Limit j d)) =>
 Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> Obj (Limit j d)
-> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
forall (i :: k) (j :: k) (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 (Limit j d)
l

-- | The universal property of the limit.
--
-- The dotted inner square is the input square, the outer square is the output square.
--
-- > A-+--p--+-K
-- > | :  v  : |
-- > | j--@  : |
-- > | :  v  : |
-- > | I..d..K |
-- > A----l----K
limitUniv
  :: forall {hk} {vk} {a} {i} {k} (j :: hk i a) (d :: vk i k) (p :: vk a k)
   . (Ob0 vk i, L.HasLimits vk j k, Ob d, Ob p)
  => Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
  -> Sq '(Nil :: Path hk a a, p ::: Nil) '(Nil, L.Limit j d ::: Nil)
limitUniv :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk i a) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil)
limitUniv (Sq (Str SPath (j ::: (Companion hk p ::: Nil))
_ SPath (Companion hk d ::: Nil)
_ Fold (j ::: (Companion hk p ::: Nil))
~> Fold (Companion hk d ::: Nil)
n)) = (p ~> Limit j d) -> Sq '(Nil, p ::: Nil) '(I, Limit j d ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
(f ~> g) -> Sq '(Nil, f ::: Nil) '(I, g ::: Nil)
vArr (forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) (p :: vk a k).
(HasLimits vk j k, Ob d, Ob p) =>
(O (Companion hk p) j ~> Companion hk d) -> p ~> Limit j d
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k)
       (p :: vk a k).
(HasLimits vk j k, Ob d, Ob p) =>
(O (Companion hk p) j ~> Companion hk d) -> p ~> Limit j d
L.limitUniv @vk @j @k @d @p O (Companion hk p) j ~> Companion hk d
Fold (j ::: (Companion hk p ::: Nil))
~> Fold (Companion hk d ::: Nil)
n) ((Ob0 hk i, Ob0 hk k, Ob (O (Companion hk p) j),
  Ob (Companion hk d)) =>
 Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil))
-> (O (Companion hk p) j ~> Companion hk d)
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: 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
\\\ O (Companion hk p) j ~> Companion hk d
Fold (j ::: (Companion hk p ::: Nil))
~> Fold (Companion hk d ::: Nil)
n

-- | Preservation of limits by right adjoints
--
-- Let @l@ be the @j@-weighted limit of @d@ and @l'@ be the @j@-weighted limit of @g ∘ d@.
-- Then we provide the following square:
--
-- > A--l'-K'
-- > |  v  |
-- > |  @  |
-- > | / \ |
-- > | v v |
-- > A-l-g-K'
--
-- With this implementation:
--
-- > +-----l'--+---------+
-- > |     v   |   /@\   |
-- > |     |   |  v   v  |
-- > +-+---l'--+-f-+-+-g-+
-- > | :   v   | v : | v |
-- > | j---@   | | : | | |
-- > | :  / \  | | : | | |
-- > | : v   v | v : | | |
-- > | +-d-+-g-+-f-+ | | |
-- > | : | | v   v : | | |
-- > | : v |  \@/  : | | |
-- > | +.d.+.......+ | v |
-- > +-------l-------+-g-+
rightAdjointPreservesLimits
  :: forall {hk} {vk} {k} {k'} {i} {a} (f :: vk k' k) (g :: vk k k') (d :: vk i k) (j :: hk i a)
   . ( Adjunction f g
     , HasCompanions hk vk
     , Ob d
     , Ob f
     , Ob g
     , L.HasLimits vk j k
     , L.HasLimits vk j k'
     , Ob0 vk i
     , Ob0 vk k
     , Ob0 vk k'
     , Ob0 vk a
     )
  => Sq '(Nil :: Path hk a a, L.Limit j (g `O` d) ::: Nil) '(Nil, L.Limit j d ::: g ::: Nil)
rightAdjointPreservesLimits :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {k :: k}
       {k' :: k} {i :: k} {a :: k} (f :: vk k' k) (g :: vk k k')
       (d :: vk i k) (j :: hk i a).
(Adjunction f g, HasCompanions hk vk, Ob d, Ob f, Ob g,
 HasLimits vk j k, HasLimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k',
 Ob0 vk a) =>
Sq
  '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil))
rightAdjointPreservesLimits =
  let g :: Obj g
g = forall (a :: vk k k'). (CategoryOf (vk k k'), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g; d :: Obj d
d = forall (a :: vk i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d; f :: Obj f
f = forall (a :: vk k' k). (CategoryOf (vk k' k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f
  in Obj g
g Obj g -> Obj d -> O g d ~> O g d
forall {i :: k} (j :: k) (k :: k) (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 d
d (O g d ~> O g d)
-> ((Ob (O g d), Ob (O g d)) =>
    Sq
      '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil)))
-> Sq
     '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      let l' :: Obj (Limit j (O g d))
l' = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
L.limitObj @vk @j @k' @(g `O` d)
      in Obj (Limit j (O g d))
-> Sq
     '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j (O g d) ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
Obj f -> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId' Obj (Limit j (O g d))
l' Sq '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j (O g d) ::: Nil)
-> Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
-> Sq
     '(Nil, O Nil (Limit j (O g d) ::: Nil))
     '(Nil, O (f ::: (g ::: Nil)) (Limit j (O g d) ::: Nil))
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)
||| forall (f :: vk k' k) (g :: vk k k').
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk k',
 Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk k j).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j,
 Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
unit @f @g
          Sq
  '(Nil, Limit j (O g d) ::: Nil)
  '(Nil, Limit j (O g d) ::: (f ::: (g ::: Nil)))
-> Sq
     '(Nil, Limit j (O g d) ::: (f ::: (g ::: Nil)))
     '(Nil, Limit j d ::: (g ::: Nil))
-> Sq
     '(O Nil Nil, Limit j (O g d) ::: Nil)
     '(O Nil Nil, Limit j d ::: (g ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== ( Sq
  '(Nil, Limit j (O g d) ::: (f ::: Nil))
  '(Nil, O f (Limit j (O g d)) ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine
                  Sq
  '(Nil, Limit j (O g d) ::: (f ::: Nil))
  '(Nil, O f (Limit j (O g d)) ::: Nil)
-> Sq
     '(Nil, O f (Limit j (O g d)) ::: Nil) '(Nil, Limit j d ::: Nil)
-> Sq
     '(O Nil Nil, Limit j (O g d) ::: (f ::: Nil))
     '(O Nil Nil, Limit j d ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== forall (j :: hk i a) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk i a) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil)
limitUniv @j
                    ( Sq
  '(Nil, O f (Limit j (O g d)) ::: Nil)
  '(Nil, Limit j (O g d) ::: (f ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit
                        Sq
  '(Nil, O f (Limit j (O g d)) ::: Nil)
  '(Nil, Limit j (O g d) ::: (f ::: Nil))
-> Sq
     '(j ::: Nil, Limit j (O g d) ::: (f ::: Nil))
     '(Nil, d ::: (g ::: (f ::: Nil)))
-> Sq
     '(O Nil (j ::: Nil), O f (Limit j (O g d)) ::: Nil)
     '(O Nil Nil, d ::: (g ::: (f ::: Nil)))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== (forall (j :: hk i a) (d :: vk i k').
(Ob0 vk i, HasLimits vk j k', Ob d) =>
Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk i a) (d :: vk i k).
(Ob0 vk i, HasLimits vk j k, Ob d) =>
Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
limit @j Sq '(j ::: Nil, Limit j (O g d) ::: Nil) '(Nil, O g d ::: Nil)
-> Sq '(Nil, O g d ::: Nil) '(Nil, d ::: (g ::: Nil))
-> Sq
     '(O (j ::: Nil) Nil, Limit j (O g d) ::: Nil)
     '(O Nil Nil, d ::: (g ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq '(Nil, O g d ::: Nil) '(Nil, d ::: (g ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit) Sq '(j ::: Nil, Limit j (O g d) ::: Nil) '(Nil, d ::: (g ::: Nil))
-> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
-> Sq
     '(j ::: Nil, O (f ::: Nil) (Limit j (O g d) ::: Nil))
     '(Nil, O (f ::: Nil) (d ::: (g ::: Nil)))
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)
||| forall (f :: vk k' k).
(HasCompanions hk vk, Ob0 vk k', Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @f
                        Sq
  '(j ::: Nil, O f (Limit j (O g d)) ::: Nil)
  '(Nil, d ::: (g ::: (f ::: Nil)))
-> Sq '(Nil, d ::: (g ::: (f ::: Nil))) '(Nil, d ::: Nil)
-> Sq
     '(O (j ::: Nil) Nil, O f (Limit j (O g d)) ::: Nil)
     '(O Nil Nil, d ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== forall (f :: vk i k).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @d Sq '(Nil, d ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
-> Sq
     '(Nil, O (g ::: (f ::: Nil)) (d ::: Nil)) '(Nil, O Nil (d ::: Nil))
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)
||| forall (f :: vk k' k) (g :: vk k k').
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk k',
 Ob0 vk k) =>
Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk k j).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j,
 Ob0 vk k) =>
Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
counit @f @g
                    )
              )
            Sq
  '(Nil, Limit j (O g d) ::: (f ::: Nil)) '(Nil, Limit j d ::: Nil)
-> Sq '(Nil, g ::: Nil) '(Nil, g ::: Nil)
-> Sq
     '(Nil, O (g ::: Nil) (Limit j (O g d) ::: (f ::: Nil)))
     '(Nil, O (g ::: Nil) (Limit j d ::: Nil))
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)
||| forall (f :: vk k k').
(HasCompanions hk vk, Ob0 vk k, Ob0 vk k', Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @g
          ((Ob0 vk a, Ob0 vk k', Ob (Limit j (O g d)),
  Ob (Limit j (O g d))) =>
 Sq
   '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil)))
-> Obj (Limit j (O g d))
-> Sq
     '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil))
forall (i :: k) (j :: k) (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 (Limit j (O g d))
l'
          ((Ob0 vk a, Ob0 vk k, Ob (O f (Limit j (O g d))),
  Ob (O f (Limit j (O g d)))) =>
 Sq
   '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil)))
-> (O f (Limit j (O g d)) ~> O f (Limit j (O g d)))
-> Sq
     '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil))
forall (i :: k) (j :: k) (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 Obj f
-> Obj (Limit j (O g d))
-> O f (Limit j (O g d)) ~> O f (Limit j (O g d))
forall {i :: k} (j :: k) (k :: k) (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 (Limit j (O g d))
l'

-- | The inverse works for any arrow:
--
-- The required square
--
-- > A-l-g-K'
-- > | v v |
-- > | \@/ |
-- > |  |  |
-- > A--l'-K'
--
-- is implemented as
--
-- > A-+-l-+-g-+-K'
-- > | : v | v : |
-- > | j-@ | | : |
-- > | : v | v : |
-- > | +.d.+.g.+ |
-- > A-----l'----K'
rightAdjointPreservesLimitsInv
  :: forall {hk} {vk} {k} {k'} {i} {a} (g :: vk k k') (d :: vk i k) (j :: hk i a)
   . (HasCompanions hk vk, Ob d, Ob g, L.HasLimits vk j k, L.HasLimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a)
  => Sq '(Nil :: Path hk a a, L.Limit j d ::: g ::: Nil) '(Nil, L.Limit j (g `O` d) ::: Nil)
rightAdjointPreservesLimitsInv :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {k :: k}
       {k' :: k} {i :: k} {a :: k} (g :: vk k k') (d :: vk i k)
       (j :: hk i a).
(HasCompanions hk vk, Ob d, Ob g, HasLimits vk j k,
 HasLimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a) =>
Sq
  '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
rightAdjointPreservesLimitsInv =
  let l :: Obj (Limit j d)
l = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
L.limitObj @vk @j @k @d; g :: Obj g
g = forall (a :: vk k k'). (CategoryOf (vk k k'), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g; d :: Obj d
d = forall (a :: vk i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d
  in Sq
  '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, O g (Limit j d) ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine
      Sq
  '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, O g (Limit j d) ::: Nil)
-> Sq
     '(Nil, O g (Limit j d) ::: Nil) '(Nil, Limit j (O g d) ::: Nil)
-> Sq
     '(O Nil Nil, Limit j d ::: (g ::: Nil))
     '(O Nil Nil, Limit j (O g d) ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== forall (j :: hk i a) (d :: vk i k') (p :: vk a k').
(Ob0 vk i, HasLimits vk j k', Ob d, Ob p) =>
Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk i a) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil)
limitUniv @j @(g `O` d) @(g `O` L.Limit j d)
        ( Sq
  '(Nil, O g (Limit j d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit
            Sq
  '(Nil, O g (Limit j d) ::: Nil) '(Nil, Limit j d ::: (g ::: Nil))
-> Sq
     '(j ::: Nil, Limit j d ::: (g ::: Nil)) '(Nil, d ::: (g ::: Nil))
-> Sq
     '(O Nil (j ::: Nil), O g (Limit j d) ::: Nil)
     '(O Nil Nil, d ::: (g ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== forall (j :: hk i a) (d :: vk i k).
(Ob0 vk i, HasLimits vk j k, Ob d) =>
Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk i a) (d :: vk i k).
(Ob0 vk i, HasLimits vk j k, Ob d) =>
Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
limit @j @d Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, g ::: Nil) '(Nil, g ::: Nil)
-> Sq
     '(j ::: Nil, O (g ::: Nil) (Limit j d ::: Nil))
     '(Nil, O (g ::: Nil) (d ::: Nil))
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)
||| forall (f :: vk k k').
(HasCompanions hk vk, Ob0 vk k, Ob0 vk k', Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @g
            Sq '(j ::: Nil, O g (Limit j d) ::: Nil) '(Nil, d ::: (g ::: Nil))
-> Sq '(Nil, d ::: (g ::: Nil)) '(Nil, O g d ::: Nil)
-> Sq
     '(O (j ::: Nil) Nil, O g (Limit j d) ::: Nil)
     '(O Nil Nil, O g d ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq '(Nil, d ::: (g ::: Nil)) '(Nil, O g d ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine
        )
      ((Ob0 vk a, Ob0 vk k, Ob (Limit j d), Ob (Limit j d)) =>
 Sq
   '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> Obj (Limit j d)
-> Sq
     '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
forall (i :: k) (j :: k) (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 (Limit j d)
l
      ((Ob0 vk i, Ob0 vk k', Ob (O g d), Ob (O g d)) =>
 Sq
   '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> (O g d ~> O g d)
-> Sq
     '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
forall (i :: k) (j :: k) (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 Obj g -> Obj d -> O g d ~> O g d
forall {i :: k} (j :: k) (k :: k) (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 d
d
      ((Ob0 vk a, Ob0 vk k', Ob (O g (Limit j d)),
  Ob (O g (Limit j d))) =>
 Sq
   '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> (O g (Limit j d) ~> O g (Limit j d))
-> Sq
     '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
forall (i :: k) (j :: k) (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 Obj g -> Obj (Limit j d) -> O g (Limit j d) ~> O g (Limit j d)
forall {i :: k} (j :: k) (k :: k) (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 (Limit j d)
l

-- | The projection into the @j@-weighted colimit @c@ of @d@.
--
-- > I--d--K
-- > |  v  |
-- > j--@  |
-- > |  v  |
-- > A--l--K
colimit
  :: forall {hk} {vk} {a} {i} {k} (j :: hk a i) (d :: vk i k)
   . (Ob0 vk i, L.HasColimits vk j k, Ob d)
  => Sq '(j ::: Nil, d ::: Nil) '(Nil, L.Colimit j d ::: Nil)
colimit :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk a i) (d :: vk i k).
(Ob0 vk i, HasColimits vk j k, Ob d) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
colimit =
  let c :: Obj (Colimit j d)
c = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
Obj (Colimit j d)
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
Obj (Colimit j d)
L.colimitObj @vk @j @k @d
  in (O (Companion (Path hk) (d ::: Nil)) (j ::: Nil)
 ~> O Nil (Companion (Path hk) (Colimit j d ::: Nil)))
-> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: 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 (j ::: (Companion hk d ::: Nil))
-> SPath (Companion hk (Colimit j d) ::: Nil)
-> (Fold (j ::: (Companion hk d ::: Nil))
    ~> Fold (Companion hk (Colimit j d) ::: Nil))
-> Strictified
     (j ::: (Companion hk d ::: Nil))
     (Companion hk (Colimit j d) ::: 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
          (Obj j
-> SPath (Companion hk d ::: Nil)
-> SPath (j ::: (Companion hk d ::: 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 (forall (a :: hk a i). (CategoryOf (hk a i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j) (Obj (Companion hk d) -> SPath Nil -> SPath (Companion hk d ::: 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 (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 i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d)) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))
          (Obj (Companion hk (Colimit j d))
-> SPath Nil -> SPath (Companion hk (Colimit j d) ::: 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 (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 (Colimit j d)
c) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)
          (forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
O (Companion hk d) j ~> Companion hk (Colimit j d)
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
O (Companion hk d) j ~> Companion hk (Colimit j d)
L.colimit @vk @j @k @d)
      )
      ((Ob0 vk a, Ob0 vk k, Ob (Colimit j d), Ob (Colimit j d)) =>
 Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> Obj (Colimit j d)
-> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
forall (i :: k) (j :: k) (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 (Colimit j d)
c

-- | The universal property of the colimit.
--
-- The dotted inner square is the input square, the outer square is the output square.
--
-- > A----c----K
-- > | I..d..K |
-- > | :  v  : |
-- > | j--@  : |
-- > | :  v  : |
-- > A-+--p--+-K
colimitUniv
  :: forall {hk} {vk} {a} {i} {k} (j :: hk a i) (d :: vk i k) (p :: vk a k)
   . (Ob0 vk i, L.HasColimits vk j k, Ob d, Ob p)
  => Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
  -> Sq '(Nil :: Path hk a a, L.Colimit j d ::: Nil) '(Nil, p ::: Nil)
colimitUniv :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk a i) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasColimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil)
colimitUniv (Sq (Str SPath (j ::: (Companion hk d ::: Nil))
_ SPath (Companion hk p ::: Nil)
_ Fold (j ::: (Companion hk d ::: Nil))
~> Fold (Companion hk p ::: Nil)
n)) = (Colimit j d ~> p)
-> Sq '(Nil, Colimit j d ::: Nil) '(I, p ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
(f ~> g) -> Sq '(Nil, f ::: Nil) '(I, g ::: Nil)
vArr (forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k) (p :: vk a k).
(HasColimits vk j k, Ob d, Ob p) =>
(O (Companion hk d) j ~> Companion hk p) -> Colimit j d ~> p
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k)
       (p :: vk a k).
(HasColimits vk j k, Ob d, Ob p) =>
(O (Companion hk d) j ~> Companion hk p) -> Colimit j d ~> p
L.colimitUniv @vk @j @k @d @p O (Companion hk d) j ~> Companion hk p
Fold (j ::: (Companion hk d ::: Nil))
~> Fold (Companion hk p ::: Nil)
n) ((Ob0 hk a, Ob0 hk k, Ob (O (Companion hk d) j),
  Ob (Companion hk p)) =>
 Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil))
-> (O (Companion hk d) j ~> Companion hk p)
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: 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
\\\ O (Companion hk d) j ~> Companion hk p
Fold (j ::: (Companion hk d ::: Nil))
~> Fold (Companion hk p ::: Nil)
n

-- | Preservation of colimits by left adjoints
--
-- Let @c@ be the @j@-weighted colimit of @d@ and @c'@ be the @j@-weighted colimit of @g ∘ d@.
-- Then we provide the following square:
--
-- > A-c-f-K'
-- > | v v |
-- > | \ / |
-- > |  @  |
-- > |  v  |
-- > A--c'-K'
--
-- With this implementation:
--
-- > +-------c-------+-f-+
-- > | +.d.+.......+ | v |
-- > | : v |  /@\  : | | |
-- > | : | | v   v : | | |
-- > | +-d-+-f-+-g-+ | | |
-- > | : v   v | v : | | |
-- > | :  \ /  | | : | | |
-- > | j---@   | | : | | |
-- > | :   v   | v : | v |
-- > +-+---c'--+-g-+-+-f-+
-- > |     |   |  v   v  |
-- > |     v   |   \@/   |
-- > +-----c'--+---------+
leftAdjointPreservesColimits
  :: forall {hk} {vk} {k} {k'} {i} {a} (f :: vk k k') (g :: vk k' k) (d :: vk i k) (j :: hk a i)
   . ( Adjunction f g
     , HasCompanions hk vk
     , Ob d
     , Ob f
     , Ob g
     , L.HasColimits vk j k
     , L.HasColimits vk j k'
     , Ob0 vk i
     , Ob0 vk k
     , Ob0 vk k'
     , Ob0 vk a
     )
  => Sq '(Nil :: Path hk a a, L.Colimit j d ::: f ::: Nil) '(Nil, L.Colimit j (f `O` d) ::: Nil)
leftAdjointPreservesColimits :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {k :: k}
       {k' :: k} {i :: k} {a :: k} (f :: vk k k') (g :: vk k' k)
       (d :: vk i k) (j :: hk a i).
(Adjunction f g, HasCompanions hk vk, Ob d, Ob f, Ob g,
 HasColimits vk j k, HasColimits vk j k', Ob0 vk i, Ob0 vk k,
 Ob0 vk k', Ob0 vk a) =>
Sq
  '(Nil, Colimit j d ::: (f ::: Nil))
  '(Nil, Colimit j (O f d) ::: Nil)
leftAdjointPreservesColimits =
  let f :: Obj f
f = forall (a :: vk k k'). (CategoryOf (vk k k'), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; g :: Obj g
g = forall (a :: vk k' k). (CategoryOf (vk k' k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g; d :: Obj d
d = forall (a :: vk i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d
  in Obj f
f Obj f -> Obj d -> O f d ~> O f d
forall {i :: k} (j :: k) (k :: k) (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 d
d (O f d ~> O f d)
-> ((Ob (O f d), Ob (O f d)) =>
    Sq
      '(Nil, Colimit j d ::: (f ::: Nil))
      '(Nil, Colimit j (O f d) ::: Nil))
-> Sq
     '(Nil, Colimit j d ::: (f ::: Nil))
     '(Nil, Colimit j (O f d) ::: Nil)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      let c' :: Obj (Colimit j (O f d))
c' = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
Obj (Colimit j d)
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
Obj (Colimit j d)
L.colimitObj @vk @j @k' @(f `O` d)
      in ( forall (j :: hk a i) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasColimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk a i) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasColimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil)
colimitUniv @j
            ( forall (f :: vk i k).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @d Sq '(Nil, d ::: Nil) '(Nil, d ::: Nil)
-> Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
-> Sq
     '(Nil, O Nil (d ::: Nil)) '(Nil, O (f ::: (g ::: Nil)) (d ::: Nil))
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)
||| forall (f :: vk k k') (g :: vk k' k).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk k,
 Ob0 vk k') =>
Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk k j).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j,
 Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
unit @f @g
                Sq '(Nil, d ::: Nil) '(Nil, d ::: (f ::: (g ::: Nil)))
-> Sq
     '(j ::: Nil, d ::: (f ::: (g ::: Nil)))
     '(Nil, Colimit j (O f d) ::: (g ::: Nil))
-> Sq
     '(O Nil (j ::: Nil), d ::: Nil)
     '(O Nil Nil, Colimit j (O f d) ::: (g ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== (Sq '(Nil, d ::: (f ::: Nil)) '(Nil, O f d ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine Sq '(Nil, d ::: (f ::: Nil)) '(Nil, O f d ::: Nil)
-> Sq '(j ::: Nil, O f d ::: Nil) '(Nil, Colimit j (O f d) ::: Nil)
-> Sq
     '(O Nil (j ::: Nil), d ::: (f ::: Nil))
     '(O Nil Nil, Colimit j (O f d) ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== forall (j :: hk a i) (d :: vk i k').
(Ob0 vk i, HasColimits vk j k', Ob d) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk a i) (d :: vk i k).
(Ob0 vk i, HasColimits vk j k, Ob d) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
colimit @j) Sq
  '(j ::: Nil, d ::: (f ::: Nil)) '(Nil, Colimit j (O f d) ::: Nil)
-> Sq '(Nil, g ::: Nil) '(Nil, g ::: Nil)
-> Sq
     '(j ::: Nil, O (g ::: Nil) (d ::: (f ::: Nil)))
     '(Nil, O (g ::: Nil) (Colimit j (O f d) ::: Nil))
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)
||| forall (f :: vk k' k).
(HasCompanions hk vk, Ob0 vk k', Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @g
                Sq
  '(j ::: Nil, d ::: Nil) '(Nil, Colimit j (O f d) ::: (g ::: Nil))
-> Sq
     '(Nil, Colimit j (O f d) ::: (g ::: Nil))
     '(Nil, O g (Colimit j (O f d)) ::: Nil)
-> Sq
     '(O (j ::: Nil) Nil, d ::: Nil)
     '(O Nil Nil, O g (Colimit j (O f d)) ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq
  '(Nil, Colimit j (O f d) ::: (g ::: Nil))
  '(Nil, O g (Colimit j (O f d)) ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine
            )
            Sq
  '(Nil, Colimit j d ::: Nil) '(Nil, O g (Colimit j (O f d)) ::: Nil)
-> Sq
     '(Nil, O g (Colimit j (O f d)) ::: Nil)
     '(Nil, Colimit j (O f d) ::: (g ::: Nil))
-> Sq
     '(O Nil Nil, Colimit j d ::: Nil)
     '(O Nil Nil, Colimit j (O f d) ::: (g ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq
  '(Nil, O g (Colimit j (O f d)) ::: Nil)
  '(Nil, Colimit j (O f d) ::: (g ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit
         )
          Sq
  '(Nil, Colimit j d ::: Nil)
  '(Nil, Colimit j (O f d) ::: (g ::: Nil))
-> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
-> Sq
     '(Nil, O (f ::: Nil) (Colimit j d ::: Nil))
     '(Nil, O (f ::: Nil) (Colimit j (O f d) ::: (g ::: Nil)))
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)
||| forall (f :: vk k k').
(HasCompanions hk vk, Ob0 vk k, Ob0 vk k', Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @f
          Sq
  '(Nil, Colimit j d ::: (f ::: Nil))
  '(Nil, Colimit j (O f d) ::: (g ::: (f ::: Nil)))
-> Sq
     '(Nil, Colimit j (O f d) ::: (g ::: (f ::: Nil)))
     '(Nil, Colimit j (O f d) ::: Nil)
-> Sq
     '(O Nil Nil, Colimit j d ::: (f ::: Nil))
     '(O Nil Nil, Colimit j (O f d) ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Obj (Colimit j (O f d))
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil) '(Nil, Colimit j (O f d) ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
Obj f -> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId' Obj (Colimit j (O f d))
c' Sq
  '(Nil, Colimit j (O f d) ::: Nil) '(Nil, Colimit j (O f d) ::: Nil)
-> Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
-> Sq
     '(Nil, O (g ::: (f ::: Nil)) (Colimit j (O f d) ::: Nil))
     '(Nil, O Nil (Colimit j (O f d) ::: Nil))
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)
||| forall (f :: vk k k') (g :: vk k' k).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk k,
 Ob0 vk k') =>
Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk k j).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j,
 Ob0 vk k) =>
Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
counit @f @g
          ((Ob0 vk a, Ob0 vk k', Ob (Colimit j (O f d)),
  Ob (Colimit j (O f d))) =>
 Sq
   '(Nil, Colimit j d ::: (f ::: Nil))
   '(Nil, Colimit j (O f d) ::: Nil))
-> Obj (Colimit j (O f d))
-> Sq
     '(Nil, Colimit j d ::: (f ::: Nil))
     '(Nil, Colimit j (O f d) ::: Nil)
forall (i :: k) (j :: k) (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 (Colimit j (O f d))
c'
          ((Ob0 vk a, Ob0 vk k, Ob (O g (Colimit j (O f d))),
  Ob (O g (Colimit j (O f d)))) =>
 Sq
   '(Nil, Colimit j d ::: (f ::: Nil))
   '(Nil, Colimit j (O f d) ::: Nil))
-> (O g (Colimit j (O f d)) ~> O g (Colimit j (O f d)))
-> Sq
     '(Nil, Colimit j d ::: (f ::: Nil))
     '(Nil, Colimit j (O f d) ::: Nil)
forall (i :: k) (j :: k) (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 Obj g
-> Obj (Colimit j (O f d))
-> O g (Colimit j (O f d)) ~> O g (Colimit j (O f d))
forall {i :: k} (j :: k) (k :: k) (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 (Colimit j (O f d))
c'

-- | The inverse works for any arrow:
--
-- The required square
--
-- > A--c'-K'
-- > |  |  |
-- > | /@\ |
-- > | v v |
-- > A-c-g-K'
--
-- is implemented as
--
-- > A-----c'----K'
-- > | +.d.+.f.+ |
-- > | : v | v : |
-- > | j-@ | | : |
-- > | : v | v : |
-- > A-+-c-+-f-+-K'
leftAdjointPreservesColimitsInv
  :: forall {hk} {vk} {k} {k'} {i} {a} (f :: vk k k') (d :: vk i k) (j :: hk a i)
   . (HasCompanions hk vk, Ob d, Ob f, L.HasColimits vk j k, L.HasColimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a)
  => Sq '(Nil :: Path hk a a, L.Colimit j (f `O` d) ::: Nil) '(Nil, L.Colimit j d ::: f ::: Nil)
leftAdjointPreservesColimitsInv :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {k :: k}
       {k' :: k} {i :: k} {a :: k} (f :: vk k k') (d :: vk i k)
       (j :: hk a i).
(HasCompanions hk vk, Ob d, Ob f, HasColimits vk j k,
 HasColimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a) =>
Sq
  '(Nil, Colimit j (O f d) ::: Nil)
  '(Nil, Colimit j d ::: (f ::: Nil))
leftAdjointPreservesColimitsInv =
  let c :: Obj (Colimit j d)
c = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
Obj (Colimit j d)
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
Obj (Colimit j d)
L.colimitObj @vk @j @k @d; f :: Obj f
f = forall (a :: vk k k'). (CategoryOf (vk k k'), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; d :: Obj d
d = forall (a :: vk i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d
  in forall (j :: hk a i) (d :: vk i k') (p :: vk a k').
(Ob0 vk i, HasColimits vk j k', Ob d, Ob p) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk a i) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, HasColimits vk j k, Ob d, Ob p) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil)
colimitUniv @j @(f `O` d) @(f `O` L.Colimit j d)
        ( Sq '(Nil, O f d ::: Nil) '(Nil, d ::: (f ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit
            Sq '(Nil, O f d ::: Nil) '(Nil, d ::: (f ::: Nil))
-> Sq
     '(j ::: Nil, d ::: (f ::: Nil)) '(Nil, Colimit j d ::: (f ::: Nil))
-> Sq
     '(O Nil (j ::: Nil), O f d ::: Nil)
     '(O Nil Nil, Colimit j d ::: (f ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== forall (j :: hk a i) (d :: vk i k).
(Ob0 vk i, HasColimits vk j k, Ob d) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k}
       {i :: k} {k :: k} (j :: hk a i) (d :: vk i k).
(Ob0 vk i, HasColimits vk j k, Ob d) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
colimit @j @d Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
-> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
-> Sq
     '(j ::: Nil, O (f ::: Nil) (d ::: Nil))
     '(Nil, O (f ::: Nil) (Colimit j d ::: Nil))
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)
||| forall (f :: vk k k').
(HasCompanions hk vk, Ob0 vk k, Ob0 vk k', Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId @f
            Sq '(j ::: Nil, O f d ::: Nil) '(Nil, Colimit j d ::: (f ::: Nil))
-> Sq
     '(Nil, Colimit j d ::: (f ::: Nil))
     '(Nil, O f (Colimit j d) ::: Nil)
-> Sq
     '(O (j ::: Nil) Nil, O f d ::: Nil)
     '(O Nil Nil, O f (Colimit j d) ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq
  '(Nil, Colimit j d ::: (f ::: Nil))
  '(Nil, O f (Colimit j d) ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine
        )
      Sq
  '(Nil, Colimit j (O f d) ::: Nil) '(Nil, O f (Colimit j d) ::: Nil)
-> Sq
     '(Nil, O f (Colimit j d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
-> Sq
     '(O Nil Nil, Colimit j (O f d) ::: Nil)
     '(O Nil Nil, Colimit j d ::: (f ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq
  '(Nil, O f (Colimit j d) ::: Nil)
  '(Nil, Colimit j d ::: (f ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit
      ((Ob0 vk a, Ob0 vk k, Ob (Colimit j d), Ob (Colimit j d)) =>
 Sq
   '(Nil, Colimit j (O f d) ::: Nil)
   '(Nil, Colimit j d ::: (f ::: Nil)))
-> Obj (Colimit j d)
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
forall (i :: k) (j :: k) (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 (Colimit j d)
c
      ((Ob0 vk i, Ob0 vk k', Ob (O f d), Ob (O f d)) =>
 Sq
   '(Nil, Colimit j (O f d) ::: Nil)
   '(Nil, Colimit j d ::: (f ::: Nil)))
-> (O f d ~> O f d)
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
forall (i :: k) (j :: k) (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 Obj f -> Obj d -> O f d ~> O f d
forall {i :: k} (j :: k) (k :: k) (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 d
d
      ((Ob0 vk a, Ob0 vk k', Ob (O f (Colimit j d)),
  Ob (O f (Colimit j d))) =>
 Sq
   '(Nil, Colimit j (O f d) ::: Nil)
   '(Nil, Colimit j d ::: (f ::: Nil)))
-> (O f (Colimit j d) ~> O f (Colimit j d))
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
forall (i :: k) (j :: k) (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 Obj f
-> Obj (Colimit j d) -> O f (Colimit j d) ~> O f (Colimit j d)
forall {i :: k} (j :: k) (k :: k) (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 (Colimit j d)
c

unit
  :: forall {hk} {vk} {j} {k} (f :: vk j k) (g :: vk k j)
   . (Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j, Ob0 vk k)
  => Sq '(Nil :: Path hk j j, Nil) '(Nil, f ::: g ::: Nil)
unit :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk k j).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j,
 Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
unit = Sq '(Nil, Nil) '(Nil, I ::: Nil)
forall {s} (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, I ::: Nil)
vUnitorInv Sq '(Nil, Nil) '(Nil, I ::: Nil)
-> Sq '(Nil, I ::: Nil) '(Nil, O g f ::: Nil)
-> Sq '(O Nil Nil, Nil) '(O Nil Nil, O g f ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== (I ~> O g f) -> Sq '(Nil, I ::: Nil) '(I, O g f ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
(f ~> g) -> Sq '(Nil, f ::: Nil) '(I, g ::: Nil)
vArr (forall (l :: vk j k) (r :: vk 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
Adj.unit @f @g) Sq '(Nil, Nil) '(Nil, O g f ::: Nil)
-> Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
-> Sq '(O Nil Nil, Nil) '(O Nil Nil, f ::: (g ::: Nil))
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit

counit
  :: forall {hk} {vk} {j} {k} (f :: vk j k) (g :: vk k j)
   . (Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j, Ob0 vk k)
  => Sq '(Nil :: Path hk k k, g ::: f ::: Nil) '(Nil, Nil)
counit :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk k j).
(Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j,
 Ob0 vk k) =>
Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
counit = Sq '(Nil, g ::: (f ::: Nil)) '(Nil, O f g ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {i :: k1} {j :: k1}
       {k2 :: k1} (f :: vk i j) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine Sq '(Nil, g ::: (f ::: Nil)) '(Nil, O f g ::: Nil)
-> Sq '(Nil, O f g ::: Nil) '(Nil, I ::: Nil)
-> Sq '(O Nil Nil, g ::: (f ::: Nil)) '(O Nil Nil, I ::: Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== (O f g ~> I) -> Sq '(Nil, O f g ::: Nil) '(I, I ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2) (g :: vk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
(f ~> g) -> Sq '(Nil, f ::: Nil) '(I, g ::: Nil)
vArr (forall (l :: vk j k) (r :: vk 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
Adj.counit @f @g) Sq '(Nil, g ::: (f ::: Nil)) '(Nil, I ::: Nil)
-> Sq '(Nil, I ::: Nil) '(Nil, Nil)
-> Sq '(O Nil Nil, g ::: (f ::: Nil)) '(O Nil Nil, Nil)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
=== Sq '(Nil, I ::: Nil) '(Nil, Nil)
forall {k1} (hk :: CAT k1) (vk :: CAT k1) (k2 :: k1).
(HasCompanions hk vk, Ob0 vk k2) =>
Sq '(Nil, I ::: Nil) '(Nil, Nil)
vUnitor