{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Equipment.Limit where

import Data.Kind (Constraint)

import Proarrow.Category.Bicategory (Bicategory (..), associator')
import Proarrow.Category.Equipment (HasCompanions (..))
import Proarrow.Core (CAT, CategoryOf (..), Obj, Promonad (..), 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
  limitObj :: Ob (d :: vk i k) => Obj (Limit j d)
  limit :: (Ob (d :: vk i k)) => Companion hk (Limit j d) `O` j ~> Companion hk d
  limitUniv :: (Ob (d :: vk i k), Ob p) => Companion hk p `O` j ~> Companion hk d -> p ~> Limit j d

-- lift :: f ~> j `O` Lift j f

rightAdjointPreservesLimitsInv
  :: forall {hk} {vk} {k} {k'} {i} {a} (g :: vk k k') (d :: vk i k) (j :: hk i a)
   . (Ob d, Ob g, HasLimits vk j k, HasLimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a)
  => g `O` Limit j d ~> Limit j (g `O` d)
rightAdjointPreservesLimitsInv :: forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {k :: s}
       {k' :: s} {i :: s} {a :: s} (g :: vk k k') (d :: vk i k)
       (j :: hk i a).
(Ob d, Ob g, HasLimits vk j k, HasLimits vk j k', Ob0 vk i,
 Ob0 vk k, Ob0 vk k', Ob0 vk a) =>
O g (Limit j d) ~> Limit j (O g d)
rightAdjointPreservesLimitsInv =
  let
    d :: Obj d
d = forall (a :: vk i k). (CategoryOf (vk i k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d
    g :: Obj g
g = forall (a :: vk k k'). (CategoryOf (vk k k'), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g
    cg :: Companion hk g ~> Companion hk g
cg = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj g
g
    j :: Obj j
j = forall (a :: hk i a). (CategoryOf (hk i a), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j
    l :: Obj (Limit j d)
l = forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
forall (vk :: CAT s) (j :: hk i a) (k :: s) (d :: vk i k).
(HasLimits vk j k, Ob d) =>
Obj (Limit j d)
limitObj @vk @j @k @d
  in
    (Obj g
g Obj g -> Obj d -> O g d ~> O g d
forall {i :: s} (j :: s) (k :: s) (a :: vk j k) (b :: vk j k)
       (c :: vk i j) (d :: vk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj d
d)
      (O g d ~> O g d)
-> ((Ob (O g d), Ob (O g d)) => O g (Limit j d) ~> Limit j (O g d))
-> O g (Limit j d) ~> Limit j (O g d)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Obj g
g Obj g -> Obj (Limit j d) -> O g (Limit j d) ~> O g (Limit j d)
forall {i :: s} (j :: s) (k :: s) (a :: vk j k) (b :: vk j k)
       (c :: vk i j) (d :: vk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (Limit j d)
l)
      (O g (Limit j d) ~> O g (Limit j d))
-> ((Ob (O g (Limit j d)), Ob (O g (Limit j d))) =>
    O g (Limit j d) ~> Limit j (O g d))
-> O g (Limit j d) ~> Limit j (O g d)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall {s} {hk :: CAT s} {a :: s} {i :: s} (vk :: CAT s)
       (j :: hk i a) (k :: s) (d :: vk i k) (p :: vk a k).
(HasLimits vk j k, Ob d, Ob p) =>
(O (Companion hk p) j ~> Companion hk d) -> p ~> Limit j d
forall (vk :: CAT s) (j :: hk i a) (k :: s) (d :: vk i k)
       (p :: vk a k).
(HasLimits vk j k, Ob d, Ob p) =>
(O (Companion hk p) j ~> Companion hk d) -> p ~> Limit j d
limitUniv @vk @j @k' @(g `O` d)
        (Obj g
-> Obj d
-> O (Companion hk g) (Companion hk d) ~> Companion hk (O g d)
forall {j1 :: s} {j2 :: s} {k :: s} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose Obj g
g Obj d
d (O (Companion hk g) (Companion hk d) ~> Companion hk (O g d))
-> (O (Companion hk (O g (Limit j d))) j
    ~> O (Companion hk g) (Companion hk d))
-> O (Companion hk (O g (Limit j d))) j ~> Companion hk (O g d)
forall (b :: hk i k') (c :: hk i k') (a :: hk i k').
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Companion hk g ~> Companion hk g
cg (Companion hk g ~> Companion hk g)
-> (O (Companion hk (Limit j d)) j ~> Companion hk d)
-> O (Companion hk g) (O (Companion hk (Limit j d)) j)
   ~> O (Companion hk g) (Companion hk d)
forall {i :: s} (j :: s) (k :: s) (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 {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 @d) (O (Companion hk g) (O (Companion hk (Limit j d)) j)
 ~> O (Companion hk g) (Companion hk d))
-> (O (Companion hk (O g (Limit j d))) j
    ~> O (Companion hk g) (O (Companion hk (Limit j d)) j))
-> O (Companion hk (O g (Limit j d))) j
   ~> O (Companion hk g) (Companion hk d)
forall (b :: hk i k') (c :: hk i k') (a :: hk i k').
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Companion hk g ~> Companion hk g)
-> Obj (Companion hk (Limit j d))
-> Obj j
-> O (O (Companion hk g) (Companion hk (Limit j d))) j
   ~> O (Companion hk g) (O (Companion hk (Limit j d)) j)
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
       {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' Companion hk g ~> Companion hk g
cg (Obj (Limit j d) -> Obj (Companion hk (Limit j d))
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 Obj (Limit j d)
l) Obj j
j (O (O (Companion hk g) (Companion hk (Limit j d))) j
 ~> O (Companion hk g) (O (Companion hk (Limit j d)) j))
-> (O (Companion hk (O g (Limit j d))) j
    ~> O (O (Companion hk g) (Companion hk (Limit j d))) j)
-> O (Companion hk (O g (Limit j d))) j
   ~> O (Companion hk g) (O (Companion hk (Limit j d)) j)
forall (b :: hk i k') (c :: hk i k') (a :: hk i k').
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj g
-> Obj (Limit j d)
-> Companion hk (O g (Limit j d))
   ~> O (Companion hk g) (Companion hk (Limit j d))
forall {i :: s} {j :: s} {k :: s} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose Obj g
g Obj (Limit j d)
l (Companion hk (O g (Limit j d))
 ~> O (Companion hk g) (Companion hk (Limit j d)))
-> Obj j
-> O (Companion hk (O g (Limit j d))) j
   ~> O (O (Companion hk g) (Companion hk (Limit j d))) j
forall {i :: s} (j :: s) (k :: s) (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` Obj j
j))

-- | weighted colimits
type HasColimits :: forall {s} {hk :: CAT s} {a :: s} {i :: s}. CAT s -> hk a i -> s -> Constraint
class (HasCompanions 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
  colimit :: (Ob (d :: vk i k)) => Companion hk d `O` j ~> Companion hk (Colimit j d)
  colimitUniv :: (Ob (d :: vk i k), Ob p) => Companion hk d `O` j ~> Companion hk p -> Colimit j d ~> p

-- > a--c--k
-- > |  v  |
-- > j--@  |
-- > |  v  |
-- > i--d--k

-- lan :: f ~> Lan j f `O` j

-- > a--c--k
-- > |  v  |
-- > | /@\ |
-- > | v v |
-- > i-j-d-k