{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares.Limit where

import Prelude (($))

import Proarrow.Category.Bicategory
  ( Adjunction
  , Bicategory (..)
  )
import Proarrow.Category.Bicategory qualified as Adj
import Proarrow.Category.Bicategory.Strictified (Path (..), Strictified (..))
import Proarrow.Category.Equipment (Equipment, IsCotight, IsTight, Tight, withObO2)
import Proarrow.Category.Equipment.Limit qualified as L
import Proarrow.Core (CategoryOf (..))
import Proarrow.Squares
  ( Sq
  , Sq' (..)
  , fromLeft
  , hArr
  , hCombineAll
  , hId
  , hSplitAll
  , toRight
  , (===)
  , (|||)
  )

-- | The projection out of the @j@-weighted limit @l@ of @d@.
--
-- > K-----K
-- > l>\   |
-- > |  @->d
-- > j-/   |
-- > I-----I
limit
  :: forall {kk} {a} {i} {k} (j :: kk i a) (d :: kk i k)
   . (L.HasLimits j k, IsTight d)
  => Sq (j ::: L.Limit j d ::: Nil) (d ::: Nil) Nil Nil
limit :: forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k).
(HasLimits j k, IsTight d) =>
Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
limit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @d (((Ob0 kk i, Ob0 kk k) =>
  Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
 -> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> ((Ob0 kk i, Ob0 kk k) =>
    Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @j (((Ob0 kk i, Ob0 kk a) =>
  Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
 -> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> ((Ob0 kk i, Ob0 kk a) =>
    Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ forall (j :: kk i a) (k :: k) (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
L.withObLimit @j @k @d ((IsTight (Limit j d) =>
  Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
 -> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> (IsTight (Limit j d) =>
    Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (O Nil (j ::: (Limit j d ::: Nil)) ~> O (d ::: Nil) Nil)
-> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((O Nil (j ::: (Limit j d ::: Nil)) ~> O (d ::: Nil) Nil)
 -> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil)
-> (O Nil (j ::: (Limit j d ::: Nil)) ~> O (d ::: Nil) Nil)
-> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (Fold (j ::: (Limit j d ::: Nil)) ~> Fold (d ::: Nil))
-> Strictified (j ::: (Limit j d ::: Nil)) (d ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St ((Fold (j ::: (Limit j d ::: Nil)) ~> Fold (d ::: Nil))
 -> Strictified (j ::: (Limit j d ::: Nil)) (d ::: Nil))
-> (Fold (j ::: (Limit j d ::: Nil)) ~> Fold (d ::: Nil))
-> Strictified (j ::: (Limit j d ::: Nil)) (d ::: Nil)
forall a b. (a -> b) -> a -> b
$ forall (j :: kk i a) (k :: k) (d :: kk i k).
(HasLimits j k, IsTight d) =>
O (Limit j d) j ~> d
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k).
(HasLimits j k, IsTight d) =>
O (Limit j d) j ~> d
L.limit @j

-- | The universal property of the limit.
--
-- The dotted inner square is the input square, the outer square is the output square.
--
-- > A---------K
-- > | K.....K |
-- > p---\   : |
-- > | :  @->d l
-- > | j-/   : |
-- > | I.....I |
-- > A---------A
limitUniv
  :: forall {kk} {a} {i} {k} (j :: kk i a) (d :: kk i k) (p :: kk a k)
   . (L.HasLimits j k, IsTight d, Ob p)
  => Sq (j ::: p ::: Nil) (d ::: Nil) Nil Nil
  -> Sq (p ::: Nil) (L.Limit j d ::: Nil) Nil Nil
limitUniv :: forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
limitUniv (Sq (St Fold (j ::: (p ::: Nil)) ~> Fold (d ::: Nil)
n)) = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @j (((Ob0 kk i, Ob0 kk a) =>
  Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
 -> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
-> ((Ob0 kk i, Ob0 kk a) =>
    Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ forall (j :: kk i a) (k :: k) (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
L.withObLimit @j @k @d ((IsTight (Limit j d) =>
  Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
 -> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
-> (IsTight (Limit j d) =>
    Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (O Nil (p ::: Nil) ~> O (Limit j d ::: Nil) Nil)
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((O Nil (p ::: Nil) ~> O (Limit j d ::: Nil) Nil)
 -> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil)
-> (O Nil (p ::: Nil) ~> O (Limit j d ::: Nil) Nil)
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (Fold (p ::: Nil) ~> Fold (Limit j d ::: Nil))
-> Strictified (p ::: Nil) (Limit j d ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St ((Fold (p ::: Nil) ~> Fold (Limit j d ::: Nil))
 -> Strictified (p ::: Nil) (Limit j d ::: Nil))
-> (Fold (p ::: Nil) ~> Fold (Limit j d ::: Nil))
-> Strictified (p ::: Nil) (Limit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$ forall (j :: kk i a) (k :: k) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
(O p j ~> d) -> p ~> Limit j d
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
(O p j ~> d) -> p ~> Limit j d
L.limitUniv @j O (Fold (p ::: Nil)) j ~> d
Fold (j ::: (p ::: Nil)) ~> Fold (d ::: Nil)
n

-- |
--
-- > A-+--p--+-K
-- > | :  v  : |
-- > | j--@  : |
-- > | :  v  : |
-- > | I..d..K |
-- > A----l----K
limitUniv'
  :: forall {kk} {a} {i} {k} (j :: kk i a) (d :: kk i k) (p :: kk a k)
   . (L.HasLimits j k, IsTight d, IsTight p)
  => Sq (j ::: Nil) Nil (p ::: Nil) (d ::: Nil)
  -> Sq Nil Nil (p ::: Nil) (L.Limit j d ::: Nil)
limitUniv' :: forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, IsTight p) =>
Sq (j ::: Nil) Nil (p ::: Nil) (d ::: Nil)
-> Sq Nil Nil (p ::: Nil) (Limit j d ::: Nil)
limitUniv' Sq (j ::: Nil) Nil (p ::: Nil) (d ::: Nil)
n = forall (j :: kk i a) (k :: k) (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
L.withObLimit @j @k @d ((IsTight (Limit j d) =>
  Sq Nil Nil (p ::: Nil) (Limit j d ::: Nil))
 -> Sq Nil Nil (p ::: Nil) (Limit j d ::: Nil))
-> (IsTight (Limit j d) =>
    Sq Nil Nil (p ::: Nil) (Limit j d ::: Nil))
-> Sq Nil Nil (p ::: Nil) (Limit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$ Sq Nil (p ::: Nil) (p ::: Nil) Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (f :: kk j k2).
(Equipment kk, IsTight f) =>
Sq Nil (f ::: Nil) (f ::: Nil) Nil
toRight Sq Nil (p ::: Nil) (p ::: Nil) Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
-> Sq Nil (Limit j d ::: Nil) ((p ::: Nil) +++ Nil) (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| forall (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
limitUniv @j @d @p (Sq (p ::: Nil) Nil Nil (p ::: Nil)
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (f :: kk j k2).
(Equipment kk, IsTight f) =>
Sq (f ::: Nil) Nil Nil (f ::: Nil)
fromLeft Sq (p ::: Nil) Nil Nil (p ::: Nil)
-> Sq (j ::: Nil) Nil (p ::: Nil) (d ::: Nil)
-> Sq ((j ::: Nil) +++ (p ::: Nil)) (Nil +++ Nil) Nil (d ::: Nil)
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq (j ::: Nil) Nil (p ::: Nil) (d ::: Nil)
n Sq' '(j ::: (p ::: Nil), SUB Nil) '(Nil, SUB (d ::: Nil))
-> Sq Nil (d ::: Nil) (d ::: Nil) Nil
-> Sq (Nil +++ (j ::: (p ::: Nil))) ((d ::: Nil) +++ Nil) Nil Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq Nil (d ::: Nil) (d ::: Nil) Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (f :: kk j k2).
(Equipment kk, IsTight f) =>
Sq Nil (f ::: Nil) (f ::: Nil) Nil
toRight) Sq' '(Nil, SUB (p ::: Nil)) '(Limit j d ::: Nil, SUB Nil)
-> Sq (Limit j d ::: Nil) Nil Nil (Limit j d ::: Nil)
-> Sq Nil Nil ((p ::: Nil) +++ Nil) (Nil +++ (Limit j d ::: Nil))
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| Sq (Limit j d ::: Nil) Nil Nil (Limit j d ::: Nil)
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (f :: kk j k2).
(Equipment kk, IsTight f) =>
Sq (f ::: Nil) Nil Nil (f ::: Nil)
fromLeft

-- | 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 {kk} {k} {k'} {i} {a} (f :: kk k' k) (g :: kk k k') (d :: kk i k) (j :: kk i a)
   . ( Adjunction f g
     , Equipment kk
     , IsTight d
     , IsTight f
     , IsTight g
     , L.HasLimits j k
     , L.HasLimits j k'
     )
  => Sq (L.Limit j (g `O` d) ::: Nil) (L.Limit j d ::: g ::: Nil) Nil Nil
rightAdjointPreservesLimits :: forall {k} {kk :: k -> k -> Type} {k :: k} {k' :: k} {i :: k}
       {a :: k} (f :: kk k' k) (g :: kk k k') (d :: kk i k) (j :: kk i a).
(Adjunction f g, Equipment kk, IsTight d, IsTight f, IsTight g,
 HasLimits j k, HasLimits j k') =>
Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil
rightAdjointPreservesLimits =
  forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @g (((Ob0 kk k, Ob0 kk k') =>
  Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
 -> Sq
      (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> ((Ob0 kk k, Ob0 kk k') =>
    Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil
forall a b. (a -> b) -> a -> b
$
    forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @j (((Ob0 kk i, Ob0 kk a) =>
  Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
 -> Sq
      (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> ((Ob0 kk i, Ob0 kk a) =>
    Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil
forall a b. (a -> b) -> a -> b
$
      forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @_ @g @d (((IsOb Tight (O g d), Ob (O g d)) =>
  Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
 -> Sq
      (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> ((IsOb Tight (O g d), Ob (O g d)) =>
    Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil
forall a b. (a -> b) -> a -> b
$
        forall (j :: kk i a) (k :: k) (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
L.withObLimit @j @_ @(g `O` d) ((IsTight (Limit j (O g d)) =>
  Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
 -> Sq
      (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> (IsTight (Limit j (O g d)) =>
    Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil
forall a b. (a -> b) -> a -> b
$
          forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @_ @f @(L.Limit j (g `O` d)) (((IsOb Tight (O f (Limit j (O g d))),
   Ob (O f (Limit j (O g d)))) =>
  Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
 -> Sq
      (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> ((IsOb Tight (O f (Limit j (O g d))),
     Ob (O f (Limit j (O g d)))) =>
    Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil)
-> Sq (Limit j (O g d) ::: Nil) (Limit j d ::: (g ::: Nil)) Nil Nil
forall a b. (a -> b) -> a -> b
$
            (forall (f :: kk k' k) (g :: kk k k').
(Adjunction f g, Equipment kk) =>
Sq Nil (f ::: (g ::: Nil)) Nil Nil
forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (g :: kk k j).
(Adjunction f g, Equipment kk) =>
Sq Nil (f ::: (g ::: Nil)) Nil Nil
unit @f @g Sq Nil (f ::: (g ::: Nil)) Nil Nil
-> Sq (Limit j (O g d) ::: Nil) (Limit j (O g d) ::: Nil) Nil Nil
-> Sq
     ((Limit j (O g d) ::: Nil) +++ Nil)
     ((Limit j (O g d) ::: Nil) +++ (f ::: (g ::: Nil)))
     Nil
     Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq (Limit j (O g d) ::: Nil) (Limit j (O g d) ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId)
              Sq'
  '(Limit j (O g d) ::: Nil, SUB Nil)
  '(Limit j (O g d) ::: (f ::: (g ::: Nil)), SUB Nil)
-> Sq
     (Limit j (O g d) ::: (f ::: (g ::: Nil)))
     (Limit j d ::: (g ::: Nil))
     Nil
     Nil
-> Sq
     (Limit j (O g d) ::: Nil)
     (Limit j d ::: (g ::: Nil))
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| ( Sq (g ::: Nil) (g ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId
                      Sq (g ::: Nil) (g ::: Nil) Nil Nil
-> Sq (Limit j (O g d) ::: (f ::: Nil)) (Limit j d ::: Nil) Nil Nil
-> Sq
     ((Limit j (O g d) ::: (f ::: Nil)) +++ (g ::: Nil))
     ((Limit j d ::: Nil) +++ (g ::: Nil))
     Nil
     Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== ( forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
forall (ps :: Path kk a k).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll @(L.Limit j (g `O` d) ::: f ::: Nil)
                              Sq'
  '(Limit j (O g d) ::: (f ::: Nil), SUB Nil)
  '(O f (Limit j (O g d)) ::: Nil, SUB Nil)
-> Sq (O f (Limit j (O g d)) ::: Nil) (Limit j d ::: Nil) Nil Nil
-> Sq
     (Limit j (O g d) ::: (f ::: Nil))
     (Limit j d ::: Nil)
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| forall (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
limitUniv @j
                                ((Sq'
  '(O f (Limit j (O g d)) ::: Nil, SUB Nil)
  '(Limit j (O g d) ::: (f ::: Nil), SUB Nil)
Sq
  (Fold (Limit j (O g d) ::: (f ::: Nil)) ::: Nil)
  (Limit j (O g d) ::: (f ::: Nil))
  Nil
  Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll Sq'
  '(O f (Limit j (O g d)) ::: Nil, SUB Nil)
  '(Limit j (O g d) ::: (f ::: Nil), SUB Nil)
-> Sq (j ::: Nil) (j ::: Nil) Nil Nil
-> Sq
     ((j ::: Nil) +++ (O f (Limit j (O g d)) ::: Nil))
     ((j ::: Nil) +++ (Limit j (O g d) ::: (f ::: Nil)))
     Nil
     Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq (j ::: Nil) (j ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId) Sq'
  '(j ::: (O f (Limit j (O g d)) ::: Nil), SUB Nil)
  '(j ::: (Limit j (O g d) ::: (f ::: Nil)), SUB Nil)
-> Sq
     (j ::: (Limit j (O g d) ::: (f ::: Nil)))
     (d ::: (g ::: (f ::: Nil)))
     Nil
     Nil
-> Sq
     (j ::: (O f (Limit j (O g d)) ::: Nil))
     (d ::: (g ::: (f ::: Nil)))
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (Sq (f ::: Nil) (f ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId Sq (f ::: Nil) (f ::: Nil) Nil Nil
-> Sq (j ::: (Limit j (O g d) ::: Nil)) (d ::: (g ::: Nil)) Nil Nil
-> Sq
     ((j ::: (Limit j (O g d) ::: Nil)) +++ (f ::: Nil))
     ((d ::: (g ::: Nil)) +++ (f ::: Nil))
     Nil
     Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== (forall (j :: kk i a) (d :: kk i k').
(HasLimits j k', IsTight d) =>
Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k).
(HasLimits j k, IsTight d) =>
Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
limit @j Sq (j ::: (Limit j (O g d) ::: Nil)) (O g d ::: Nil) Nil Nil
-> Sq (O g d ::: Nil) (d ::: (g ::: Nil)) Nil Nil
-> Sq
     (j ::: (Limit j (O g d) ::: Nil))
     (d ::: (g ::: Nil))
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
forall (ps :: Path kk i k').
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll @(d ::: g ::: Nil))) Sq'
  '(j ::: (O f (Limit j (O g d)) ::: Nil), SUB Nil)
  '(d ::: (g ::: (f ::: Nil)), SUB Nil)
-> Sq (d ::: (g ::: (f ::: Nil))) (d ::: Nil) Nil Nil
-> Sq
     (j ::: (O f (Limit j (O g d)) ::: Nil))
     (d ::: Nil)
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (forall (f :: kk k' k) (g :: kk k k').
(Adjunction f g, Equipment kk) =>
Sq (g ::: (f ::: Nil)) Nil Nil Nil
forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (g :: kk k j).
(Adjunction f g, Equipment kk) =>
Sq (g ::: (f ::: Nil)) Nil Nil Nil
counit @f @g Sq (g ::: (f ::: Nil)) Nil Nil Nil
-> Sq (d ::: Nil) (d ::: Nil) Nil Nil
-> Sq
     ((d ::: Nil) +++ (g ::: (f ::: Nil))) ((d ::: Nil) +++ Nil) Nil Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq (d ::: Nil) (d ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId))
                          )
                  )

-- | 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 {kk} {k} {k'} {i} {a} (f :: kk k' k) (g :: kk k k') (d :: kk i k) (j :: kk i a)
   . ( Adjunction f g
     , Equipment kk
     , IsTight d
     , IsTight f
     , IsTight g
     , L.HasLimits j k
     , L.HasLimits j k'
     )
  => Sq (L.Limit j d ::: g ::: Nil) (L.Limit j (g `O` d) ::: Nil) Nil Nil
rightAdjointPreservesLimitsInv :: forall {k} {kk :: k -> k -> Type} {k :: k} {k' :: k} {i :: k}
       {a :: k} (f :: kk k' k) (g :: kk k k') (d :: kk i k) (j :: kk i a).
(Adjunction f g, Equipment kk, IsTight d, IsTight f, IsTight g,
 HasLimits j k, HasLimits j k') =>
Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil
rightAdjointPreservesLimitsInv =
  forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @g (((Ob0 kk k, Ob0 kk k') =>
  Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
 -> Sq
      (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> ((Ob0 kk k, Ob0 kk k') =>
    Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$
    forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @j (((Ob0 kk i, Ob0 kk a) =>
  Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
 -> Sq
      (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> ((Ob0 kk i, Ob0 kk a) =>
    Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$
      forall (j :: kk i a) (k :: k) (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk i a) (k :: s)
       (d :: kk i k) r.
(HasLimits j k, IsTight d) =>
(IsTight (Limit j d) => r) -> r
L.withObLimit @j @k @d ((IsTight (Limit j d) =>
  Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
 -> Sq
      (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> (IsTight (Limit j d) =>
    Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$
        forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @_ @g @d (((IsOb Tight (O g d), Ob (O g d)) =>
  Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
 -> Sq
      (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> ((IsOb Tight (O g d), Ob (O g d)) =>
    Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$
          forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @_ @g @(L.Limit j d) (((IsOb Tight (O g (Limit j d)), Ob (O g (Limit j d))) =>
  Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
 -> Sq
      (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> ((IsOb Tight (O g (Limit j d)), Ob (O g (Limit j d))) =>
    Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil)
-> Sq (Limit j d ::: (g ::: Nil)) (Limit j (O g d) ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$
            Sq'
  '(Limit j d ::: (g ::: Nil), SUB Nil)
  '(O g (Limit j d) ::: Nil, SUB Nil)
Sq
  (Limit j d ::: (g ::: Nil))
  (Fold (Limit j d ::: (g ::: Nil)) ::: Nil)
  Nil
  Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll
              Sq'
  '(Limit j d ::: (g ::: Nil), SUB Nil)
  '(O g (Limit j d) ::: Nil, SUB Nil)
-> Sq (O g (Limit j d) ::: Nil) (Limit j (O g d) ::: Nil) Nil Nil
-> Sq
     (Limit j d ::: (g ::: Nil))
     (Limit j (O g d) ::: Nil)
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| forall (j :: kk i a) (d :: kk i k') (p :: kk a k').
(HasLimits j k', IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k) (p :: kk a k).
(HasLimits j k, IsTight d, Ob p) =>
Sq (j ::: (p ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Limit j d ::: Nil) Nil Nil
limitUniv @j @(g `O` d) @(g `O` L.Limit j d)
                ( (Sq'
  '(O g (Limit j d) ::: Nil, SUB Nil)
  '(Limit j d ::: (g ::: Nil), SUB Nil)
Sq
  (Fold (Limit j d ::: (g ::: Nil)) ::: Nil)
  (Limit j d ::: (g ::: Nil))
  Nil
  Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll Sq'
  '(O g (Limit j d) ::: Nil, SUB Nil)
  '(Limit j d ::: (g ::: Nil), SUB Nil)
-> Sq (j ::: Nil) (j ::: Nil) Nil Nil
-> Sq
     ((j ::: Nil) +++ (O g (Limit j d) ::: Nil))
     ((j ::: Nil) +++ (Limit j d ::: (g ::: Nil)))
     Nil
     Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== forall (p :: kk i a).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId @j)
                    Sq'
  '(j ::: (O g (Limit j d) ::: Nil), SUB Nil)
  '(j ::: (Limit j d ::: (g ::: Nil)), SUB Nil)
-> Sq
     (j ::: (Limit j d ::: (g ::: Nil))) (d ::: (g ::: Nil)) Nil Nil
-> Sq
     (j ::: (O g (Limit j d) ::: Nil))
     (d ::: (g ::: Nil))
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (forall (p :: kk k k').
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId @g Sq (g ::: Nil) (g ::: Nil) Nil Nil
-> Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
-> Sq
     ((j ::: (Limit j d ::: Nil)) +++ (g ::: Nil))
     ((d ::: Nil) +++ (g ::: Nil))
     Nil
     Nil
forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1}
       {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k2).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== forall (j :: kk i a) (d :: kk i k).
(HasLimits j k, IsTight d) =>
Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk i a) (d :: kk i k).
(HasLimits j k, IsTight d) =>
Sq (j ::: (Limit j d ::: Nil)) (d ::: Nil) Nil Nil
limit @j @d)
                    Sq'
  '(j ::: (O g (Limit j d) ::: Nil), SUB Nil)
  '(d ::: (g ::: Nil), SUB Nil)
-> Sq (d ::: (g ::: Nil)) (O g d ::: Nil) Nil Nil
-> Sq
     (j ::: (O g (Limit j d) ::: Nil))
     (O g d ::: Nil)
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| Sq (d ::: (g ::: Nil)) (O g d ::: Nil) Nil Nil
Sq (d ::: (g ::: Nil)) (Fold (d ::: (g ::: Nil)) ::: Nil) Nil Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll
                )

-- | The projection into the @j@-weighted colimit @c@ of @d@.
--
-- > I-----I
-- > j-\   |
-- > |  @-<d
-- > c</   |
-- > K-----K
colimit
  :: forall {kk} {a} {i} {k} (j :: kk a i) (d :: kk k i)
   . (L.HasColimits j k, IsCotight d)
  => Sq (L.Colimit j d ::: j ::: Nil) (d ::: Nil) Nil Nil
colimit :: forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk a i) (d :: kk k i).
(HasColimits j k, IsCotight d) =>
Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil
colimit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @d (((Ob0 kk k, Ob0 kk i) =>
  Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
 -> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> ((Ob0 kk k, Ob0 kk i) =>
    Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @j (((Ob0 kk a, Ob0 kk i) =>
  Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
 -> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> ((Ob0 kk a, Ob0 kk i) =>
    Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ forall (j :: kk a i) (k :: k) (d :: kk k i) r.
(HasColimits j k, IsCotight d) =>
(IsCotight (Colimit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk a i) (k :: s)
       (d :: kk k i) r.
(HasColimits j k, IsCotight d) =>
(IsCotight (Colimit j d) => r) -> r
L.withObColimit @j @k @d ((IsCotight (Colimit j d) =>
  Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
 -> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> (IsCotight (Colimit j d) =>
    Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (O Nil (Colimit j d ::: (j ::: Nil)) ~> O (d ::: Nil) Nil)
-> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((O Nil (Colimit j d ::: (j ::: Nil)) ~> O (d ::: Nil) Nil)
 -> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil)
-> (O Nil (Colimit j d ::: (j ::: Nil)) ~> O (d ::: Nil) Nil)
-> Sq (Colimit j d ::: (j ::: Nil)) (d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (Fold (Colimit j d ::: (j ::: Nil)) ~> Fold (d ::: Nil))
-> Strictified (Colimit j d ::: (j ::: Nil)) (d ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St ((Fold (Colimit j d ::: (j ::: Nil)) ~> Fold (d ::: Nil))
 -> Strictified (Colimit j d ::: (j ::: Nil)) (d ::: Nil))
-> (Fold (Colimit j d ::: (j ::: Nil)) ~> Fold (d ::: Nil))
-> Strictified (Colimit j d ::: (j ::: Nil)) (d ::: Nil)
forall a b. (a -> b) -> a -> b
$ forall (j :: kk a i) (k :: k) (d :: kk k i).
(HasColimits j k, IsCotight d) =>
O j (Colimit j d) ~> d
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk a i) (k :: s)
       (d :: kk k i).
(HasColimits j k, IsCotight d) =>
O j (Colimit j d) ~> d
L.colimit @j

-- | The universal property of the colimit.
--
-- The dotted inner square is the input square, the outer square is the output square.
--
-- > A---------A
-- > | I.....I |
-- > | j-\   : |
-- > | :  @-<d c
-- > p---/   : |
-- > | K.....K |
-- > K---------K
colimitUniv
  :: forall {kk} {a} {i} {k} (j :: kk a i) (d :: kk k i) (p :: kk k a)
   . (L.HasColimits j k, IsCotight d, Ob p)
  => Sq (p ::: j ::: Nil) (d ::: Nil) Nil Nil
  -> Sq (p ::: Nil) (L.Colimit j d ::: Nil) Nil Nil
colimitUniv :: forall {k} {kk :: k -> k -> Type} {a :: k} {i :: k} {k :: k}
       (j :: kk a i) (d :: kk k i) (p :: kk k a).
(HasColimits j k, IsCotight d, Ob p) =>
Sq (p ::: (j ::: Nil)) (d ::: Nil) Nil Nil
-> Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil
colimitUniv (Sq (St Fold (p ::: (j ::: Nil)) ~> Fold (d ::: Nil)
n)) = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @j (((Ob0 kk a, Ob0 kk i) =>
  Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil)
 -> Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil)
-> ((Ob0 kk a, Ob0 kk i) =>
    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
$ forall (j :: kk a i) (k :: k) (d :: kk k i) r.
(HasColimits j k, IsCotight d) =>
(IsCotight (Colimit j d) => r) -> r
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk a i) (k :: s)
       (d :: kk k i) r.
(HasColimits j k, IsCotight d) =>
(IsCotight (Colimit j d) => r) -> r
L.withObColimit @j @k @d ((IsCotight (Colimit j d) =>
  Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil)
 -> Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil)
-> (IsCotight (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
$ (O Nil (p ::: Nil) ~> O (Colimit j d ::: Nil) Nil)
-> Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((O Nil (p ::: Nil) ~> O (Colimit j d ::: Nil) Nil)
 -> Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil)
-> (O Nil (p ::: Nil) ~> O (Colimit j d ::: Nil) Nil)
-> Sq (p ::: Nil) (Colimit j d ::: Nil) Nil Nil
forall a b. (a -> b) -> a -> b
$ (Fold (p ::: Nil) ~> Fold (Colimit j d ::: Nil))
-> Strictified (p ::: Nil) (Colimit j d ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St ((Fold (p ::: Nil) ~> Fold (Colimit j d ::: Nil))
 -> Strictified (p ::: Nil) (Colimit j d ::: Nil))
-> (Fold (p ::: Nil) ~> Fold (Colimit j d ::: Nil))
-> Strictified (p ::: Nil) (Colimit j d ::: Nil)
forall a b. (a -> b) -> a -> b
$ forall (j :: kk a i) (k :: k) (d :: kk k i) (p :: kk k a).
(HasColimits j k, IsCotight d, Ob p) =>
(O j p ~> d) -> p ~> Colimit j d
forall {s} {kk :: CAT s} {a :: s} {i :: s} (j :: kk a i) (k :: s)
       (d :: kk k i) (p :: kk k a).
(HasColimits j k, IsCotight d, Ob p) =>
(O j p ~> d) -> p ~> Colimit j d
L.colimitUniv @j @k O j (Fold (p ::: Nil)) ~> d
Fold (p ::: (j ::: Nil)) ~> Fold (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' n =
--   withObConjoint @hk @vk @p $
--     fromRight ||| (colimitUniv @j @d @(Conjoint hk p) (n === 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 =
--   withOb2 @_ @f @d $
--     L.withObColimit @vk @j @k' @(f `O` d) $
--       withOb2 @_ @g @(L.Colimit j (f `O` d)) $
--         ( colimitUniv' @j
--             ( vId @d ||| unit @f @g
--                 === (vCombine === colimit @j) ||| vId @g
--                 === vCombine
--             )
--             === vSplit
--         )
--           ||| vId @f
--           === vId @(L.Colimit j (f `O` d)) ||| 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 =
--   L.withObColimit @vk @j @k @d $
--     withOb2 @vk @f @d $
--       withOb2 @vk @f @(L.Colimit j d) $
--         colimitUniv' @j @(f `O` d) @(f `O` L.Colimit j d)
--           ( vSplit
--               === colimit @j @d ||| vId @f
--               === vCombine
--           )
--           === vSplit

unit
  :: forall {kk} {j} {k} (f :: kk j k) (g :: kk k j)
   . (Adjunction f g, Equipment kk)
  => Sq Nil (f ::: g ::: Nil) Nil Nil
unit :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (g :: kk k j).
(Adjunction f g, Equipment kk) =>
Sq Nil (f ::: (g ::: Nil)) Nil Nil
unit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f (((Ob0 kk j, Ob0 kk k) => Sq Nil (f ::: (g ::: Nil)) Nil Nil)
 -> Sq Nil (f ::: (g ::: Nil)) Nil Nil)
-> ((Ob0 kk j, Ob0 kk k) => Sq Nil (f ::: (g ::: Nil)) Nil Nil)
-> Sq Nil (f ::: (g ::: Nil)) Nil Nil
forall a b. (a -> b) -> a -> b
$ Sq' '(Nil, SUB Nil) '(I ::: Nil, SUB Nil)
Sq Nil (Fold Nil ::: Nil) Nil Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll Sq' '(Nil, SUB Nil) '(I ::: Nil, SUB Nil)
-> Sq (I ::: Nil) (O g f ::: Nil) Nil Nil
-> Sq Nil (O g f ::: Nil) (Nil +++ Nil) (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (I ~> O g f) -> Sq (I ::: Nil) (O g f ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2) (q :: kk j k2).
Equipment kk =>
(p ~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr (forall (l :: kk j k) (r :: kk 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, SUB Nil) '(O g f ::: Nil, SUB Nil)
-> Sq (O g f ::: Nil) (f ::: (g ::: Nil)) Nil Nil
-> Sq Nil (f ::: (g ::: Nil)) (Nil +++ Nil) (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| Sq (O g f ::: Nil) (f ::: (g ::: Nil)) Nil Nil
Sq (Fold (f ::: (g ::: Nil)) ::: Nil) (f ::: (g ::: Nil)) Nil Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll

counit
  :: forall {kk} {j} {k} (f :: kk j k) (g :: kk k j)
   . (Adjunction f g, Equipment kk)
  => Sq (g ::: f ::: Nil) Nil Nil Nil
counit :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (g :: kk k j).
(Adjunction f g, Equipment kk) =>
Sq (g ::: (f ::: Nil)) Nil Nil Nil
counit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f (((Ob0 kk j, Ob0 kk k) => Sq (g ::: (f ::: Nil)) Nil Nil Nil)
 -> Sq (g ::: (f ::: Nil)) Nil Nil Nil)
-> ((Ob0 kk j, Ob0 kk k) => Sq (g ::: (f ::: Nil)) Nil Nil Nil)
-> Sq (g ::: (f ::: Nil)) Nil Nil Nil
forall a b. (a -> b) -> a -> b
$ Sq' '(g ::: (f ::: Nil), SUB Nil) '(O f g ::: Nil, SUB Nil)
Sq (g ::: (f ::: Nil)) (Fold (g ::: (f ::: Nil)) ::: Nil) Nil Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll Sq' '(g ::: (f ::: Nil), SUB Nil) '(O f g ::: Nil, SUB Nil)
-> Sq (O f g ::: Nil) (I ::: Nil) Nil Nil
-> Sq (g ::: (f ::: Nil)) (I ::: Nil) (Nil +++ Nil) (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (O f g ~> I) -> Sq (O f g ::: Nil) (I ::: Nil) Nil Nil
forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1}
       (p :: kk j k2) (q :: kk j k2).
Equipment kk =>
(p ~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr (forall (l :: kk j k) (r :: kk 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' '(g ::: (f ::: Nil), SUB Nil) '(I ::: Nil, SUB Nil)
-> Sq (I ::: Nil) Nil Nil Nil
-> Sq (g ::: (f ::: Nil)) Nil (Nil +++ Nil) (Nil +++ Nil)
forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c2) (gs :: Path kk b c1).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| Sq (I ::: Nil) Nil Nil Nil
Sq (Fold Nil ::: Nil) Nil Nil Nil
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1}
       (ps :: Path kk j k2).
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll