{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Equipment.Limit where

import Data.Kind (Constraint)
import Prelude (($))

import Proarrow.Category.Bicategory
  ( Bicategory (..)
  , flipLeftAdjoint
  , flipLeftAdjointInv
  , flipRightAdjoint
  , flipRightAdjointInv
  , obj1
  )
import Proarrow.Category.Equipment (CotightAdjoint, Equipment (..), IsCotight, IsTight, TightAdjoint)
import Proarrow.Core (CAT, CategoryOf (..), (.))

-- | weighted limits
type HasLimits :: forall {s} {kk :: CAT s} {a :: s} {i :: s}. kk i a -> s -> Constraint
class (Equipment kk, Ob j) => HasLimits (j :: kk i a) k where
  type Limit (j :: kk i a) (d :: kk i k) :: kk a k
  withObLimit :: (IsTight (d :: kk i k)) => ((IsTight (Limit j d)) => r) -> r
  limit :: (IsTight (d :: kk i k)) => Limit j d `O` j ~> d
  limitUniv :: (IsTight (d :: kk i k), Ob p) => p `O` j ~> d -> p ~> Limit j d

limitToLimitAdj
  :: forall {kk} {k} {a} {b} (j :: kk a b) (c :: kk k b) (r :: kk a k)
   . (Equipment kk, HasLimits j k, IsTight r, IsCotight c)
  => I ~> c `O` Limit j r -> j ~> c `O` r
limitToLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s}
       (j :: kk a b) (c :: kk k b) (r :: kk a k).
(Equipment kk, HasLimits j k, IsTight r, IsCotight c) =>
(I ~> O c (Limit j r)) -> j ~> O c r
limitToLimitAdj I ~> O c (Limit j r)
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @r (((Ob0 kk a, Ob0 kk k) => j ~> O c r) -> j ~> O c r)
-> ((Ob0 kk a, Ob0 kk k) => j ~> O c r) -> j ~> O c r
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @c (((Ob0 kk k, Ob0 kk b) => j ~> O c r) -> j ~> O c r)
-> ((Ob0 kk k, Ob0 kk b) => j ~> O c r) -> j ~> O c r
forall a b. (a -> b) -> a -> b
$
      forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
forall (kk :: CAT s) {j :: s} {k1 :: s} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @kk @c (((Adjunction_ (TightAdjoint c) c, IsTight (TightAdjoint c)) =>
  j ~> O c r)
 -> j ~> O c r)
-> ((Adjunction_ (TightAdjoint c) c, IsTight (TightAdjoint c)) =>
    j ~> O c r)
