{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Equipment.Limit where

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

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq, flipCompanion, flipCompanionInv)
import Proarrow.Core (CAT, CategoryOf (..), Obj, obj, (.))

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

toLimitAdj
  :: forall {hk} {vk} {k} {a} {b} (j :: hk a b) (c :: vk b k) (r :: vk a k)
   . (Equipment hk vk, HasLimits vk j k, Ob r, Ob c)
  => Companion hk c ~> Companion hk (Limit j r) -> j ~> Conjoint hk c `O` Companion hk r
toLimitAdj :: forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {k :: c}
       {a :: c} {b :: c} (j :: hk a b) (c :: vk b k) (r :: vk a k).
(Equipment hk vk, HasLimits vk j k, Ob r, Ob c) =>
(Companion hk c ~> Companion hk (Limit j r))
-> j ~> O (Conjoint hk c) (Companion hk r)
toLimitAdj Companion hk c ~> Companion hk (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 c) {j :: c} {k :: c} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @vk @r (((Ob0 vk a, Ob0 vk k) => j ~> O (Conjoint hk c) (Companion hk r))
 -> j ~> O (Conjoint hk c) (Companion hk r))
-> ((Ob0 vk a, Ob0 vk k) =>
    j ~> O (Conjoint hk c) (Companion hk r))
-> j ~> O (Conjoint hk c) (Companion hk 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 c) {j :: c} {k :: c} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @vk @c (((Ob0 vk b, Ob0 vk k) => j ~> O (Conjoint hk c) (Companion hk r))
 -> j ~> O (Conjoint hk c) (Companion hk r))
-> ((Ob0 vk b, Ob0 vk k) =>
    j ~> O (Conjoint hk c) (Companion hk r))
-> j ~> O (Conjoint hk c) (Companion hk r)
forall a b. (a -> b) -> a -> b
$
      forall (f :: vk b k) (p :: hk a b) (q :: hk a k).
(Equipment hk vk, Ob p) =>
Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) 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 p) =>
Obj f -> (O (Companion hk f) p ~> q) -> p ~> O (Conjoint hk f) q
flipCompanion @c @j @(Companion hk r) (forall (a :: vk b k). (CategoryOf (vk b k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) (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 c) (j :: hk a b) (k :: c) (d :: vk a k).
(HasLimits vk j k, Ob d) =>
O (Companion hk (Limit j d)) j ~> Companion hk d
limit @vk @j @k @r (O (Companion hk (Limit j r)) j ~> Companion hk r)
-> (O (Companion hk c) j ~> O (Companion hk (Limit j r)) j)
-> O (Companion hk c) j ~> Companion hk r
forall (b :: hk a k) (c :: hk a k) (a :: hk 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
. (Companion hk c ~> Companion hk (Limit j r)
n (Companion hk c ~> Companion hk (Limit j r))
-> (j ~> j)
-> O (Companion hk c) j ~> O (Companion hk (Limit j r)) j
forall {i :: c} (j :: c) (k :: c) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk 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 :: hk a b). (CategoryOf (hk a b), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j)) ((Ob0 hk b, Ob0 hk k, Ob (Companion hk c),
  Ob (Companion hk (Limit j r))) =>
 j ~> O (Conjoint hk c) (Companion hk r))
-> (Companion hk c ~> Companion hk (Limit j r))
-> j ~> O (Conjoint hk c) (Companion hk r)
forall (i :: c) (j :: c) (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
\\\ Companion hk c ~> Companion hk (Limit j r)
n

fromLimitAdj
  :: forall {hk} {vk} {k} {a} {b} (j :: hk a b) (c :: vk b k) (r :: vk a k)
   . (Equipment hk vk, HasLimits vk j k, Ob r, Ob c)
  => j ~> Conjoint hk c `O` Companion hk r -> Companion hk c ~> Companion hk (Limit j r)
fromLimitAdj :: forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {k :: s}
       {a :: s} {b :: s} (j :: hk a b) (c :: vk b k) (r :: vk a k).
(Equipment hk vk, HasLimits vk j k, Ob r, Ob c) =>
(j ~> O (Conjoint hk c) (Companion hk r))
-> Companion hk c ~> Companion hk (Limit j r)
fromLimitAdj j ~> O (Conjoint hk c) (Companion hk 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 @vk @r (((Ob0 vk a, Ob0 vk k) =>
  Companion hk c ~> Companion hk (Limit j r))
 -> Companion hk c ~> Companion hk (Limit j r))
-> ((Ob0 vk a, Ob0 vk k) =>
    Companion hk c ~> Companion hk (Limit j r))
-> Companion hk c ~> Companion hk (Limit j 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 @vk @c (((Ob0 vk b, Ob0 vk k) =>
  Companion hk c ~> Companion hk (Limit j r))
 -> Companion hk c ~> Companion hk (Limit j r))
-> ((Ob0 vk b, Ob0 vk k) =>
    Companion hk c ~> Companion hk (Limit j r))
-> Companion hk c ~> Companion hk (Limit j r)
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 s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @r ((Ob (Companion hk r) =>
  Companion hk c ~> Companion hk (Limit j r))
 -> Companion hk c ~> Companion hk (Limit j r))
-> (Ob (Companion hk r) =>
    Companion hk c ~> Companion hk (Limit j r))
-> Companion hk c ~> Companion hk (Limit j r)
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 s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @c ((Ob (Companion hk c) =>
  Companion hk c ~> Companion hk (Limit j r))
 -> Companion hk c ~> Companion hk (Limit j r))
-> (Ob (Companion hk c) =>
    Companion hk c ~> Companion hk (Limit j r))
-> Companion hk c ~> Companion hk (Limit j r)
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) (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 s) (j :: hk a b) (k :: s) (d :: vk a k)
       (p :: hk b k).
(HasLimits vk j k, Ob d, Ob p) =>
(O p j ~> Companion hk d) -> p ~> Companion hk (Limit j d)
limitUniv @vk @j @k @r (forall (f :: vk b k) (p :: hk a b) (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 @c @j @(Companion hk r) (forall (a :: vk b k). (CategoryOf (vk b k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) j ~> O (Conjoint hk c) (Companion hk r)
n) ((Ob0 hk a, Ob0 hk b, Ob j,
  Ob (O (Conjoint hk c) (Companion hk r))) =>
 Companion hk c ~> Companion hk (Limit j r))
-> (j ~> O (Conjoint hk c) (Companion hk r))
-> Companion hk c ~> Companion hk (Limit j r)
forall (i :: s) (j :: s) (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
\\\ j ~> O (Conjoint hk c) (Companion hk r)
n

mapLimit
  :: forall {hk} {vk} {i} {a} (j :: hk i a) k p q
   . (HasLimits vk j k)
  => (p :: vk i k) ~> q -> Companion hk (Limit j p) ~> Companion hk (Limit j q)
mapLimit :: forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {i :: s}
       {a :: s} (j :: hk i a) (k :: s) (p :: vk i k) (q :: vk i k).
HasLimits vk j k =>
(p ~> q) -> Companion hk (Limit j p) ~> Companion hk (Limit j q)
mapLimit p ~> q
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 s) (j :: hk i a) (k :: s) (d :: vk i k) r.
(HasLimits vk j k, Ob d) =>
(Ob (Limit j d) => r) -> r
withObLimit @vk @j @k @p ((Ob (Limit j p) =>
  Companion hk (Limit j p) ~> Companion hk (Limit j q))
 -> Companion hk (Limit j p) ~> Companion hk (Limit j q))
-> (Ob (Limit j p) =>
    Companion hk (Limit j p) ~> Companion hk (Limit j q))
-> Companion hk (Limit j p) ~> Companion hk (Limit j q)
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 s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
       r.
(HasCompanions hk vk, Ob f) =>
(Ob (Companion hk f) => r) -> r
withObCompanion @hk @vk @(Limit j p) ((Ob (Companion hk (Limit j p)) =>
  Companion hk (Limit j p) ~> Companion hk (Limit j q))
 -> Companion hk (Limit j p) ~> Companion hk (Limit j q))
-> (Ob (Companion hk (Limit j p)) =>
    Companion hk (Limit j p) ~> Companion hk (Limit j q))
-> Companion hk (Limit j p) ~> Companion hk (Limit j q)
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) (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 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)
limitUniv @vk @j @k @q ((p ~> q) -> Companion hk p ~> Companion hk q
forall {j :: s} {k :: s} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion p ~> q
n (Companion hk p ~> Companion hk q)
-> (O (Companion hk (Limit j p)) j ~> Companion hk p)
-> O (Companion hk (Limit j p)) j ~> Companion hk q
forall (b :: hk i k) (c :: hk i k) (a :: hk 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 {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 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
limit @vk @j @k @p)
  )
    ((Ob0 vk i, Ob0 vk k, Ob p, Ob q) =>
 Companion hk (Limit j p) ~> Companion hk (Limit j q))
-> (p ~> q) -> Companion hk (Limit j p) ~> Companion hk (Limit j q)
forall (i :: s) (j :: s) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ p ~> q
n

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

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)