{-# 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 (..), Strictified (..), st)
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..), flipCompanionInv, flipConjoint)
import Proarrow.Category.Equipment.Limit qualified as L
import Proarrow.Core (CategoryOf (..), obj)
import Proarrow.Squares
  ( fromLeft
  , fromRight
  , hArr
  , toLeft
  , toRight
  , vArr
  , vCombine
  , vId
  , vSplit
  , vUnitor
  , vUnitorInv
  , (===)
  , (|||)
  )
import Prelude (($))

-- | 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, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, HasLimits vk j k, Ob d) =>
Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
limit =
  forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
L.withObLimit @vk @j @_ @d ((Ob (Limit j d) =>
  Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
 -> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> (Ob (Limit j d) =>
    Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
forall a b. (a -> b) -> a -> b
$
    forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @d ((Ob (Companion hk d) =>
  Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
 -> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> (Ob (Companion hk d) =>
    Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
forall a b. (a -> b) -> a -> b
$
      forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @(L.Limit j d) ((Ob (Companion hk (Limit j d)) =>
  Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
 -> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> (Ob (Companion hk (Limit j d)) =>
    Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil))
-> Sq '(j ::: Nil, Limit j d ::: Nil) '(Nil, d ::: Nil)
forall a b. (a -> b) -> a -> b
$
        (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 ((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))
-> (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 a b. (a -> b) -> a -> b
$
          forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path hk i k) (qs :: Path hk i k).
(Bicategory hk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @(j ::: Companion hk (L.Limit j d) ::: Nil) @(Companion hk d ::: Nil)
            (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)

-- | 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 :: hk a k)
   . (Ob0 vk i, Ob0 vk a, L.HasLimits vk j k, Ob d, Ob p)
  => Sq '(j ::: p ::: Nil, Nil) '(Nil, d ::: Nil)
  -> Sq '(p ::: Nil, 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 :: hk a k).
(Ob0 vk i, Ob0 vk a, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: (p ::: Nil), Nil) '(Nil, d ::: Nil)
-> Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil)
limitUniv (Sq (Str SPath (j ::: (p ::: Nil))
_ SPath (Companion hk d ::: Nil)
_ Fold (j ::: (p ::: Nil)) ~> Fold (Companion hk d ::: Nil)
n)) =
  forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
L.withObLimit @vk @j @k @d ((Ob (Limit j d) => Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil))
 -> Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil))
-> (Ob (Limit j d) =>
    Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil))
-> Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$
    (p ~> Companion hk (Limit j d))
-> Sq '(p ::: Nil, Nil) '(Companion hk (Limit j d) ::: Nil, Nil)
forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type}
       {j :: k1} {k2 :: k1} (p :: hk j k2) (q :: hk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
(p ~> q) -> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
hArr (forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) (p :: hk a k).
(HasLimits vk j k, Ob d, Ob p) =>
(O p j ~> Companion hk d) -> p ~> Companion hk (Limit j d)
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k)
       (p :: hk a k).
(HasLimits vk j k, Ob d, Ob p) =>
(O p j ~> Companion hk d) -> p ~> Companion hk (Limit j d)
L.limitUniv @vk @j @k @d @p O p j ~> Companion hk d
Fold (j ::: (p ::: Nil)) ~> Fold (Companion hk d ::: Nil)
n) Sq '(p ::: Nil, Nil) '(Companion hk (Limit j d) ::: Nil, Nil)
-> Sq
     '(Companion hk (Limit j d) ::: Nil, Nil) '(Nil, Limit j d ::: Nil)
-> Sq '(p ::: Nil, Nil +++ Nil) '(Nil, Nil +++ (Limit j d ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| Sq
  '(Companion hk (Limit j d) ::: Nil, Nil) '(Nil, Limit j d ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
fromLeft ((Ob0 hk i, Ob0 hk k, Ob (O p j), Ob (Companion hk d)) =>
 Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil))
-> (O p j ~> Companion hk d)
-> Sq '(p ::: Nil, 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 p j ~> Companion hk d
Fold (j ::: (p ::: Nil)) ~> Fold (Companion hk d ::: Nil)
n

limitUniv'
  :: forall {hk} {vk} {a} {i} {k} (j :: hk i a) (d :: vk i k) (p :: vk a k)
   . (Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, 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 '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
n =
  forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @p ((Ob (Companion hk p) =>
  Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil))
 -> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil))
-> (Ob (Companion hk p) =>
    Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil))
-> Sq '(Nil, p ::: Nil) '(Nil, Limit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$
    Sq '(Nil, p ::: Nil) '(Companion hk p ::: Nil, Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob' f) =>
Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
toRight Sq '(Nil, p ::: Nil) '(Companion hk p ::: Nil, Nil)
-> Sq '(Companion hk p ::: Nil, Nil) '(Nil, Limit j d ::: Nil)
-> Sq
     '(Nil, (p ::: Nil) +++ Nil) '(Nil, Nil +++ (Limit j d ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| (forall (j :: hk i a) (d :: vk i k) (p :: hk a k).
(Ob0 vk i, Ob0 vk a, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: (p ::: Nil), Nil) '(Nil, d ::: Nil)
-> Sq '(p ::: Nil, 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 :: hk a k).
(Ob0 vk i, Ob0 vk a, HasLimits vk j k, Ob d, Ob p) =>
Sq '(j ::: (p ::: Nil), Nil) '(Nil, d ::: Nil)
-> Sq '(p ::: Nil, Nil) '(Nil, Limit j d ::: Nil)
limitUniv @j @d @(Companion hk p) (Sq '(Companion hk p ::: Nil, Nil) '(Nil, p ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
fromLeft Sq '(Companion hk p ::: Nil, Nil) '(Nil, p ::: Nil)
-> Sq '(j ::: Nil, p ::: Nil) '(Nil, d ::: Nil)
-> Sq
     '((j ::: Nil) +++ (Companion hk p ::: Nil), Nil)
     '(Nil +++ Nil, d ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== Sq '(j ::: Nil, p ::: Nil) '(Nil, 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 =
  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 k) {i :: k} {j :: k} {k :: k} (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 @_ @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)))
-> (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 a b. (a -> b) -> a -> b
$
    forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
L.withObLimit @_ @j @_ @(g `O` d) ((Ob (Limit j (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)))
-> (Ob (Limit j (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 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 k) {i :: k} {j :: k} {k :: k} (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 @_ @f @(L.Limit j (g `O` d)) ((Ob (O f (Limit j (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)))
-> (Ob (O f (Limit j (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 a b. (a -> b) -> a -> b
$
        forall (f :: vk a k').
(HasCompanions hk vk, Ob0 vk a, 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 @(L.Limit j (g `O` d)) Sq '(Nil, Limit j (O g d) ::: Nil) '(Nil, Limit j (O g d) ::: Nil)
-> Sq '(Nil, Nil) '(Nil, f ::: (g ::: Nil))
-> Sq
     '(Nil, (Limit j (O g d) ::: Nil) +++ Nil)
     '(Nil, (Limit j (O g d) ::: Nil) +++ (f ::: (g ::: Nil)))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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) ::: Nil) +++ (f ::: (g ::: Nil)))
-> Sq
     '(Nil, (Limit j (O g d) ::: Nil) +++ (f ::: (g ::: Nil)))
     '(Nil, Limit j d ::: (g ::: Nil))
-> Sq
     '(Nil +++ Nil, Limit j (O g d) ::: Nil)
     '(Nil +++ Nil, Limit j d ::: (g ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== ( 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
     '(Nil +++ Nil, Limit j (O g d) ::: (f ::: Nil))
     '(Nil +++ Nil, Limit j d ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== forall (j :: hk i a) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, 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
     '((j ::: Nil) +++ Nil, O f (Limit j (O g d)) ::: Nil)
     '(Nil +++ Nil, d ::: (g ::: (f ::: Nil)))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== (forall (j :: hk i a) (d :: vk i k').
(Ob0 vk i, Ob0 vk a, Ob0 vk k', 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, Ob0 vk a, Ob0 vk k, 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
     '(Nil +++ (j ::: Nil), Limit j (O g d) ::: Nil)
     '(Nil +++ Nil, d ::: (g ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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, (Limit j (O g d) ::: Nil) +++ (f ::: Nil))
     '(Nil, (d ::: (g ::: Nil)) +++ (f ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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
     '(Nil +++ (j ::: Nil), O f (Limit j (O g d)) ::: Nil)
     '(Nil +++ Nil, d ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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, (d ::: Nil) +++ (g ::: (f ::: Nil)))
     '(Nil, (d ::: Nil) +++ Nil)
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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, (Limit j (O g d) ::: (f ::: Nil)) +++ (g ::: Nil))
     '(Nil, (Limit j d ::: Nil) +++ (g ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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

-- | 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 =
  forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
forall (vk :: CAT k) (j :: hk i a) (k :: k) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
L.withObLimit @vk @j @k @d ((Ob (Limit j d) =>
  Sq
    '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
 -> Sq
      '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> (Ob (Limit j d) =>
    Sq
      '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> Sq
     '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
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 k) {i :: k} {j :: k} {k :: k} (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 @d ((Ob (O g d) =>
  Sq
    '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
 -> Sq
      '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> (Ob (O g d) =>
    Sq
      '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> Sq
     '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
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 k) {i :: k} {j :: k} {k :: k} (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 @(L.Limit j d) ((Ob (O g (Limit j d)) =>
  Sq
    '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
 -> Sq
      '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> (Ob (O g (Limit j d)) =>
    Sq
      '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil))
-> Sq
     '(Nil, Limit j d ::: (g ::: Nil)) '(Nil, Limit j (O g d) ::: Nil)
forall a b. (a -> b) -> a -> b
$
        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
     '(Nil +++ Nil, Limit j d ::: (g ::: Nil))
     '(Nil +++ Nil, Limit j (O g d) ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== forall (j :: hk i a) (d :: vk i k') (p :: vk a k').
(Ob0 vk i, Ob0 vk a, Ob0 vk k', 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, Ob0 vk a, Ob0 vk k, 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
     '((j ::: Nil) +++ Nil, O g (Limit j d) ::: Nil)
     '(Nil +++ Nil, d ::: (g ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== forall (j :: hk i a) (d :: vk i k).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, 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, (Limit j d ::: Nil) +++ (g ::: Nil))
     '(Nil, (d ::: Nil) +++ (g ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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
     '(Nil +++ (j ::: Nil), O g (Limit j d) ::: Nil)
     '(Nil +++ Nil, O g d ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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
            )

-- | The projection into the @j@-weighted colimit @c@ of @d@.
--
-- > I--d--K
-- > |  v  |
-- > j--@  |
-- > |  v  |
-- > A--c--K
colimit
  :: forall {hk} {vk} {a} {i} {k} (j :: hk a i) (d :: vk i k)
   . (Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, HasColimits vk j k, Ob d) =>
Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
colimit =
  forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
L.withObColimit @vk @j @_ @d ((Ob (Colimit j d) =>
  Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
 -> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> (Ob (Colimit j d) =>
    Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$
    forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @d ((Ob (Companion hk d) =>
  Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
 -> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> (Ob (Companion hk d) =>
    Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$
      forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @(L.Colimit j d) ((Ob (Companion hk (Colimit j d)) =>
  Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
 -> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> (Ob (Companion hk (Colimit j d)) =>
    Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil))
-> Sq '(j ::: Nil, d ::: Nil) '(Nil, Colimit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$
        (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 ((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))
-> (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 a b. (a -> b) -> a -> b
$
          forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path hk a k) (qs :: Path hk a k).
(Bicategory hk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @(j ::: Companion hk d ::: Nil) @(Companion hk (L.Colimit j d) ::: Nil)
            ( forall (f :: vk i k) (p :: hk a i) (q :: hk a k).
(Equipment hk vk, Ob q) =>
Obj f -> (p ~> O (Conjoint hk f) q) -> O (Companion hk f) p ~> q
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 @d @j @(Companion hk (L.Colimit j d)) Obj d
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj ((j ~> O (Conjoint hk d) (Companion hk (Colimit j d)))
 -> O (Companion hk d) j ~> Companion hk (Colimit j d))
-> (j ~> O (Conjoint hk d) (Companion hk (Colimit j d)))
-> O (Companion hk d) j ~> Companion hk (Colimit j d)
forall a b. (a -> b) -> a -> b
$
                forall (f :: vk a k) (p :: hk a i) (q :: hk k i).
(Equipment hk vk, Ob p) =>
Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
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 p) =>
Obj f -> (O p (Conjoint hk f) ~> q) -> p ~> O q (Companion hk f)
flipConjoint @(L.Colimit j d) @j @(Conjoint hk d) Obj (Colimit j d)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj ((O j (Conjoint hk (Colimit j d)) ~> Conjoint hk d)
 -> j ~> O (Conjoint hk d) (Companion hk (Colimit j d)))
-> (O j (Conjoint hk (Colimit j d)) ~> Conjoint hk d)
-> j ~> O (Conjoint hk d) (Companion hk (Colimit j d))
forall a b. (a -> b) -> a -> b
$
                  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 j (Conjoint hk (Colimit j d)) ~> Conjoint hk d
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k).
(HasColimits vk j k, Ob d) =>
O j (Conjoint hk (Colimit j d)) ~> Conjoint hk d
L.colimit @vk @j @k @d
            )

-- | 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 :: hk k a)
   . (Ob0 vk i, Ob0 vk a, Ob0 vk k, L.HasColimits vk j k, Ob d, Ob p)
  => Sq '(p ::: j ::: Nil, d ::: Nil) '(Nil, Nil)
  -> Sq '(p ::: Nil, L.Colimit j d ::: Nil) '(Nil, 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 :: hk k a).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, HasColimits vk j k, Ob d, Ob p) =>
Sq '(p ::: (j ::: Nil), d ::: Nil) '(Nil, Nil)
-> Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil)
colimitUniv Sq '(p ::: (j ::: Nil), d ::: Nil) '(Nil, Nil)
sq = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
L.withObColimit @vk @j @_ @d ((Ob (Colimit j d) =>
  Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil))
 -> Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil))
-> (Ob (Colimit j d) =>
    Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil))
-> Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil)
forall a b. (a -> b) -> a -> b
$
  case (Sq '(Nil, Nil) '(Conjoint hk d ::: Nil, d ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
fromRight Sq '(Nil, Nil) '(Conjoint hk d ::: Nil, d ::: Nil)
-> Sq '(p ::: (j ::: Nil), d ::: Nil) '(Nil, Nil)
-> Sq
     '((p ::: (j ::: Nil)) +++ Nil, Nil)
     '(Nil +++ (Conjoint hk d ::: Nil), Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== Sq '(p ::: (j ::: Nil), d ::: Nil) '(Nil, Nil)
sq) of
    Sq (Str SPath (p ::: (j ::: Nil))
_ SPath (Conjoint hk d ::: Nil)
_ Fold (p ::: (j ::: Nil)) ~> Fold (Conjoint hk d ::: Nil)
n) -> (p ~> Conjoint hk (Colimit j d))
-> Sq '(p ::: Nil, Nil) '(Conjoint hk (Colimit j d) ::: Nil, Nil)
forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type}
       {j :: k1} {k2 :: k1} (p :: hk j k2) (q :: hk j k2).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) =>
(p ~> q) -> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
hArr (forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k) (p :: hk k a).
(HasColimits vk j k, Ob d, Ob p) =>
(O j p ~> Conjoint hk d) -> p ~> Conjoint hk (Colimit j d)
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k)
       (p :: hk k a).
(HasColimits vk j k, Ob d, Ob p) =>
(O j p ~> Conjoint hk d) -> p ~> Conjoint hk (Colimit j d)
L.colimitUniv @vk @j @k @d @p O j p ~> Conjoint hk d
Fold (p ::: (j ::: Nil)) ~> Fold (Conjoint hk d ::: Nil)
n) Sq '(p ::: Nil, Nil) '(Conjoint hk (Colimit j d) ::: Nil, Nil)
-> Sq
     '(Conjoint hk (Colimit j d) ::: Nil, Colimit j d ::: Nil)
     '(Nil, Nil)
-> Sq
     '(p ::: Nil, Nil +++ (Colimit j d ::: Nil)) '(Nil, Nil +++ Nil)
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| Sq
  '(Conjoint hk (Colimit j d) ::: Nil, Colimit j d ::: Nil)
  '(Nil, Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
toLeft ((Ob0 hk k, Ob0 hk i, Ob (O j p), Ob (Conjoint hk d)) =>
 Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil))
-> (O j p ~> Conjoint hk d)
-> Sq '(p ::: Nil, Colimit j d ::: Nil) '(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
\\\ O j p ~> Conjoint hk d
Fold (p ::: (j ::: Nil)) ~> Fold (Conjoint hk d ::: Nil)
n

colimitUniv'
  :: forall {hk} {vk} {a} {i} {k} (j :: hk a i) (d :: vk i k) (p :: vk a k)
   . (Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, 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 '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
n = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) r.
(Equipment hk vk, Ob f) =>
(Ob (Conjoint hk f) => r) -> r
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       r.
(Equipment hk vk, Ob f) =>
(Ob (Conjoint hk f) => r) -> r
withObConjoint @hk @vk @p ((Ob (Conjoint hk p) =>
  Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil))
 -> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil))
-> (Ob (Conjoint hk p) =>
    Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil))
-> Sq '(Nil, Colimit j d ::: Nil) '(Nil, p ::: Nil)
forall a b. (a -> b) -> a -> b
$
  Sq '(Nil, Nil) '(Conjoint hk p ::: Nil, p ::: Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
fromRight Sq '(Nil, Nil) '(Conjoint hk p ::: Nil, p ::: Nil)
-> Sq '(Conjoint hk p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil)
-> Sq
     '(Nil, Nil +++ (Colimit j d ::: Nil)) '(Nil, (p ::: Nil) +++ Nil)
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| (forall (j :: hk a i) (d :: vk i k) (p :: hk k a).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, HasColimits vk j k, Ob d, Ob p) =>
Sq '(p ::: (j ::: Nil), d ::: Nil) '(Nil, Nil)
-> Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, 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 :: hk k a).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, HasColimits vk j k, Ob d, Ob p) =>
Sq '(p ::: (j ::: Nil), d ::: Nil) '(Nil, Nil)
-> Sq '(p ::: Nil, Colimit j d ::: Nil) '(Nil, Nil)
colimitUniv @j @d @(Conjoint hk p) (Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
n Sq '(j ::: Nil, d ::: Nil) '(Nil, p ::: Nil)
-> Sq '(Conjoint hk p ::: Nil, p ::: Nil) '(Nil, Nil)
-> Sq
     '((Conjoint hk p ::: Nil) +++ (j ::: Nil), d ::: Nil)
     '(Nil +++ Nil, Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== Sq '(Conjoint hk p ::: Nil, p ::: Nil) '(Nil, Nil)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (f :: vk j k2).
(Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) =>
Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
toLeft))

-- | 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 =
  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 k) {i :: k} {j :: k} {k :: k} (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 @_ @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))
-> (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 a b. (a -> b) -> a -> b
$
    forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
L.withObColimit @vk @j @k' @(f `O` d) ((Ob (Colimit j (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))
-> (Ob (Colimit j (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 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 k) {i :: k} {j :: k} {k :: k} (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 @_ @g @(L.Colimit j (f `O` d)) ((Ob (O g (Colimit j (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))
-> (Ob (O g (Colimit j (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 a b. (a -> b) -> a -> b
$
        ( forall (j :: hk a i) (d :: vk i k) (p :: vk a k).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, 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, (d ::: Nil) +++ Nil)
     '(Nil, (d ::: Nil) +++ (f ::: (g ::: Nil)))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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
     '((j ::: Nil) +++ Nil, d ::: Nil)
     '(Nil +++ Nil, Colimit j (O f d) ::: (g ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== (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
     '((j ::: Nil) +++ Nil, d ::: (f ::: Nil))
     '(Nil +++ Nil, Colimit j (O f d) ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== forall (j :: hk a i) (d :: vk i k').
(Ob0 vk i, Ob0 vk a, Ob0 vk k', 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, Ob0 vk a, Ob0 vk k, 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, (d ::: (f ::: Nil)) +++ (g ::: Nil))
     '(Nil, (Colimit j (O f d) ::: Nil) +++ (g ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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
     '(Nil +++ (j ::: Nil), d ::: Nil)
     '(Nil +++ Nil, O g (Colimit j (O f d)) ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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
     '(Nil +++ Nil, Colimit j d ::: Nil)
     '(Nil +++ Nil, Colimit j (O f d) ::: (g ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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, (Colimit j d ::: Nil) +++ (f ::: Nil))
     '(Nil, (Colimit j (O f d) ::: (g ::: Nil)) +++ (f ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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
     '(Nil +++ Nil, Colimit j d ::: (f ::: Nil))
     '(Nil +++ Nil, Colimit j (O f d) ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== forall (f :: vk a k').
(HasCompanions hk vk, Ob0 vk a, 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 @(L.Colimit j (f `O` d)) Sq
  '(Nil, Colimit j (O f d) ::: Nil) '(Nil, Colimit j (O f d) ::: Nil)
-> Sq '(Nil, g ::: (f ::: Nil)) '(Nil, Nil)
-> Sq
     '(Nil, (Colimit j (O f d) ::: Nil) +++ (g ::: (f ::: Nil)))
     '(Nil, (Colimit j (O f d) ::: Nil) +++ Nil)
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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

-- | 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 =
  forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk a i) (k :: s) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
forall (vk :: CAT k) (j :: hk a i) (k :: k) (d :: vk i k) r.
(HasColimits vk j k, Ob d) =>
(Ob (Colimit j d) => r) -> r
L.withObColimit @vk @j @k @d ((Ob (Colimit j d) =>
  Sq
    '(Nil, Colimit j (O f d) ::: Nil)
    '(Nil, Colimit j d ::: (f ::: Nil)))
 -> Sq
      '(Nil, Colimit j (O f d) ::: Nil)
      '(Nil, Colimit j d ::: (f ::: Nil)))
-> (Ob (Colimit j d) =>
    Sq
      '(Nil, Colimit j (O f d) ::: Nil)
      '(Nil, Colimit j d ::: (f ::: Nil)))
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
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 k) {i :: k} {j :: k} {k :: k} (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
    '(Nil, Colimit j (O f d) ::: Nil)
    '(Nil, Colimit j d ::: (f ::: Nil)))
 -> Sq
      '(Nil, Colimit j (O f d) ::: Nil)
      '(Nil, Colimit j d ::: (f ::: Nil)))
-> (Ob (O f d) =>
    Sq
      '(Nil, Colimit j (O f d) ::: Nil)
      '(Nil, Colimit j d ::: (f ::: Nil)))
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
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 k) {i :: k} {j :: k} {k :: k} (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 @(L.Colimit j d) ((Ob (O f (Colimit j d)) =>
  Sq
    '(Nil, Colimit j (O f d) ::: Nil)
    '(Nil, Colimit j d ::: (f ::: Nil)))
 -> Sq
      '(Nil, Colimit j (O f d) ::: Nil)
      '(Nil, Colimit j d ::: (f ::: Nil)))
-> (Ob (O f (Colimit j d)) =>
    Sq
      '(Nil, Colimit j (O f d) ::: Nil)
      '(Nil, Colimit j d ::: (f ::: Nil)))
-> Sq
     '(Nil, Colimit j (O f d) ::: Nil)
     '(Nil, Colimit j d ::: (f ::: Nil))
forall a b. (a -> b) -> a -> b
$
        forall (j :: hk a i) (d :: vk i k') (p :: vk a k').
(Ob0 vk i, Ob0 vk a, Ob0 vk k', 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, Ob0 vk a, Ob0 vk k, 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
     '((j ::: Nil) +++ Nil, O f d ::: Nil)
     '(Nil +++ Nil, Colimit j d ::: (f ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== forall (j :: hk a i) (d :: vk i k).
(Ob0 vk i, Ob0 vk a, Ob0 vk k, 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, Ob0 vk a, Ob0 vk k, 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, (d ::: Nil) +++ (f ::: Nil))
     '(Nil, (Colimit j d ::: Nil) +++ (f ::: Nil))
forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1}
       {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l)
       (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h)
       (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| 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
     '(Nil +++ (j ::: Nil), O f d ::: Nil)
     '(Nil +++ Nil, O f (Colimit j d) ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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
     '(Nil +++ Nil, Colimit j (O f d) ::: Nil)
     '(Nil +++ Nil, Colimit j d ::: (f ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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

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 '(Nil +++ Nil, Nil) '(Nil +++ Nil, O g f ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== (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 '(Nil +++ Nil, Nil) '(Nil +++ Nil, f ::: (g ::: Nil))
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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 '(Nil +++ Nil, g ::: (f ::: Nil)) '(Nil +++ Nil, I ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== (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 '(Nil +++ Nil, g ::: (f ::: Nil)) '(Nil +++ Nil, Nil)
forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1}
       {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j)
       (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i)
       (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== 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