-> j ~> O c r
forall a b. (a -> b) -> a -> b
$
        forall (j :: kk a b) (k :: s) (d :: kk a 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
withObLimit @j @_ @r ((IsTight (Limit j r) => j ~> O c r) -> j ~> O c r)
-> (IsTight (Limit j r) => j ~> O c r) -> j ~> O c r
forall a b. (a -> b) -> a -> b
$
          forall (l :: kk b k) (r :: kk k b) (a :: kk a b) (b :: kk a k).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
flipLeftAdjoint @(TightAdjoint c) @c @j @r ((O (TightAdjoint c) j ~> r) -> j ~> O c r)
-> (O (TightAdjoint c) j ~> r) -> j ~> O c r
forall a b. (a -> b) -> a -> b
$
            forall (j :: kk a b) (k :: s) (d :: kk a 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
limit @j @k @r
              (O (Limit j r) j ~> r)
-> (O (TightAdjoint c) j ~> O (Limit j r) j)
-> O (TightAdjoint c) j ~> r
forall (b :: kk a k) (c :: kk a k) (a :: kk a k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((forall (l :: kk b k) (r :: kk k b) (a :: kk b b) (b :: kk b k).
(Adjunction l r, Ob b) =>
(a ~> O r b) -> O l a ~> b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob b) =>
(a ~> O r b) -> O l a ~> b
flipLeftAdjointInv @(TightAdjoint c) @c @I @(Limit j r) I ~> O c (Limit j r)
n (O (TightAdjoint c) I ~> Limit j r)
-> (TightAdjoint c ~> O (TightAdjoint c) I)
-> TightAdjoint c ~> Limit j r
forall (b :: kk b k) (c :: kk b k) (a :: kk b k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
forall (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
rightUnitorInv @kk @(TightAdjoint c)) (TightAdjoint c ~> Limit j r)
-> (j ~> j) -> O (TightAdjoint c) j ~> O (Limit j r) j
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk a b). (Bicategory kk, Ob a) => Obj a
forall {s} {kk :: CAT s} {j :: s} {k :: s} (a :: kk j k).
(Bicategory kk, Ob a) =>
Obj a
obj1 @j)

limitFromLimitAdj
  :: forall {kk} {k} {a} {b} (j :: kk a b) (c :: kk k b) (r :: kk a k)
   . (Equipment kk, HasLimits j k, IsTight r, IsCotight c)
  => j ~> c `O` r -> I ~> c `O` Limit j r
limitFromLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s}
       (j :: kk a b) (c :: kk k b) (r :: kk a k).
(Equipment kk, HasLimits j k, IsTight r, IsCotight c) =>
(j ~> O c r) -> I ~> O c (Limit j r)
limitFromLimitAdj j ~> O c r
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @c (((Ob0 kk k, Ob0 kk b) => I ~> O c (Limit j r))
 -> I ~> O c (Limit j r))
-> ((Ob0 kk k, Ob0 kk b) => I ~> O c (Limit j r))
-> I ~> O c (Limit j r)
forall a b. (a -> b) -> a -> b
$
    forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
forall (kk :: CAT s) {j :: s} {k1 :: s} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @kk @c (((Adjunction_ (TightAdjoint c) c, IsTight (TightAdjoint c)) =>
  I ~> O c (Limit j r))
 -> I ~> O c (Limit j r))
-> ((Adjunction_ (TightAdjoint c) c, IsTight (TightAdjoint c)) =>
    I ~> O c (Limit j r))
-> I ~> O c (Limit j r)
forall a b. (a -> b) -> a -> b
$
      forall (l :: kk b k) (r :: kk k b) (a :: kk b b) (b :: kk b k).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
flipLeftAdjoint @(TightAdjoint c) @c @I @(Limit j r) ((O (TightAdjoint c) I ~> Limit j r) -> I ~> O c (Limit j r))
-> (O (TightAdjoint c) I ~> Limit j r) -> I ~> O c (Limit j r)
forall a b. (a -> b) -> a -> b
$
        forall (j :: kk a b) (k :: s) (d :: kk a k) (p :: kk b 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
limitUniv @j @k @r (forall (l :: kk b k) (r :: kk k b) (a :: kk a b) (b :: kk a k).
(Adjunction l r, Ob b) =>
(a ~> O r b) -> O l a ~> b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob b) =>
(a ~> O r b) -> O l a ~> b
flipLeftAdjointInv @(TightAdjoint c) @c @j @r j ~> O c r
n) (TightAdjoint c ~> Limit j r)
-> (O (TightAdjoint c) I ~> TightAdjoint c)
-> O (TightAdjoint c) I ~> Limit j r
forall (b :: kk b k) (c :: kk b k) (a :: kk b k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor @kk @(TightAdjoint c)

mapLimit
  :: forall {kk} {i} {a} (j :: kk i a) k p q
   . (HasLimits j k, IsTight p, IsTight q)
  => (p :: kk i k) ~> q -> Limit j p ~> Limit j q
mapLimit :: forall {s} {kk :: s -> s -> Type} {i :: s} {a :: s} (j :: kk i a)
       (k :: s) (p :: kk i k) (q :: kk i k).
(HasLimits j k, IsTight p, IsTight q) =>
(p ~> q) -> Limit j p ~> Limit j q
mapLimit p ~> q
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p (((Ob0 kk i, Ob0 kk k) => Limit j p ~> Limit j q)
 -> Limit j p ~> Limit j q)
-> ((Ob0 kk i, Ob0 kk k) => Limit j p ~> Limit j q)
-> Limit j p ~> Limit j q
forall a b. (a -> b) -> a -> b
$ forall (j :: kk i a) (k :: s) (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
withObLimit @j @_ @p ((IsTight (Limit j p) => Limit j p ~> Limit j q)
 -> Limit j p ~> Limit j q)
-> (IsTight (Limit j p) => Limit j p ~> Limit j q)
-> Limit j p ~> Limit j q
forall a b. (a -> b) -> a -> b
$ forall (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
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
limitUniv @j @k @q (p ~> q
n (p ~> q) -> (O (Limit j p) j ~> p) -> O (Limit j p) j ~> q
forall (b :: kk i k) (c :: kk i k) (a :: kk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk i a) (k :: s) (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
limit @j @k @p)

-- | weighted colimits
type HasColimits :: forall {s} {kk :: CAT s} {a :: s} {i :: s}. kk a i -> s -> Constraint
class (Equipment kk, Ob j) => HasColimits (j :: kk a i) k where
  type Colimit (j :: kk a i) (d :: kk k i) :: kk k a
  withObColimit :: (IsCotight (d :: kk k i)) => ((IsCotight (Colimit j d)) => r) -> r
  colimit :: (IsCotight (d :: kk k i)) => j `O` Colimit j d ~> d
  colimitUniv :: (IsCotight (d :: kk k i), Ob p) => (j `O` p ~> d) -> p ~> Colimit j d

colimitToLimitAdj
  :: forall {kk} {k} {a} {b} (j :: kk a b) (c :: kk k b) (r :: kk a k)
   . (Equipment kk, HasColimits j k, IsTight r, IsCotight c)
  => I ~> Colimit j c `O` r -> j ~> c `O` r
colimitToLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s}
       (j :: kk a b) (c :: kk k b) (r :: kk a k).
(Equipment kk, HasColimits j k, IsTight r, IsCotight c) =>
(I ~> O (Colimit j c) r) -> j ~> O c r
colimitToLimitAdj I ~> O (Colimit j c) r
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @c (((Ob0 kk k, Ob0 kk b) => j ~> O c r) -> j ~> O c r)
-> ((Ob0 kk k, Ob0 kk b) => j ~> O c r) -> j ~> O c r
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @r (((Ob0 kk a, Ob0 kk k) => j ~> O c r) -> j ~> O c r)
-> ((Ob0 kk a, Ob0 kk k) => j ~> O c r) -> j ~> O c r
forall a b. (a -> b) -> a -> b
$
      forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
forall (kk :: CAT s) {j :: s} {k1 :: s} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @kk @r (((Adjunction_ r (CotightAdjoint r),
   IsCotight (CotightAdjoint r)) =>
  j ~> O c r)
 -> j ~> O c r)
-> ((Adjunction_ r (CotightAdjoint r),
     IsCotight (CotightAdjoint r)) =>
    j ~> O c r)
-> j ~> O c r
forall a b. (a -> b) -> a -> b
$
        forall (j :: kk a b) (k :: s) (d :: kk k b) 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
withObColimit @j @_ @c ((IsCotight (Colimit j c) => j ~> O c r) -> j ~> O c r)
-> (IsCotight (Colimit j c) => j ~> O c r) -> j ~> O c r
forall a b. (a -> b) -> a -> b
$
          forall (l :: kk a k) (r :: kk k a) (a :: kk a b) (b :: kk k b).
(Adjunction l r, Ob a) =>
(O a r ~> b) -> a ~> O b l
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob a) =>
(O a r ~> b) -> a ~> O b l
flipRightAdjoint @r @(CotightAdjoint r) @j @c ((O j (CotightAdjoint r) ~> c) -> j ~> O c r)
-> (O j (CotightAdjoint r) ~> c) -> j ~> O c r
forall a b. (a -> b) -> a -> b
$
            forall (j :: kk a b) (k :: s) (d :: kk k b).
(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
colimit @j @k @c
              (O j (Colimit j c) ~> c)
-> (O j (CotightAdjoint r) ~> O j (Colimit j c))
-> O j (CotightAdjoint r) ~> c
forall (b :: kk k b) (c :: kk k b) (a :: kk k b).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: kk a b). (Bicategory kk, Ob a) => Obj a
forall {s} {kk :: CAT s} {j :: s} {k :: s} (a :: kk j k).
(Bicategory kk, Ob a) =>
Obj a
obj1 @j Obj j
-> (CotightAdjoint r ~> Colimit j c)
-> O j (CotightAdjoint r) ~> O j (Colimit j c)
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` (forall (l :: kk a k) (r :: kk k a) (a :: kk a a) (b :: kk k a).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
flipRightAdjointInv @r @(CotightAdjoint r) @I @(Colimit j c) I ~> O (Colimit j c) r
n (O I (CotightAdjoint r) ~> Colimit j c)
-> (CotightAdjoint r ~> O I (CotightAdjoint r))
-> CotightAdjoint r ~> Colimit j c
forall (b :: kk k a) (c :: kk k a) (a :: kk k a).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
forall (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv @kk @(CotightAdjoint r)))

colimitFromLimitAdj
  :: forall {kk} {k} {a} {b} (j :: kk a b) (c :: kk k b) (r :: kk a k)
   . (Equipment kk, HasColimits j k, IsTight r, IsCotight c)
  => j ~> c `O` r -> I ~> Colimit j c `O` r
colimitFromLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s}
       (j :: kk a b) (c :: kk k b) (r :: kk a k).
(Equipment kk, HasColimits j k, IsTight r, IsCotight c) =>
(j ~> O c r) -> I ~> O (Colimit j c) r
colimitFromLimitAdj j ~> O c r
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @r (((Ob0 kk a, Ob0 kk k) => I ~> O (Colimit j c) r)
 -> I ~> O (Colimit j c) r)
-> ((Ob0 kk a, Ob0 kk k) => I ~> O (Colimit j c) r)
-> I ~> O (Colimit j c) r
forall a b. (a -> b) -> a -> b
$
    forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
forall (kk :: CAT s) {j :: s} {k1 :: s} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @kk @r (((Adjunction_ r (CotightAdjoint r),
   IsCotight (CotightAdjoint r)) =>
  I ~> O (Colimit j c) r)
 -> I ~> O (Colimit j c) r)
-> ((Adjunction_ r (CotightAdjoint r),
     IsCotight (CotightAdjoint r)) =>
    I ~> O (Colimit j c) r)
-> I ~> O (Colimit j c) r
forall a b. (a -> b) -> a -> b
$
      forall (l :: kk a k) (r :: kk k a) (a :: kk a a) (b :: kk k a).
(Adjunction l r, Ob a) =>
(O a r ~> b) -> a ~> O b l
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob a) =>
(O a r ~> b) -> a ~> O b l
flipRightAdjoint @r @(CotightAdjoint r) @I @(Colimit j c) ((O I (CotightAdjoint r) ~> Colimit j c) -> I ~> O (Colimit j c) r)
-> (O I (CotightAdjoint r) ~> Colimit j c)
-> I ~> O (Colimit j c) r
forall a b. (a -> b) -> a -> b
$
        forall (j :: kk a b) (k :: s) (d :: kk k b) (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
colimitUniv @j @k @c (forall (l :: kk a k) (r :: kk k a) (a :: kk a b) (b :: kk k b).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
flipRightAdjointInv @r @(CotightAdjoint r) @j @c j ~> O c r
n) (CotightAdjoint r ~> Colimit j c)
-> (O I (CotightAdjoint r) ~> CotightAdjoint r)
-> O I (CotightAdjoint r) ~> Colimit j c
forall (b :: kk k a) (c :: kk k a) (a :: kk k a).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor @kk @(CotightAdjoint r)

mapColimit
  :: forall {kk} {i} {a} (j :: kk a i) k p q
   . (HasColimits j k, IsCotight p, IsCotight q)
  => (p :: kk k i) ~> q -> Colimit j p ~> Colimit j q
mapColimit :: forall {s} {kk :: s -> s -> Type} {i :: s} {a :: s} (j :: kk a i)
       (k :: s) (p :: kk k i) (q :: kk k i).
(HasColimits j k, IsCotight p, IsCotight q) =>
(p ~> q) -> Colimit j p ~> Colimit j q
mapColimit p ~> q
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 s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p (((Ob0 kk k, Ob0 kk i) => Colimit j p ~> Colimit j q)
 -> Colimit j p ~> Colimit j q)
-> ((Ob0 kk k, Ob0 kk i) => Colimit j p ~> Colimit j q)
-> Colimit j p ~> Colimit j q
forall a b. (a -> b) -> a -> b
$ forall (j :: kk a i) (k :: s) (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
withObColimit @j @_ @p ((IsCotight (Colimit j p) => Colimit j p ~> Colimit j q)
 -> Colimit j p ~> Colimit j q)
-> (IsCotight (Colimit j p) => Colimit j p ~> Colimit j q)
-> Colimit j p ~> Colimit j q
forall a b. (a -> b) -> a -> b
$ forall (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
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
colimitUniv @j @k @q (p ~> q
n (p ~> q) -> (O j (Colimit j p) ~> p) -> O j (Colimit j p) ~> q
forall (b :: kk k i) (c :: kk k i) (a :: kk k i).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (j :: kk a i) (k :: s) (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
colimit @j @k @p)

-- type family TerminalObject (hk :: CAT s) (vk :: CAT s) :: s
-- type HasTerminalObject :: forall {s}. CAT s -> CAT s -> Constraint
-- class (HasCompanions hk vk) => HasTerminalObject (hk :: CAT s) (vk :: CAT s) where
--   type Terminate hk vk (j :: s) :: vk j (TerminalObject hk vk)
--   terminate :: (Ob0 vk j) => Obj (Terminate hk vk j)
--   termUniv :: (Ob0 vk i, Ob0 vk j, Ob (p :: hk i j)) => Sq '(p, Terminate hk vk j) '(I, Terminate hk vk i)

-- type family InitialObject (hk :: CAT s) (vk :: CAT s) :: s
-- type HasInitialObject :: forall {s}. CAT s -> CAT s -> Constraint
-- class (HasCompanions hk vk) => HasInitialObject (hk :: CAT s) (vk :: CAT s) where
--   type Initiate hk vk (j :: s) :: vk (InitialObject hk vk) j
--   initiate :: (Ob0 vk j) => Obj (Initiate hk vk j)
--   initUniv :: (Ob0 vk i, Ob0 vk j, Ob (p :: hk i j)) => Sq '(I, Initiate hk vk j) '(p, Initiate hk vk i)

-- type family Product (hk :: CAT s) (vk :: CAT s) (a :: s) (b :: s) :: s
-- type HasBinaryProducts :: forall {s}. CAT s -> CAT s -> Constraint
-- class HasBinaryProducts (hk :: CAT s) (vk :: CAT s) where
--   type Fst hk vk (i :: s) (j :: s) :: vk (Product hk vk i j) i
--   type Snd hk vk (i :: s) (j :: s) :: vk (Product hk vk i j) j
--   fstObj :: (Ob0 vk i, Ob0 vk j) => Obj (Fst hk vk i j)
--   sndObj :: (Ob0 vk i, Ob0 vk j) => Obj (Snd hk vk i j)
--   type ProdV hk vk (f :: vk k i) (g :: vk k j) :: vk k (Product hk vk i j)
--   type ProdH hk vk (p :: hk j k) (q :: hk j' k') :: hk (Product hk vk j j') (Product hk vk k k')
--   prodObj :: (Ob0 vk j, Ob0 vk a, Ob0 vk b, Ob (f :: vk j a), Ob (g :: vk j b)) => Obj (ProdV hk vk f g)
--   prodUniv
--     :: Sq '(p :: hk k k', f' :: vk k' i') '(a, f)
--     -> Sq '(p, g' :: vk k' j') '(b, g)
--     -> Sq '(p, ProdV hk vk f' g') '(ProdH hk vk a b, ProdV hk vk f g)

-- type family Coproduct (hk :: CAT s) (vk :: CAT s) (a :: s) (b :: s) :: s
-- type HasBinaryCoproducts :: forall {s}. CAT s -> CAT s -> Constraint
-- class HasBinaryCoproducts (hk :: CAT s) (vk :: CAT s) where
--   type Lft hk vk (i :: s) (j :: s) :: vk i (Coproduct hk vk i j)
--   type Rgt hk vk (i :: s) (j :: s) :: vk j (Coproduct hk vk i j)
--   lftObj :: (Ob0 vk i, Ob0 vk j) => Obj (Lft hk vk i j)
--   rgtObj :: (Ob0 vk i, Ob0 vk j) => Obj (Rgt hk vk i j)
--   type CoprodV hk vk (f :: vk i k) (g :: vk j k) :: vk (Coproduct hk vk i j) k
--   type CoprodH hk vk (p :: hk j k) (q :: hk j' k') :: hk (Coproduct hk vk j j') (Coproduct hk vk k k')
--   coprodObj :: (Ob0 vk j, Ob0 vk a, Ob0 vk b, Ob (f :: vk a j), Ob (g :: vk b j)) => Obj (CoprodV hk vk f g)
--   coprodUniv
--     :: Sq '(a :: hk i i', f' :: vk i' k') '(p :: hk k k', f :: vk i k)
--     -> Sq '(b :: hk j j', g' :: vk j' k') '(p :: hk k k', g :: vk j k)
--     -> Sq '(CoprodH hk vk a b, CoprodV hk vk f' g') '(p, CoprodV hk vk f g)