{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Adjunction where

import Data.Kind (Constraint)

import Proarrow.Category.Colimit (HasColimits (..), mapColimit)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (COREP, COREPK, REP, REPK, SUBCAT (..), Sub (..))
import Proarrow.Category.Limit (HasLimits (..), mapLimit)
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, lmap, rmap, (//), (:~>), type (+->))
import Proarrow.Functor (map)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep)
import Proarrow.Profunctor.Costar (Costar (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable
  ( CorepStar (..)
  , RepCostar (..)
  , Representable (..)
  , mapCorepStar
  , mapRepCostar
  , trivialRep
  )
import Proarrow.Profunctor.Star (Star (..))
import Proarrow.Promonad (Procomonad (..))

-- | Adjunctions as heteromorphisms.
class (Representable p, Corepresentable p) => Adjunction p

instance (Representable p, Corepresentable p) => Adjunction p

leftAdjunct :: forall p a b. (Adjunction p, Ob a) => (p %% a ~> b) -> a ~> p % b
leftAdjunct :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Adjunction p, Ob a) =>
((p %% a) ~> b) -> a ~> (p % b)
leftAdjunct = p a b -> a ~> (p % b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (p a b -> a ~> (p % b))
-> (((p %% a) ~> b) -> p a b) -> ((p %% a) ~> b) -> a ~> (p % b)
forall b c 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 {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate @p

rightAdjunct :: forall p a b. (Adjunction p, Ob b) => a ~> p % b -> (p %% a ~> b)
rightAdjunct :: forall {k} {k} (p :: k +-> k) (a :: k) (b :: k).
(Adjunction p, Ob b) =>
(a ~> (p % b)) -> (p %% a) ~> b
rightAdjunct = p a b -> (p %% a) ~> b
forall (a :: k) (b :: k). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex (p a b -> (p %% a) ~> b)
-> ((a ~> (p % b)) -> p a b) -> (a ~> (p % b)) -> (p %% a) ~> b
forall b c 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 {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: k +-> k) (b :: k) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p

unitRep :: forall p a. (Adjunction p, Ob a) => a ~> p % (p %% a)
unitRep :: forall {j} {k} (p :: j +-> k) (a :: k).
(Adjunction p, Ob a) =>
a ~> (p % (p %% a))
unitRep = p a (p %% a) -> a ~> (p % (p %% a))
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @p)

counitRep :: forall p a. (Adjunction p, Ob a) => p %% (p % a) ~> a
counitRep :: forall {k} {k} (p :: k +-> k) (a :: k).
(Adjunction p, Ob a) =>
(p %% (p % a)) ~> a
counitRep = p (p % a) a -> (p %% (p % a)) ~> a
forall (a :: k) (b :: k). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
trivialRep @p)

-- | The left adjoint of @((->) a)@ is @(,) a@.
instance Corepresentable (Star ((->) a)) where
  type Star ((->) a) %% b = (a, b)
  cotabulate :: forall a b.
Ob a =>
((Star ((->) a) %% a) ~> b) -> Star ((->) a) a b
cotabulate (Star ((->) a) %% a) ~> b
f = (a ~> (a -> b)) -> Star ((->) a) a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star \a
a a
b -> (Star ((->) a) %% a) ~> b
(a, a) -> b
f (a
b, a
a)
  coindex :: forall a b. Star ((->) a) a b -> (Star ((->) a) %% a) ~> b
coindex (Star a ~> (a -> b)
f) (a
a, a
b) = a ~> (a -> b)
a -> (a -> b)
f a
b a
a
  corepMap :: forall a b.
(a ~> b) -> (Star ((->) a) %% a) ~> (Star ((->) a) %% b)
corepMap = (a ~> b) -> (a, a) ~> (a, b)
(a ~> b) -> (Star ((->) a) %% a) ~> (Star ((->) a) %% b)
forall a b. (a ~> b) -> (a, a) ~> (a, b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map

-- | The right adjoint of @(,) a@ is @((->) a)@.
instance Representable (Costar ((,) a)) where
  type Costar ((,) a) % b = a -> b
  tabulate :: forall b a.
Ob b =>
(a ~> (Costar ((,) a) % b)) -> Costar ((,) a) a b
tabulate a ~> (Costar ((,) a) % b)
f = ((a, a) ~> b) -> Costar ((,) a) a b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar \(a
a, a
b) -> a ~> (Costar ((,) a) % b)
a -> (a -> b)
f a
b a
a
  index :: forall a b. Costar ((,) a) a b -> a ~> (Costar ((,) a) % b)
index (Costar (a, a) ~> b
g) a
a a
b = (a, a) ~> b
(a, a) -> b
g (a
b, a
a)
  repMap :: forall a b.
(a ~> b) -> (Costar ((,) a) % a) ~> (Costar ((,) a) % b)
repMap = (a ~> b) -> (Costar ((,) a) % a) ~> (Costar ((,) a) % b)
(a ~> b) -> (a -> a) ~> (a -> b)
forall a b. (a ~> b) -> (a -> a) ~> (a -> b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map

type Proadjunction :: forall {j} {k}. j +-> k -> k +-> j -> Constraint

-- | Adjunctions between two profunctors.
class (Profunctor p, Profunctor q) => Proadjunction (p :: j +-> k) (q :: k +-> j) where
  unit :: (Ob a) => (q :.: p) a a -- (~>) :~> q :.: p
  counit :: p :.: q :~> (~>)

instance (Representable f) => Proadjunction f (RepCostar f) where
  unit :: forall (a :: k). Ob a => (:.:) (RepCostar f) f a a
unit = RepCostar f a (RepCostar f %% a)
RepCostar f a (f % a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep RepCostar f a (f % a) -> f (f % a) a -> (:.:) (RepCostar f) f a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: f (f % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep
  counit :: (f :.: RepCostar f) :~> (~>)
counit (f a b
f :.: RepCostar f b b
g) = RepCostar f b b -> (RepCostar f %% b) ~> b
forall (a :: k) (b :: j).
RepCostar f a b -> (RepCostar f %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex RepCostar f b b
g ((f % b) ~> b) -> (a ~> (f % b)) -> a ~> b
forall (b :: j) (c :: j) (a :: j). (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
. f a b -> a ~> (f % b)
forall (a :: j) (b :: k). f a b -> a ~> (f % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index f a b
f

instance (Corepresentable f) => Proadjunction (CorepStar f) f where
  unit :: forall (a :: j). Ob a => (:.:) f (CorepStar f) a a
unit = f a (f %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep f a (f %% a) -> CorepStar f (f %% a) a -> (:.:) f (CorepStar f) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: CorepStar f (f %% a) a
CorepStar f (CorepStar f % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep
  counit :: (CorepStar f :.: f) :~> (~>)
counit (CorepStar f a b
f :.: f b b
g) = f b b -> (f %% b) ~> b
forall (a :: j) (b :: k). f a b -> (f %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex f b b
g ((f %% b) ~> b) -> (a ~> (f %% b)) -> a ~> b
forall (b :: k) (c :: k) (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
. CorepStar f a b -> a ~> (CorepStar f % b)
forall (a :: k) (b :: j). CorepStar f a b -> a ~> (CorepStar f % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index CorepStar f a b
f

instance (Proadjunction l1 r1, Proadjunction l2 r2) => Proadjunction (l1 :.: l2) (r2 :.: r1) where
  unit :: forall a. (Ob a) => ((r2 :.: r1) :.: (l1 :.: l2)) a a
  unit :: forall (a :: k). Ob a => (:.:) (r2 :.: r1) (l1 :.: l2) a a
unit = case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k +-> j) (q :: j +-> k) (a :: k).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @l2 @r2 @a of
    r2 a b
r2 :.: l2 b a
l2 ->
      l2 b a
l2 l2 b a
-> ((Ob b, Ob a) => (:.:) (r2 :.: r1) (l1 :.: l2) a a)
-> (:.:) (r2 :.: r1) (l1 :.: l2) a a
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: j +-> i) (q :: i +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @l1 @r1 of
        r1 b b
r1 :.: l1 b b
l1 -> (r2 a b
r2 r2 a b -> r1 b b -> (:.:) r2 r1 a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r1 b b
r1) (:.:) r2 r1 a b
-> (:.:) l1 l2 b a -> (:.:) (r2 :.: r1) (l1 :.: l2) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (l1 b b
l1 l1 b b -> l2 b a -> (:.:) l1 l2 b a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: l2 b a
l2)
  counit :: ((l1 :.: l2) :.: (r2 :.: r1)) :~> (~>)
counit ((l1 a b
l1 :.: l2 b b
l2) :.: (r2 b b
r2 :.: r1 b b
r1)) = (:.:) l1 r1 a b -> a ~> b
(l1 :.: r1) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit ((b ~> b) -> l1 a b -> l1 a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((:.:) l2 r2 b b -> b ~> b
(l2 :.: r2) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (l2 b b
l2 l2 b b -> r2 b b -> (:.:) l2 r2 b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r2 b b
r2)) l1 a b
l1 l1 a b -> r1 b b -> (:.:) l1 r1 a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r1 b b
r1)

instance (CategoryOf k) => Proadjunction (Id :: CAT k) Id where
  unit :: forall (a :: k). Ob a => (:.:) Id Id a a
unit = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Id a a -> Id a a -> (:.:) Id Id a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (Id :.: Id) :~> (~>)
counit (Id a ~> b
f :.: Id b ~> b
g) = b ~> b
g (b ~> b) -> (a ~> b) -> a ~> b
forall (b :: k) (c :: k) (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
. a ~> b
f

instance (Proadjunction q p) => Proadjunction (Op p) (Op q) where
  unit :: forall (a :: OPPOSITE j). Ob a => (:.:) (Op q) (Op p) a a
unit = case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @q @p of p (UN 'OP a) b
q :.: q b (UN 'OP a)
p -> q b (UN 'OP a) -> Op q ('OP (UN 'OP a)) ('OP b)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op q b (UN 'OP a)
p Op q a ('OP b) -> Op p ('OP b) a -> (:.:) (Op q) (Op p) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p (UN 'OP a) b -> Op p ('OP b) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op p (UN 'OP a) b
q
  counit :: (Op p :.: Op q) :~> (~>)
counit (Op p b1 a1
q :.: Op q b1 a1
p) = (b1 ~> a1) -> Op (~>) ('OP a1) ('OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((:.:) q p b1 a1 -> b1 ~> a1
(q :.: p) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (q b1 a1
p q b1 a1 -> p a1 a1 -> (:.:) q p b1 a1
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b1 a1
p a1 a1
q))

instance (Proadjunction p q) => Promonad (q :.: p) where
  id :: forall (a :: k). Ob a => (:.:) q p a a
id = (:.:) q p a a
forall (a :: k). Ob a => (:.:) q p a a
forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit
  (q b b
q :.: p b c
p) . :: forall (b :: k) (c :: k) (a :: k).
(:.:) q p b c -> (:.:) q p a b -> (:.:) q p a c
. (q a b
q' :.: p b b
p') = (b ~> b) -> q a b -> q a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((:.:) p q b b -> b ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (p b b
p' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q)) q a b
q' q a b -> p b c -> (:.:) q p a c
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b c
p

instance (Proadjunction p q) => Procomonad (p :.: q) where
  extract :: (p :.: q) :~> (~>)
extract = (:.:) p q a b -> a ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit
  duplicate :: (p :.: q) :~> ((p :.: q) :.: (p :.: q))
duplicate (p a b
p :.: q b b
q) = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) (p :.: q) (p :.: q) a b)
-> (:.:) (p :.: q) (p :.: q) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case (:.:) q p b b
forall (a :: j). Ob a => (:.:) q p a a
forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit of q b b
q' :.: p b b
p' -> (p a b
p p a b -> q b b -> (:.:) p q a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q') (:.:) p q a b -> (:.:) p q b b -> (:.:) (p :.: q) (p :.: q) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (p b b
p' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q)

-- (~>) :~> Colimit j c :.: r
--    <=>
-- j :~> c :.: r
--    <=>
-- (~>) :~> c :.: Limit j r

type LimitAdj :: (a +-> b) -> REPK a k +-> COREPK b k
data LimitAdj j c r where
  LimitAdj :: (Corepresentable c, Representable r) => (j :~> c :.: r) -> LimitAdj j (COREP c) (REP r)
instance (Profunctor j) => Profunctor (LimitAdj j) where
  dimap :: forall (c :: COREPK b k) (a :: COREPK b k) (b :: REPK a k)
       (d :: REPK a k).
(c ~> a) -> (b ~> d) -> LimitAdj j a b -> LimitAdj j c d
dimap (Sub (Op (Prof b1 :~> a1
l))) (Sub (Prof a1 :~> b1
r)) (LimitAdj j :~> (c :.: r)
n) = (j :~> (a1 :.: b1)) -> LimitAdj j (COREP a1) (SUB b1)
forall {j} {k} {i} (c :: j +-> k) (r :: i +-> j) (j :: i +-> k).
(Corepresentable c, Representable r) =>
(j :~> (c :.: r)) -> LimitAdj j (COREP c) (REP r)
LimitAdj (\j a b
j -> case j a b -> (:.:) c r a b
j :~> (c :.: r)
n j a b
j of c a b
c :.: r b b
d -> b1 a b -> a1 a b
b1 :~> a1
l b1 a b
c a b
c a1 a b -> b1 b b -> (:.:) a1 b1 a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: a1 b b -> b1 b b
a1 :~> b1
r a1 b b
r b b
d)
  (Ob a, Ob b) => r
r \\ :: forall (a :: COREPK b k) (b :: REPK a k) r.
((Ob a, Ob b) => r) -> LimitAdj j a b -> r
\\ LimitAdj j :~> (c :.: r)
f = r
(Ob (j (ZonkAny 0) (ZonkAny 1)),
 Ob ((:.:) c r (ZonkAny 0) (ZonkAny 1))) =>
r
(Ob a, Ob b) => r
r ((Ob (j (ZonkAny 0) (ZonkAny 1)),
  Ob ((:.:) c r (ZonkAny 0) (ZonkAny 1))) =>
 r)
-> (j (ZonkAny 0) (ZonkAny 1) -> (:.:) c r (ZonkAny 0) (ZonkAny 1))
-> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ j (ZonkAny 0) (ZonkAny 1) -> (:.:) c r (ZonkAny 0) (ZonkAny 1)
j :~> (c :.: r)
f

-- | Colimit j -| Limit j
instance (HasLimits j k) => Representable (LimitAdj (j :: a +-> b) :: REPK a k +-> COREPK b k) where
  type LimitAdj j % r = COREP (RepCostar (Limit j (UN SUB r)))
  index :: forall (a :: COREPK b k) (b :: REPK a k).
LimitAdj j a b -> a ~> (LimitAdj j % b)
index @c (LimitAdj j :~> (c :.: r)
n) =
    Op Prof ('OP c) ('OP (RepCostar (Limit j r)))
-> Sub (Op Prof) (SUB ('OP c)) (SUB ('OP (RepCostar (Limit j r))))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub
      ( Prof (RepCostar (Limit j r)) c
-> Op Prof ('OP c) ('OP (RepCostar (Limit j r)))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op
          ( (RepCostar (Limit j r) :~> c) -> Prof (RepCostar (Limit j r)) c
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(RepCostar @o (Limit j r % a) ~> b
l) ->
              ((c %% a) ~> b) -> c a b
forall (a :: b) (b :: k). Ob a => ((c %% a) ~> b) -> c a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate
                ( (Limit j r % a) ~> b
l
                    ((Limit j r % a) ~> b)
-> ((c %% a) ~> (Limit j r % a)) -> (c %% a) ~> b
forall (b :: k) (c :: k) (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
. Limit j r (c %% a) a -> (c %% a) ~> (Limit j r % a)
forall (a :: k) (b :: b). Limit j r a b -> a ~> (Limit j r % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index
                      ( forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: a +-> b) k (d :: a +-> k) (p :: b +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j @k
                          (\(CorepStar c a b
g :.: j b b
j) -> case j b b -> (:.:) c r b b
j :~> (c :.: r)
n j b b
j of c b b
c :.: r b b
r -> (a ~> b) -> r b b -> r a b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (c b b -> (c %% b) ~> b
forall (a :: b) (b :: k). c a b -> (c %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex c b b
c ((c %% b) ~> b) -> (a ~> (c %% b)) -> a ~> b
forall (b :: k) (c :: k) (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
. CorepStar c a b -> a ~> (CorepStar c % b)
forall (a :: k) (b :: b). CorepStar c a b -> a ~> (CorepStar c % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index CorepStar c a b
g) r b b
r)
                          (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: b +-> k) (a :: b).
(Representable p, Ob a) =>
p (p % a) a
trivialRep @(CorepStar (UN OP (UN SUB c))) @o)
                      )
                )
          )
      )
  tabulate :: forall (b :: REPK a k) (a :: COREPK b k).
Ob b =>
(a ~> (LimitAdj j % b)) -> LimitAdj j a b
tabulate @(SUB r) (Sub (Op (Prof RepCostar (Limit j (UN SUB b)) :~> a1
n))) = (j :~> (a1 :.: UN SUB b)) -> LimitAdj j (COREP a1) (SUB (UN SUB b))
forall {j} {k} {i} (c :: j +-> k) (r :: i +-> j) (j :: i +-> k).
(Corepresentable c, Representable r) =>
(j :~> (c :.: r)) -> LimitAdj j (COREP c) (REP r)
LimitAdj (\j a b
j -> RepCostar (Limit j (UN SUB b)) a (UN SUB b % b)
-> a1 a (UN SUB b % b)
RepCostar (Limit j (UN SUB b)) :~> a1
n (((Limit j (UN SUB b) % a) ~> (UN SUB b % b))
-> RepCostar (Limit j (UN SUB b)) a (UN SUB b % b)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: a +-> k) (a :: k) (b :: a).
Representable p =>
p a b -> a ~> (p % b)
index @r ((:.:) (Limit j (UN SUB b)) j (Limit j (UN SUB b) % a) b
-> UN SUB b (Limit j (UN SUB b) % a) b
(Limit j (UN SUB b) :.: j) :~> UN SUB b
forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (d :: a +-> k). Representable d => (Limit j d :.: j) :~> d
limit (Limit j (UN SUB b) (Limit j (UN SUB b) % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep Limit j (UN SUB b) (Limit j (UN SUB b) % a) a
-> j a b -> (:.:) (Limit j (UN SUB b)) j (Limit j (UN SUB b) % a) b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j a b
j)))) a1 a (UN SUB b % b)
-> UN SUB b (UN SUB b % b) b -> (:.:) a1 (UN SUB b) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: UN SUB b (UN SUB b % b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep ((Ob a, Ob b) => (:.:) a1 (UN SUB b) a b)
-> j a b -> (:.:) a1 (UN SUB b) a b
forall (a :: b) (b :: a) r. ((Ob a, Ob b) => r) -> j a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ j a b
j)
  repMap :: forall (a :: REPK a k) (b :: REPK a k).
(a ~> b) -> (LimitAdj j % a) ~> (LimitAdj j % b)
repMap (Sub Prof a1 b1
n) = Op
  Prof ('OP (RepCostar (Limit j a1))) ('OP (RepCostar (Limit j b1)))
-> Sub
     (Op Prof)
     (SUB ('OP (RepCostar (Limit j a1))))
     (SUB ('OP (RepCostar (Limit j b1))))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (Prof (RepCostar (Limit j b1)) (RepCostar (Limit j a1))
-> Op
     Prof ('OP (RepCostar (Limit j a1))) ('OP (RepCostar (Limit j b1)))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((Limit j a1 ~> Limit j b1)
-> RepCostar (Limit j b1) ~> RepCostar (Limit j a1)
forall {k} {j} (p :: k +-> j) (q :: k +-> j).
(Representable p, Representable q) =>
(p ~> q) -> RepCostar q ~> RepCostar p
mapRepCostar (forall {a} {i} (j :: i +-> a) k (p :: i +-> k) (q :: i +-> k).
(HasLimits j k, Representable p, Representable q) =>
(p ~> q) -> Limit j p ~> Limit j q
forall (j :: a +-> b) k (p :: a +-> k) (q :: a +-> k).
(HasLimits j k, Representable p, Representable q) =>
(p ~> q) -> Limit j p ~> Limit j q
mapLimit @j a1 ~> b1
Prof a1 b1
n)))

instance (HasColimits j k) => Corepresentable (LimitAdj (j :: a +-> b) :: REPK a k +-> COREPK b k) where
  type LimitAdj j %% c = REP (CorepStar (Colimit j (UN OP (UN SUB c))))
  cotabulate :: forall (a :: COREPK b k) (b :: REPK a k).
Ob a =>
((LimitAdj j %% a) ~> b) -> LimitAdj j a b
cotabulate @(SUB (OP r)) (Sub (Prof CorepStar (Colimit j (UN 'OP (UN SUB a))) :~> b1
n)) = (j :~> (UN 'OP (UN SUB a) :.: b1))
-> LimitAdj j (COREP (UN 'OP (UN SUB a))) (SUB b1)
forall {j} {k} {i} (c :: j +-> k) (r :: i +-> j) (j :: i +-> k).
(Corepresentable c, Representable r) =>
(j :~> (c :.: r)) -> LimitAdj j (COREP c) (REP r)
LimitAdj (\j a b
j -> UN 'OP (UN SUB a) a (UN 'OP (UN SUB a) %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep UN 'OP (UN SUB a) a (UN 'OP (UN SUB a) %% a)
-> b1 (UN 'OP (UN SUB a) %% a) b
-> (:.:) (UN 'OP (UN SUB a)) b1 a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: CorepStar
  (Colimit j (UN 'OP (UN SUB a))) (UN 'OP (UN SUB a) %% a) b
-> b1 (UN 'OP (UN SUB a) %% a) b
CorepStar (Colimit j (UN 'OP (UN SUB a))) :~> b1
n (((UN 'OP (UN SUB a) %% a) ~> (Colimit j (UN 'OP (UN SUB a)) %% b))
-> CorepStar
     (Colimit j (UN 'OP (UN SUB a))) (UN 'OP (UN SUB a) %% a) b
forall {j} {k} (b :: j) (a :: k) (p :: k +-> j).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> b) (a :: b) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @r ((:.:)
  j
  (Colimit j (UN 'OP (UN SUB a)))
  a
  (Colimit j (UN 'OP (UN SUB a)) %% b)
-> UN 'OP (UN SUB a) a (Colimit j (UN 'OP (UN SUB a)) %% b)
(j :.: Colimit j (UN 'OP (UN SUB a))) :~> UN 'OP (UN SUB a)
forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (d :: k +-> b).
Corepresentable d =>
(j :.: Colimit j d) :~> d
colimit (j a b
j j a b
-> Colimit
     j (UN 'OP (UN SUB a)) b (Colimit j (UN 'OP (UN SUB a)) %% b)
-> (:.:)
     j
     (Colimit j (UN 'OP (UN SUB a)))
     a
     (Colimit j (UN 'OP (UN SUB a)) %% b)
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Colimit
  j (UN 'OP (UN SUB a)) b (Colimit j (UN 'OP (UN SUB a)) %% b)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep)))) ((Ob a, Ob b) => (:.:) (UN 'OP (UN SUB a)) b1 a b)
-> j a b -> (:.:) (UN 'OP (UN SUB a)) b1 a b
forall (a :: b) (b :: a) r. ((Ob a, Ob b) => r) -> j a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ j a b
j)
  coindex :: forall (a :: COREPK b k) (b :: REPK a k).
LimitAdj j a b -> (LimitAdj j %% a) ~> b
coindex @_ @r (LimitAdj j :~> (c :.: r)
n) =
    Prof (CorepStar (Colimit j c)) r
-> Sub Prof (SUB (CorepStar (Colimit j c))) (SUB r)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub
      ( (CorepStar (Colimit j c) :~> r) -> Prof (CorepStar (Colimit j c)) r
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(CorepStar @o a ~> (Colimit j c %% b)
l) ->
          (a ~> (r % b)) -> r a b
forall (b :: a) (a :: k). Ob b => (a ~> (r % b)) -> r a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate
            ( Colimit j c b (r % b) -> (Colimit j c %% b) ~> (r % b)
forall (a :: a) (b :: k).
Colimit j c a b -> (Colimit j c %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex
                ( forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: a +-> b) k (d :: k +-> b) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j @k
                    (\(j a b
j :.: RepCostar r b b
p) -> case j a b -> (:.:) c r a b
j :~> (c :.: r)
n j a b
j of c a b
c :.: r b b
r -> (b ~> b) -> c a b -> c a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (RepCostar r b b -> (RepCostar r %% b) ~> b
forall (a :: a) (b :: k).
RepCostar r a b -> (RepCostar r %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex RepCostar r b b
p ((r % b) ~> b) -> (b ~> (r % b)) -> b ~> b
forall (b :: k) (c :: k) (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
. r b b -> b ~> (r % b)
forall (a :: k) (b :: a). r a b -> a ~> (r % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index r b b
r) c a b
c)
                    (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: k +-> a) (a :: a).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @(RepCostar (UN SUB r)) @o)
                )
                ((Colimit j c %% b) ~> (r % b))
-> (a ~> (Colimit j c %% b)) -> a ~> (r % b)
forall (b :: k) (c :: k) (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
. a ~> (Colimit j c %% b)
l
            )
      )
  corepMap :: forall (a :: COREPK b k) (b :: COREPK b k).
(a ~> b) -> (LimitAdj j %% a) ~> (LimitAdj j %% b)
corepMap (Sub (Op Prof b1 a1
n)) = Prof (CorepStar (Colimit j a1)) (CorepStar (Colimit j b1))
-> Sub
     Prof
     (SUB (CorepStar (Colimit j a1)))
     (SUB (CorepStar (Colimit j b1)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((Colimit j b1 ~> Colimit j a1)
-> CorepStar (Colimit j a1) ~> CorepStar (Colimit j b1)
forall {k} {j} (p :: k +-> j) (q :: k +-> j).
(Corepresentable p, Corepresentable q) =>
(p ~> q) -> CorepStar q ~> CorepStar p
mapCorepStar (forall {a} {i} (j :: a +-> i) k (p :: k +-> i) (q :: k +-> i).
(HasColimits j k, Corepresentable p, Corepresentable q) =>
(p ~> q) -> Colimit j p ~> Colimit j q
forall (j :: a +-> b) k (p :: k +-> b) (q :: k +-> b).
(HasColimits j k, Corepresentable p, Corepresentable q) =>
(p ~> q) -> Colimit j p ~> Colimit j q
mapColimit @j b1 ~> a1
Prof b1 a1
n))

rightAdjointPreservesLimits
  :: forall {k} {k'} {i} {a} (j :: i +-> a) (p :: k +-> k') (d :: i +-> k)
   . (Adjunction p, Representable d, HasLimits j k, HasLimits j k')
  => Limit j (p :.: d) :~> p :.: Limit j d
rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (j :: i +-> a) (p :: k +-> k')
       (d :: i +-> k).
(Adjunction p, Representable d, HasLimits j k, HasLimits j k') =>
Limit j (p :.: d) :~> (p :.: Limit j d)
rightAdjointPreservesLimits Limit j (p :.: d) a b
lim =
  forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: k +-> k') (a :: k').
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @p
    p a (p %% a) -> Limit j d (p %% a) b -> (:.:) p (Limit j d) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j @k @d
      (\((CorepStar p a b
f' :.: Limit j (p :.: d) b b
lim') :.: j b b
j) -> case forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
limit @j @k' @(p :.: d) (Limit j (p :.: d) b b
lim' Limit j (p :.: d) b b -> j b b -> (:.:) (Limit j (p :.: d)) j b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j b b
j) of p b b
g' :.: d b b
d -> (a ~> b) -> d b b -> d a b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (p b b -> (p %% b) ~> b
forall (a :: k') (b :: k). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p b b
g' ((p %% b) ~> b) -> (a ~> (p %% b)) -> a ~> b
forall (b :: k) (c :: k) (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
. CorepStar p a b -> a ~> (CorepStar p % b)
forall (a :: k) (b :: k').
CorepStar p a b -> a ~> (CorepStar p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index CorepStar p a b
f') d b b
d)
      (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k' +-> k) (a :: k').
(Representable p, Ob a) =>
p (p % a) a
trivialRep @(CorepStar p) CorepStar p (p %% a) a
-> Limit j (p :.: d) a b
-> (:.:) (CorepStar p) (Limit j (p :.: d)) (p %% a) b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Limit j (p :.: d) a b
lim)
    ((Ob a, Ob b) => (:.:) p (Limit j d) a b)
-> Limit j (p :.: d) a b -> (:.:) p (Limit j d) a b
forall (a :: k') (b :: a) r.
((Ob a, Ob b) => r) -> Limit j (p :.: d) a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Limit j (p :.: d) a b
lim

rightAdjointPreservesLimitsInv
  :: forall {k} {k'} {i} {a} (p :: k +-> k') (d :: i +-> k) (j :: i +-> a)
   . (Representable p, Representable d, HasLimits j k, HasLimits j k')
  => p :.: Limit j d :~> Limit j (p :.: d)
rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (p :: k +-> k') (d :: i +-> k)
       (j :: i +-> a).
(Representable p, Representable d, HasLimits j k,
 HasLimits j k') =>
(p :.: Limit j d) :~> Limit j (p :.: d)
rightAdjointPreservesLimitsInv = forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j @k' @(p :.: d) (\((p a b
p :.: Limit j d b b
lim) :.: j b b
j) -> p a b
p p a b -> d b b -> (:.:) p d a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (:.:) (Limit j d) j b b -> d b b
(Limit j d :.: j) :~> d
forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d
limit (Limit j d b b
lim Limit j d b b -> j b b -> (:.:) (Limit j d) j b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j b b
j))

leftAdjointPreservesColimits
  :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i) (j :: a +-> i)
   . (Adjunction p, Corepresentable d, HasColimits j k, HasColimits j k')
  => Colimit j (d :.: p) :~> Colimit j d :.: p
leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i)
       (j :: a +-> i).
(Adjunction p, Corepresentable d, HasColimits j k,
 HasColimits j k') =>
Colimit j (d :.: p) :~> (Colimit j d :.: p)
leftAdjointPreservesColimits Colimit j (d :.: p) a b
colim =
  forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j @k @d
    (\(j a b
j :.: (Colimit j (d :.: p) b b
colim' :.: RepCostar p b b
g')) -> case forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
colimit @j @k' @(d :.: p) (j a b
j j a b
-> Colimit j (d :.: p) b b -> (:.:) j (Colimit j (d :.: p)) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Colimit j (d :.: p) b b
colim') of d a b
d :.: p b b
f' -> (b ~> b) -> d a b -> d a b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (RepCostar p b b -> (RepCostar p %% b) ~> b
forall (a :: k') (b :: k).
RepCostar p a b -> (RepCostar p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex RepCostar p b b
g' ((p % b) ~> b) -> (b ~> (p % b)) -> b ~> b
forall (b :: k) (c :: k) (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
. p b b -> b ~> (p % b)
forall (a :: k) (b :: k'). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p b b
f') d a b
d)
    (Colimit j (d :.: p) a b
colim Colimit j (d :.: p) a b
-> RepCostar p b (p % b)
-> (:.:) (Colimit j (d :.: p)) (RepCostar p) a (p % b)
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: k +-> k') (a :: k').
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @(RepCostar p))
    Colimit j d a (p % b) -> p (p % b) b -> (:.:) (Colimit j d) p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k' +-> k) (a :: k').
(Representable p, Ob a) =>
p (p % a) a
trivialRep @p
    ((Ob a, Ob b) => (:.:) (Colimit j d) p a b)
-> Colimit j (d :.: p) a b -> (:.:) (Colimit j d) p a b
forall (a :: a) (b :: k') r.
((Ob a, Ob b) => r) -> Colimit j (d :.: p) a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Colimit j (d :.: p) a b
colim

leftAdjointPreservesColimitsInv
  :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i) (j :: a +-> i)
   . (Corepresentable p, Corepresentable d, HasColimits j k, HasColimits j k')
  => Colimit j d :.: p :~> Colimit j (d :.: p)
leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (p :: k' +-> k) (d :: k +-> i)
       (j :: a +-> i).
(Corepresentable p, Corepresentable d, HasColimits j k,
 HasColimits j k') =>
(Colimit j d :.: p) :~> Colimit j (d :.: p)
leftAdjointPreservesColimitsInv = forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j @k' @(d :.: p) (\(j a b
j :.: (Colimit j d b b
colim :.: p b b
p)) -> (:.:) j (Colimit j d) a b -> d a b
(j :.: Colimit j d) :~> d
forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (d :: k +-> i).
Corepresentable d =>
(j :.: Colimit j d) :~> d
colimit (j a b
j j a b -> Colimit j d b b -> (:.:) j (Colimit j d) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Colimit j d b b
colim) d a b -> p b b -> (:.:) d p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
p)