module Proarrow.Category.Bicategory.Prof where

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

import Data.Proxy (Proxy (..))
import Data.Reflection (Reifies (..), reify)
import Proarrow.Adjunction qualified as A
import Proarrow.Category.Bicategory
  ( Adjunction (..)
  , Bicategory (..)
  , Bimodule (..)
  , Comonad (..)
  , Monad (..)
  )
import Proarrow.Category.Bicategory.Co (COK (..), Co (..))
import Proarrow.Category.Bicategory.Kan (RightKanExtension (..), RightKanLift (..))
import Proarrow.Category.Bicategory.Sub (IsOb, SUBCAT (..), Sub (..))
import Proarrow.Category.Colimit qualified as L
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..), vArr)
import Proarrow.Category.Equipment.Limit (HasColimits (..), HasLimits (..))
import Proarrow.Category.Instance.Collage (COLLAGE (..), Collage (..), InjL (..), InjR (..))
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (unProf)
import Proarrow.Category.Limit qualified as L
import Proarrow.Category.Opposite qualified as Op
import Proarrow.Core
  ( CAT
  , Category
  , CategoryOf (..)
  , Is
  , Profunctor (..)
  , Promonad (..)
  , UN
  , arr
  , dimapDefault
  , lmap
  , obj
  , rmap
  , src
  , tgt
  , (//)
  , (:~>)
  , type (+->)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Ran qualified as R
import Proarrow.Profunctor.Representable (RepCostar (..), Representable (..), dimapRep)
import Proarrow.Profunctor.Rift qualified as R
import Proarrow.Promonad (Procomonad (..))

type data PROFK j k = PK (j +-> k)
type instance UN PK (PK p) = p

type Prof :: CAT (PROFK j k)
data Prof p q where
  Prof :: (Ob p, Ob q) => p :~> q -> Prof (PK p) (PK q)

instance Profunctor Prof where
  dimap :: forall (c :: PROFK j k) (a :: PROFK j k) (b :: PROFK j k)
       (d :: PROFK j k).
(c ~> a) -> (b ~> d) -> Prof a b -> Prof c d
dimap = (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d
Prof c a -> Prof b d -> Prof a b -> Prof c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: PROFK j k) (b :: PROFK j k) r.
((Ob a, Ob b) => r) -> Prof a b -> r
\\ Prof p :~> q
n = r
(Ob (p Any Any), Ob (q Any Any)) => r
(Ob a, Ob b) => r
r ((Ob (p Any Any), Ob (q Any Any)) => r)
-> (p Any Any -> q Any Any) -> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p Any Any -> q Any Any
p :~> q
n
instance Promonad Prof where
  id :: forall (a :: PROFK j k). Ob a => Prof a a
id = (UN PK a :~> UN PK a) -> Prof (PK (UN PK a)) (PK (UN PK a))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof UN PK a a b -> UN PK a a b
UN PK a :~> UN PK a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Prof p :~> q
m . :: forall (b :: PROFK j k) (c :: PROFK j k) (a :: PROFK j k).
Prof b c -> Prof a b -> Prof a c
. Prof p :~> q
n = (p :~> q) -> Prof (PK p) (PK q)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (p a b -> q a b
p :~> q
m (p a b -> q a b) -> (p a b -> p a b) -> p a b -> q a b
forall b c a. (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
. p a b -> p a b
p a b -> q a b
p :~> q
n)
instance CategoryOf (PROFK j k) where
  type (~>) = Prof
  type Ob p = (Is PK p, Profunctor (UN PK p))

instance Bicategory PROFK where
  type Ob0 PROFK k = CategoryOf k
  type I = PK Id
  type p `O` q = PK (UN PK p :.: UN PK q)
  Prof p :~> q
m o :: forall {i} j k (a :: PROFK j k) (b :: PROFK j k) (c :: PROFK i j)
       (d :: PROFK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Prof p :~> q
n = ((p :.: p) :~> (q :.: q)) -> Prof (PK (p :.: p)) (PK (q :.: q))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((p :.: p) :~> (q :.: q)) -> Prof (PK (p :.: p)) (PK (q :.: q)))
-> ((p :.: p) :~> (q :.: q)) -> Prof (PK (p :.: p)) (PK (q :.: q))
forall a b. (a -> b) -> a -> b
$ \(p a b
p :.: p b b
q) -> p a b -> q a b
p :~> q
m p a b
p q a b -> q b b -> (:.:) q 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 -> q b b
p :~> q
n p b b
q
  (Ob0 PROFK i, Ob0 PROFK j, Ob ps, Ob qs) => r
r \\\ :: forall i j (ps :: PROFK i j) (qs :: PROFK i j) r.
((Ob0 PROFK i, Ob0 PROFK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Prof{} = r
(Ob0 PROFK i, Ob0 PROFK j, Ob ps, Ob qs) => r
r
  leftUnitor :: forall {i} {j} (a :: PROFK i j).
(Ob0 PROFK i, Ob0 PROFK j, Ob a) =>
O I a ~> a
leftUnitor = ((Id :.: UN PK a) :~> UN PK a)
-> Prof (PK (Id :.: UN PK a)) (PK (UN PK a))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((Id :.: UN PK a) :~> UN PK a)
 -> Prof (PK (Id :.: UN PK a)) (PK (UN PK a)))
-> ((Id :.: UN PK a) :~> UN PK a)
-> Prof (PK (Id :.: UN PK a)) (PK (UN PK a))
forall a b. (a -> b) -> a -> b
$ \(Id a ~> b
h :.: UN PK a b b
q) -> (a ~> b) -> UN PK a b b -> UN PK a a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
h UN PK a b b
q
  leftUnitorInv :: forall {i} {j} (a :: PROFK i j).
(Ob0 PROFK i, Ob0 PROFK j, Ob a) =>
a ~> O I a
leftUnitorInv = (UN PK a :~> (Id :.: UN PK a))
-> Prof (PK (UN PK a)) (PK (Id :.: UN PK a))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((UN PK a :~> (Id :.: UN PK a))
 -> Prof (PK (UN PK a)) (PK (Id :.: UN PK a)))
-> (UN PK a :~> (Id :.: UN PK a))
-> Prof (PK (UN PK a)) (PK (Id :.: UN PK a))
forall a b. (a -> b) -> a -> b
$ \UN PK a a b
p -> (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (UN PK a a b -> a ~> a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src UN PK a a b
p) Id a a -> UN PK a a b -> (:.:) Id (UN PK a) 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 PK a a b
p
  rightUnitor :: forall {i} {j} (a :: PROFK i j).
(Ob0 PROFK i, Ob0 PROFK j, Ob a) =>
O a I ~> a
rightUnitor = ((UN PK a :.: Id) :~> UN PK a)
-> Prof (PK (UN PK a :.: Id)) (PK (UN PK a))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((UN PK a :.: Id) :~> UN PK a)
 -> Prof (PK (UN PK a :.: Id)) (PK (UN PK a)))
-> ((UN PK a :.: Id) :~> UN PK a)
-> Prof (PK (UN PK a :.: Id)) (PK (UN PK a))
forall a b. (a -> b) -> a -> b
$ \(UN PK a a b
p :.: Id b ~> b
h) -> (b ~> b) -> UN PK a a b -> UN PK a a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> b
h UN PK a a b
p
  rightUnitorInv :: forall {i} {j} (a :: PROFK i j).
(Ob0 PROFK i, Ob0 PROFK j, Ob a) =>
a ~> O a I
rightUnitorInv = (UN PK a :~> (UN PK a :.: Id))
-> Prof (PK (UN PK a)) (PK (UN PK a :.: Id))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((UN PK a :~> (UN PK a :.: Id))
 -> Prof (PK (UN PK a)) (PK (UN PK a :.: Id)))
-> (UN PK a :~> (UN PK a :.: Id))
-> Prof (PK (UN PK a)) (PK (UN PK a :.: Id))
forall a b. (a -> b) -> a -> b
$ \UN PK a a b
p -> UN PK a a b
p UN PK a a b -> Id b b -> (:.:) (UN PK a) Id 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
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (UN PK a a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt UN PK a a b
p)
  associator :: forall {h} {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j)
       (c :: PROFK h i).
(Ob0 PROFK h, Ob0 PROFK i, Ob0 PROFK j, Ob0 PROFK k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator = (((UN PK a :.: UN PK b) :.: UN PK c)
 :~> (UN PK a :.: (UN PK b :.: UN PK c)))
-> Prof
     (PK ((UN PK a :.: UN PK b) :.: UN PK c))
     (PK (UN PK a :.: (UN PK b :.: UN PK c)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((((UN PK a :.: UN PK b) :.: UN PK c)
  :~> (UN PK a :.: (UN PK b :.: UN PK c)))
 -> Prof
      (PK ((UN PK a :.: UN PK b) :.: UN PK c))
      (PK (UN PK a :.: (UN PK b :.: UN PK c))))
-> (((UN PK a :.: UN PK b) :.: UN PK c)
    :~> (UN PK a :.: (UN PK b :.: UN PK c)))
-> Prof
     (PK ((UN PK a :.: UN PK b) :.: UN PK c))
     (PK (UN PK a :.: (UN PK b :.: UN PK c)))
forall a b. (a -> b) -> a -> b
$ \((UN PK a a b
p :.: UN PK b b b
q) :.: UN PK c b b
r) -> UN PK a a b
p UN PK a a b
-> (:.:) (UN PK b) (UN PK c) b b
-> (:.:) (UN PK a) (UN PK b :.: UN PK c) 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 PK b b b
q UN PK b b b -> UN PK c b b -> (:.:) (UN PK b) (UN PK c) 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
:.: UN PK c b b
r)
  associatorInv :: forall {h} {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j)
       (c :: PROFK h i).
(Ob0 PROFK h, Ob0 PROFK i, Ob0 PROFK j, Ob0 PROFK k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv = ((UN PK a :.: (UN PK b :.: UN PK c))
 :~> ((UN PK a :.: UN PK b) :.: UN PK c))
-> Prof
     (PK (UN PK a :.: (UN PK b :.: UN PK c)))
     (PK ((UN PK a :.: UN PK b) :.: UN PK c))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((UN PK a :.: (UN PK b :.: UN PK c))
  :~> ((UN PK a :.: UN PK b) :.: UN PK c))
 -> Prof
      (PK (UN PK a :.: (UN PK b :.: UN PK c)))
      (PK ((UN PK a :.: UN PK b) :.: UN PK c)))
-> ((UN PK a :.: (UN PK b :.: UN PK c))
    :~> ((UN PK a :.: UN PK b) :.: UN PK c))
-> Prof
     (PK (UN PK a :.: (UN PK b :.: UN PK c)))
     (PK ((UN PK a :.: UN PK b) :.: UN PK c))
forall a b. (a -> b) -> a -> b
$ \(UN PK a a b
p :.: (UN PK b b b
q :.: UN PK c b b
r)) -> (UN PK a a b
p UN PK a a b -> UN PK b b b -> (:.:) (UN PK a) (UN PK 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 PK b b b
q) (:.:) (UN PK a) (UN PK b) a b
-> UN PK c b b -> (:.:) (UN PK a :.: UN PK b) (UN PK c) 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 PK c b b
r

data ProfRep
type instance IsOb ProfRep p = Representable (UN PK p)

type FUNK = SUBCAT ProfRep PROFK
type FUN p = SUB @ProfRep (PK p)
type UNFUN p = UN PK (UN SUB p)

instance HasCompanions PROFK FUNK where
  type Companion PROFK p = PK (UNFUN p)
  mapCompanion :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k).
(f ~> g) -> Companion PROFK f ~> Companion PROFK g
mapCompanion (Sub (Prof p :~> q
n)) = (p :~> q) -> Prof (PK p) (PK q)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof p a b -> q a b
p :~> q
n
  compToId :: forall k. Ob0 FUNK k => Companion PROFK I ~> I
compToId = (Id :~> Id) -> Prof (PK Id) (PK Id)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof Id a b -> Id a b
Id :~> Id
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  compFromId :: forall k. Ob0 FUNK k => I ~> Companion PROFK I
compFromId = (Id :~> Id) -> Prof (PK Id) (PK Id)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof Id a b -> Id a b
Id :~> Id
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  compToCompose :: forall {i} {j} {k} (f :: FUNK j k) (g :: FUNK i j).
Obj f
-> Obj g
-> Companion PROFK (O f g)
   ~> O (Companion PROFK f) (Companion PROFK g)
compToCompose Obj f
f Obj g
g = ((UN PK (UN SUB f) :.: UN PK (UN SUB g))
 :~> (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
-> Prof
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (:.:) (UN PK (UN SUB f)) (UN PK (UN SUB g)) a b
-> (:.:) (UN PK (UN SUB f)) (UN PK (UN SUB g)) a b
(UN PK (UN SUB f) :.: UN PK (UN SUB g))
:~> (UN PK (UN SUB f) :.: UN PK (UN SUB g))
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob f, Ob f) =>
 Prof
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g))))
-> Sub f f
-> Prof
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FUNK j k) (b :: FUNK j k) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Obj f
Sub f f
f ((Ob g, Ob g) =>
 Prof
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g))))
-> Sub g g
-> Prof
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FUNK i j) (b :: FUNK i j) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Obj g
Sub g g
g
  compFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2).
Obj f
-> Obj g
-> O (Companion PROFK f) (Companion PROFK g)
   ~> Companion PROFK (O f g)
compFromCompose Obj f
f Obj g
g = ((UN PK (UN SUB f) :.: UN PK (UN SUB g))
 :~> (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
-> Prof
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (:.:) (UN PK (UN SUB f)) (UN PK (UN SUB g)) a b
-> (:.:) (UN PK (UN SUB f)) (UN PK (UN SUB g)) a b
(UN PK (UN SUB f) :.: UN PK (UN SUB g))
:~> (UN PK (UN SUB f) :.: UN PK (UN SUB g))
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob f, Ob f) =>
 Prof
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g))))
-> Sub f f
-> Prof
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FUNK j2 k) (b :: FUNK j2 k) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Obj f
Sub f f
f ((Ob g, Ob g) =>
 Prof
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
   (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g))))
-> Sub g g
-> Prof
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
     (PK (UN PK (UN SUB f) :.: UN PK (UN SUB g)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FUNK j1 j2) (b :: FUNK j1 j2) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Obj g
Sub g g
g

instance Equipment PROFK FUNK where
  type Conjoint PROFK p = PK (RepCostar (UNFUN p))
  mapConjoint :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k).
(f ~> g) -> Conjoint PROFK g ~> Conjoint PROFK f
mapConjoint (Sub (Prof @p p :~> q
n)) = (RepCostar q :~> RepCostar p)
-> Prof (PK (RepCostar q)) (PK (RepCostar p))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(RepCostar @a (q % a) ~> b
f) -> ((p % a) ~> b) -> RepCostar p a b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((q % a) ~> b
f ((q % a) ~> b) -> ((p % a) ~> (q % a)) -> (p % a) ~> b
forall (b :: k) (c :: k) (a :: 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
. q (p % a) a -> (p % a) ~> (q % a)
forall (a :: k) (b :: j). q a b -> a ~> (q % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (p (p % a) a -> q (p % a) a
p :~> q
n (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p @a (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p @a a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id))))
  conjToId :: forall k. Ob0 FUNK k => Conjoint PROFK I ~> I
conjToId = (RepCostar Id :~> Id) -> Prof (PK (RepCostar Id)) (PK Id)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> Id a b)
-> (RepCostar Id a b -> a ~> b) -> RepCostar Id a b -> Id a b
forall b c a. (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
. RepCostar Id a b -> a ~> b
RepCostar Id a b -> (Id % a) ~> b
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
RepCostar p a b -> (p % a) ~> b
unRepCostar)
  conjFromId :: forall k. Ob0 FUNK k => I ~> Conjoint PROFK I
conjFromId = (Id :~> RepCostar Id) -> Prof (PK Id) (PK (RepCostar Id))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(Id a ~> b
f) -> ((Id % a) ~> b) -> RepCostar Id a b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar a ~> b
(Id % a) ~> b
f ((Ob a, Ob b) => RepCostar Id a b) -> (a ~> b) -> RepCostar Id a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  conjToCompose :: forall {k1} {j} {k2} (f :: FUNK j k2) (g :: FUNK k1 j).
Obj f
-> Obj g
-> Conjoint PROFK (O f g)
   ~> O (Conjoint PROFK g) (Conjoint PROFK f)
conjToCompose (Sub Prof{}) (Sub (Prof @g p :~> q
_)) = (RepCostar (q :.: q) :~> (RepCostar q :.: RepCostar q))
-> Prof
     (PK (RepCostar (q :.: q))) (PK (RepCostar q :.: RepCostar q))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(RepCostar @b ((q :.: q) % a) ~> b
h) -> ((q % a) ~> (q % a)) -> RepCostar q a (q % a)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (q % a) ~> (q % a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id RepCostar q a (q % a)
-> RepCostar q (q % a) b -> (:.:) (RepCostar q) (RepCostar 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 % (q % a)) ~> b) -> RepCostar q (q % a) b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((q :.: q) % a) ~> b
(q % (q % a)) ~> b
h ((Ob (q % a), Ob (q % a)) => (:.:) (RepCostar q) (RepCostar q) a b)
-> ((q % a) ~> (q % a)) -> (:.:) (RepCostar q) (RepCostar q) a b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k1 +-> j) (a :: k1) (b :: k1).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @g (forall (a :: k1). (CategoryOf k1, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)
  conjFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2).
Obj f
-> Obj g
-> O (Conjoint PROFK g) (Conjoint PROFK f)
   ~> Conjoint PROFK (O f g)
conjFromCompose (Sub (Prof @f p :~> q
_)) (Sub Prof{}) = ((RepCostar q :.: RepCostar q) :~> RepCostar (q :.: q))
-> Prof
     (PK (RepCostar q :.: RepCostar q)) (PK (RepCostar (q :.: q)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(RepCostar (q % a) ~> b
f :.: RepCostar (q % b) ~> b
g) -> (((q :.: q) % a) ~> b) -> RepCostar (q :.: q) a b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((q % b) ~> b
g ((q % b) ~> b) -> ((q % (q % a)) ~> (q % b)) -> (q % (q % a)) ~> b
forall (b :: k) (c :: k) (a :: 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
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j2 +-> k) (a :: j2) (b :: j2).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f (q % a) ~> b
f)

instance (Promonad p) => Monad (PK p :: PROFK k k) where
  eta :: I ~> PK p
eta = (Id :~> p) -> Prof (PK Id) (PK p)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((a ~> b) -> p a b
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr ((a ~> b) -> p a b) -> (Id a b -> a ~> b) -> Id a b -> p a b
forall b c a. (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
. Id a b -> a ~> b
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId)
  mu :: O (PK p) (PK p) ~> PK p
mu = ((p :.: p) :~> p) -> Prof (PK (p :.: p)) (PK p)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(p a b
p :.: p b b
q) -> p b b
q p b b -> p a b -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p a b
p

instance (Procomonad p) => Comonad (PK p :: PROFK k k) where
  epsilon :: PK p ~> I
epsilon = (p :~> Id) -> Prof (PK p) (PK Id)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> Id a b) -> (p a b -> a ~> b) -> p a b -> Id a b
forall b c a. (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
. p a b -> a ~> b
p :~> (~>)
forall {i} (p :: PRO i i). Procomonad p => p :~> (~>)
extract)
  delta :: PK p ~> O (PK p) (PK p)
delta = (p :~> (p :.: p)) -> Prof (PK p) (PK (p :.: p))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof p a b -> (:.:) p p a b
p :~> (p :.: p)
forall {i} (p :: PRO i i). Procomonad p => p :~> (p :.: p)
duplicate

instance
  (Category (cj :: CAT j), Category (ck :: CAT k), Profunctor p)
  => Bimodule (PK ck) (PK cj) (PK p :: PROFK j k)
  where
  leftAction :: O (PK ck) (PK p) ~> PK p
leftAction = ((ck :.: p) :~> p) -> Prof (PK (ck :.: p)) (PK p)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(ck a b
f :.: p b b
p) -> (a ~> b) -> p b b -> p a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ck a b
a ~> b
f p b b
p
  rightAction :: O (PK p) (PK cj) ~> PK p
rightAction = ((p :.: cj) :~> p) -> Prof (PK (p :.: cj)) (PK p)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(p a b
p :.: cj b b
f) -> (b ~> b) -> p a b -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap cj b b
b ~> b
f p a b
p

instance (A.Adjunction l r) => Adjunction (PK l :: PROFK c d) (PK r) where
  unit :: I ~> O (PK r) (PK l)
unit = (Id :~> (r :.: l)) -> Prof (PK Id) (PK (r :.: l))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(Id a ~> b
f) -> (a ~> b) -> (:.:) r l b b -> (:.:) r l a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
f (:.:) r l b b
forall (a :: c). Ob a => (:.:) r l a a
forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
A.unit ((Ob a, Ob b) => (:.:) r l a b) -> (a ~> b) -> (:.:) r l a b
forall (a :: c) (b :: c) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  counit :: O (PK l) (PK r) ~> I
counit = ((l :.: r) :~> Id) -> Prof (PK (l :.: r)) (PK Id)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> Id a b)
-> ((:.:) l r a b -> a ~> b) -> (:.:) l r a b -> Id a b
forall b c a. (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
. (:.:) l r a b -> a ~> b
(l :.: r) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
A.counit)

instance (Profunctor f, Profunctor j) => RightKanExtension (PK j :: PROFK c d) (PK f :: PROFK c e) where
  type Ran (PK j) (PK f) = PK (R.Ran (Op.OP j) f)
  ran :: O (Ran (PK j) (PK f)) (PK j) ~> PK f
ran = ((Ran ('OP j) f :.: j) :~> f)
-> Prof (PK (Ran ('OP j) f :.: j)) (PK f)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(Ran ('OP j) f a b
r :.: j b b
j) -> j b b -> Ran ('OP j) f a b -> f a b
forall {j1} {i} {k} (j2 :: PRO j1 i) (b :: j1) (x :: i)
       (p :: i +-> k) (a :: k).
Profunctor j2 =>
j2 b x -> Ran ('OP j2) p a b -> p a x
R.runRan j b b
j Ran ('OP j) f a b
r
  ranUniv :: forall (g :: PROFK d e).
Ob g =>
(O g (PK j) ~> PK f) -> g ~> Ran (PK j) (PK f)
ranUniv (Prof p :~> q
n) = (UN PK g :~> Ran ('OP j) f)
-> Prof (PK (UN PK g)) (PK (Ran ('OP j) f))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \UN PK g a b
g -> UN PK g a b
g UN PK g a b
-> ((Ob a, Ob b) => Ran ('OP j) f a b) -> Ran ('OP j) f a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: c). Ob x => j b x -> f a x) -> Ran ('OP j) f a b
forall {k} {j} {i} (a :: k) (b :: j) (j2 :: i +-> j)
       (p :: i +-> k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 b x -> p a x) -> Ran ('OP j2) p a b
R.Ran \j b x
j -> p a x -> q a x
p :~> q
n (UN PK g a b
g UN PK g a b -> j b x -> (:.:) (UN PK g) j a x
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 x
j)

instance (Profunctor f, Profunctor j) => RightKanLift (PK j :: PROFK d c) (PK f :: PROFK e c) where
  type Rift (PK j) (PK f) = PK (R.Rift (Op.OP j) f)
  rift :: O (PK j) (Rift (PK j) (PK f)) ~> PK f
rift = ((j :.: Rift ('OP j) f) :~> f)
-> Prof (PK (j :.: Rift ('OP j) f)) (PK f)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \(j a b
j :.: Rift ('OP j) f b b
r) -> j a b -> Rift ('OP j) f b b -> f a b
forall {i} {k} {j1} (j2 :: PRO i k) (x :: i) (a :: k)
       (p :: j1 +-> i) (b :: j1).
Profunctor j2 =>
j2 x a -> Rift ('OP j2) p a b -> p x b
R.runRift j a b
j Rift ('OP j) f b b
r
  riftUniv :: forall (g :: PROFK e d).
Ob g =>
(O (PK j) g ~> PK f) -> g ~> Rift (PK j) (PK f)
riftUniv (Prof p :~> q
n) = (UN PK g :~> Rift ('OP j) f)
-> Prof (PK (UN PK g)) (PK (Rift ('OP j) f))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof \UN PK g a b
g -> UN PK g a b
g UN PK g a b
-> ((Ob a, Ob b) => Rift ('OP j) f a b) -> Rift ('OP j) f a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: c). Ob x => j x a -> f x b) -> Rift ('OP j) f a b
forall {k} {j} {i} (a :: k) (b :: j) (j2 :: k +-> i)
       (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 x a -> p x b) -> Rift ('OP j2) p a b
R.Rift \j x a
j -> p x b -> q x b
p :~> q
n (j x a
j j x a -> UN PK g a b -> (:.:) j (UN PK g) x 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 PK g a b
g)

instance (L.HasLimits j k, Ob j) => HasLimits FUNK (PK j) k where
  type Limit (PK j) d = FUN (L.Limit j (UNFUN d))
  limitObj :: forall (d :: FUNK i k). Ob d => Obj (Limit (PK j) d)
limitObj = (PK (Limit j (UN PK (UN SUB d)))
 ~> PK (Limit j (UN PK (UN SUB d))))
-> Sub
     (SUB (PK (Limit j (UN PK (UN SUB d)))))
     (SUB (PK (Limit j (UN PK (UN SUB d)))))
forall {k} ob (kk :: CAT k) (i :: k) (j :: k) (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((Limit j (UN PK (UN SUB d)) :~> Limit j (UN PK (UN SUB d)))
-> Prof
     (PK (Limit j (UN PK (UN SUB d)))) (PK (Limit j (UN PK (UN SUB d))))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof Limit j (UN PK (UN SUB d)) a b -> Limit j (UN PK (UN SUB d)) a b
Limit j (UN PK (UN SUB d)) :~> Limit j (UN PK (UN SUB d))
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  limit :: forall (d :: FUNK i k).
Ob d =>
O (Companion PROFK (Limit (PK j) d)) (PK j) ~> Companion PROFK d
limit = ((Limit j (UN PK (UN SUB d)) :.: j) :~> UN PK (UN SUB d))
-> Prof
     (PK (Limit j (UN PK (UN SUB d)) :.: j)) (PK (UN PK (UN SUB d)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (:.:) (Limit j (UN PK (UN SUB d))) j a b -> UN PK (UN SUB d) a b
(Limit j (UN PK (UN SUB d)) :.: j) :~> UN PK (UN SUB 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
L.limit
  limitUniv :: forall (d :: FUNK i k) (p :: FUNK a k).
(Ob d, Ob p) =>
(O (Companion PROFK p) (PK j) ~> Companion PROFK d)
-> p ~> Limit (PK j) d
limitUniv (Prof p :~> q
n) = (PK (UN PK (UN SUB p)) ~> PK (Limit j (UN PK (UN SUB d))))
-> Sub
     (SUB (PK (UN PK (UN SUB p))))
     (SUB (PK (Limit j (UN PK (UN SUB d)))))
forall {k} ob (kk :: CAT k) (i :: k) (j :: k) (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((UN PK (UN SUB p) :~> Limit j (UN PK (UN SUB d)))
-> Prof (PK (UN PK (UN SUB p))) (PK (Limit j (UN PK (UN SUB d))))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((UN PK (UN SUB p) :.: j) :~> UN PK (UN SUB d))
-> UN PK (UN SUB p) :~> Limit j (UN PK (UN SUB d))
forall {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Representable p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (d :: i +-> k) (p :: a +-> k).
(Representable d, Representable p) =>
((p :.: j) :~> d) -> p :~> Limit j d
L.limitUniv p a b -> q a b
(:.:) (UN PK (UN SUB p)) j a b -> UN PK (UN SUB d) a b
p :~> q
(UN PK (UN SUB p) :.: j) :~> UN PK (UN SUB d)
n))

instance (L.HasColimits j k, Ob j) => HasColimits FUNK (PK j) k where
  type Colimit (PK j) d = FUN (L.Colimit j (UNFUN d))
  colimit :: forall (d :: FUNK i k).
Ob d =>
O (Companion PROFK d) (PK j) ~> Companion PROFK (Colimit (PK j) d)
colimit = ((UN PK (UN SUB d) :.: j) :~> Colimit j (UN PK (UN SUB d)))
-> Prof
     (PK (UN PK (UN SUB d) :.: j)) (PK (Colimit j (UN PK (UN SUB d))))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (:.:) (UN PK (UN SUB d)) j a b -> Colimit j (UN PK (UN SUB d)) a b
(UN PK (UN SUB d) :.: j) :~> Colimit j (UN PK (UN SUB d))
forall {i} {a} (j :: a +-> i) k (d :: i +-> k).
(HasColimits j k, Representable d) =>
(d :.: j) :~> Colimit j d
forall (d :: i +-> k). Representable d => (d :.: j) :~> Colimit j d
L.colimit
  colimitUniv :: forall (d :: FUNK i k) (p :: FUNK a k).
(Ob d, Ob p) =>
(O (Companion PROFK d) (PK j) ~> Companion PROFK p)
-> Colimit (PK j) d ~> p
colimitUniv (Prof p :~> q
n) = (PK (Colimit j (UN PK (UN SUB d))) ~> PK (UN PK (UN SUB p)))
-> Sub
     (SUB (PK (Colimit j (UN PK (UN SUB d)))))
     (SUB (PK (UN PK (UN SUB p))))
forall {k} ob (kk :: CAT k) (i :: k) (j :: k) (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((Colimit j (UN PK (UN SUB d)) :~> UN PK (UN SUB p))
-> Prof (PK (Colimit j (UN PK (UN SUB d)))) (PK (UN PK (UN SUB p)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((UN PK (UN SUB d) :.: j) :~> UN PK (UN SUB p))
-> Colimit j (UN PK (UN SUB d)) :~> UN PK (UN SUB p)
forall {i} {a} (j :: a +-> i) k (d :: i +-> k) (p :: a +-> k).
(HasColimits j k, Representable d, Representable p) =>
((d :.: j) :~> p) -> Colimit j d :~> p
forall (d :: i +-> k) (p :: a +-> k).
(Representable d, Representable p) =>
((d :.: j) :~> p) -> Colimit j d :~> p
L.colimitUniv p a b -> q a b
(:.:) (UN PK (UN SUB d)) j a b -> UN PK (UN SUB p) a b
p :~> q
(UN PK (UN SUB d) :.: j) :~> UN PK (UN SUB p)
n))

class
  ( forall (s :: COK sk h i) (t :: tk j k). (Ob s, Ob t) => Profunctor (p s t)
  , forall (s :: COK sk h i). (Ob s) => Functor (p s)
  , Functor p
  ) =>
  IsFunctorial h i j k (p :: COK sk h i -> tk j k -> kk h j +-> kk i k)
instance
  ( forall (s :: COK sk h i) (t :: tk j k). (Ob s, Ob t) => Profunctor (p s t)
  , forall (s :: COK sk h i). (Ob s) => Functor (p s)
  , Functor p
  )
  => IsFunctorial h i j k (p :: COK sk h i -> tk j k -> kk h j +-> kk i k)

type LaxProfunctor :: forall {s} {t}. CAT s -> CAT t -> (t +-> s) -> Constraint
class
  ( Bicategory sk
  , Bicategory tk
  , forall h i j k. (Ob0 sk h, Ob0 sk i, Ob0 tk j, Ob0 tk k) => IsFunctorial h i j k (P sk tk kk)
  , forall j k. (Ob0 sk j, Ob0 tk k) => CategoryOf (kk j k)
  ) =>
  LaxProfunctor (sk :: CAT s) (tk :: CAT t) (kk :: t +-> s)
  where
  data P sk tk kk :: forall {h} {i} {j} {k}. COK sk h i -> tk j k -> kk h j +-> kk i k
  laxId :: (Ob0 sk k, Ob0 tk j) => (Id :: CAT (kk k j)) :~> P sk tk kk (CO (I :: sk k k)) (I :: tk j j)
  laxComp :: P sk tk kk s0 t0 :.: P sk tk kk s1 t1 :~> P sk tk kk (s0 `O` s1) (t0 `O` t1)

dimapLax :: (LaxProfunctor sk tk kk) => (s' ~> s) -> (t ~> t') -> P sk tk kk (CO s) t :~> P sk tk kk (CO s') t'
dimapLax :: forall {s} {t} {h :: s} {i :: s} {j :: t} {k :: t} (sk :: CAT s)
       (tk :: CAT t) (kk :: t +-> s) (s' :: sk h i) (s :: sk h i)
       (t :: tk j k) (t' :: tk j k).
LaxProfunctor sk tk kk =>
(s' ~> s)
-> (t ~> t') -> P sk tk kk ('CO s) t :~> P sk tk kk ('CO s') t'
dimapLax s' ~> s
f t ~> t'
g = (Prof (P sk tk kk ('CO s) t') (P sk tk kk ('CO s') t')
-> P sk tk kk ('CO s) t' :~> P sk tk kk ('CO s') t'
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf (Nat (P sk tk kk ('CO s)) (P sk tk kk ('CO s'))
-> P sk tk kk ('CO s) .~> P sk tk kk ('CO s')
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat (('CO s ~> 'CO s') -> P sk tk kk ('CO s) ~> P sk tk kk ('CO s')
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: COK sk h i) (b :: COK sk h i).
(a ~> b) -> P sk tk kk a ~> P sk tk kk b
map ((s' ~> s) -> Co ('CO s) ('CO s')
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co s' ~> s
f))) (P sk tk kk ('CO s) t' a b -> P sk tk kk ('CO s') t' a b)
-> (P sk tk kk ('CO s) t a b -> P sk tk kk ('CO s) t' a b)
-> P sk tk kk ('CO s) t a b
-> P sk tk kk ('CO s') t' a b
forall b c a. (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
. Prof (P sk tk kk ('CO s) t) (P sk tk kk ('CO s) t')
-> P sk tk kk ('CO s) t :~> P sk tk kk ('CO s) t'
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf ((t ~> t') -> P sk tk kk ('CO s) t ~> P sk tk kk ('CO s) t'
forall (a :: tk j k) (b :: tk j k).
(a ~> b) -> P sk tk kk ('CO s) a ~> P sk tk kk ('CO s) b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map t ~> t'
g)) ((Ob0 sk h, Ob0 sk i, Ob s', Ob s) =>
 P sk tk kk ('CO s) t a b -> P sk tk kk ('CO s') t' a b)
-> (s' ~> s)
-> P sk tk kk ('CO s) t a b
-> P sk tk kk ('CO s') t' a b
forall (i :: s) (j :: s) (ps :: sk i j) (qs :: sk i j) r.
((Ob0 sk i, Ob0 sk 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
\\\ s' ~> s
f ((Ob0 tk j, Ob0 tk k, Ob t, Ob t') =>
 P sk tk kk ('CO s) t a b -> P sk tk kk ('CO s') t' a b)
-> (t ~> t')
-> P sk tk kk ('CO s) t a b
-> P sk tk kk ('CO s') t' a b
forall (i :: t) (j :: t) (ps :: tk i j) (qs :: tk i j) r.
((Ob0 tk i, Ob0 tk 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
\\\ t ~> t'
g

instance (Monad m, Comonad c, LaxProfunctor sk tk kk, Ob c, Ob m) => Monad (PK (P sk tk kk (CO c) m)) where
  eta :: I ~> PK (P sk tk kk ('CO c) m)
eta = (Id :~> P sk tk kk ('CO c) m)
-> Prof (PK Id) (PK (P sk tk kk ('CO c) m))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((c ~> I)
-> (I ~> m) -> P sk tk kk ('CO I) I :~> P sk tk kk ('CO c) m
forall {s} {t} {h :: s} {i :: s} {j :: t} {k :: t} (sk :: CAT s)
       (tk :: CAT t) (kk :: t +-> s) (s' :: sk h i) (s :: sk h i)
       (t :: tk j k) (t' :: tk j k).
LaxProfunctor sk tk kk =>
(s' ~> s)
-> (t ~> t') -> P sk tk kk ('CO s) t :~> P sk tk kk ('CO s') t'
dimapLax c ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon I ~> m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta (P sk tk kk ('CO I) I a b -> P sk tk kk ('CO c) m a b)
-> (Id a b -> P sk tk kk ('CO I) I a b)
-> Id a b
-> P sk tk kk ('CO c) m a b
forall b c a. (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
. Id a b -> P sk tk kk ('CO I) I a b
forall (k :: s) (j :: k).
(Ob0 sk k, Ob0 tk j) =>
Id :~> P sk tk kk ('CO I) I
Id :~> P sk tk kk ('CO I) I
forall {s} {t} (sk :: CAT s) (tk :: CAT t) (kk :: t +-> s) (k :: s)
       (j :: t).
(LaxProfunctor sk tk kk, Ob0 sk k, Ob0 tk j) =>
Id :~> P sk tk kk ('CO I) I
laxId)
  mu :: O (PK (P sk tk kk ('CO c) m)) (PK (P sk tk kk ('CO c) m))
~> PK (P sk tk kk ('CO c) m)
mu = ((P sk tk kk ('CO c) m :.: P sk tk kk ('CO c) m)
 :~> P sk tk kk ('CO c) m)
-> Prof
     (PK (P sk tk kk ('CO c) m :.: P sk tk kk ('CO c) m))
     (PK (P sk tk kk ('CO c) m))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof ((c ~> O c c)
-> (O m m ~> m)
-> P sk tk kk ('CO (O c c)) (O m m) :~> P sk tk kk ('CO c) m
forall {s} {t} {h :: s} {i :: s} {j :: t} {k :: t} (sk :: CAT s)
       (tk :: CAT t) (kk :: t +-> s) (s' :: sk h i) (s :: sk h i)
       (t :: tk j k) (t' :: tk j k).
LaxProfunctor sk tk kk =>
(s' ~> s)
-> (t ~> t') -> P sk tk kk ('CO s) t :~> P sk tk kk ('CO s') t'
dimapLax c ~> O c c
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta O m m ~> m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu (P sk tk kk ('CO (O c c)) (O m m) a b -> P sk tk kk ('CO c) m a b)
-> ((:.:) (P sk tk kk ('CO c) m) (P sk tk kk ('CO c) m) a b
    -> P sk tk kk ('CO (O c c)) (O m m) a b)
-> (:.:) (P sk tk kk ('CO c) m) (P sk tk kk ('CO c) m) a b
-> P sk tk kk ('CO c) m a b
forall b c a. (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
. (:.:) (P sk tk kk ('CO c) m) (P sk tk kk ('CO c) m) a b
-> P sk tk kk (O ('CO c) ('CO c)) (O m m) a b
(:.:) (P sk tk kk ('CO c) m) (P sk tk kk ('CO c) m) a b
-> P sk tk kk ('CO (O c c)) (O m m) a b
forall {j :: s} {i :: s} {j :: k} {k :: k} {h :: s} {j :: k}
       (s0 :: COK sk j i) (t0 :: tk j k) (s1 :: COK sk h j)
       (t1 :: tk j j).
(P sk tk kk s0 t0 :.: P sk tk kk s1 t1)
:~> P sk tk kk (O s0 s1) (O t0 t1)
forall {s} {t} (sk :: CAT s) (tk :: CAT t) (kk :: t +-> s) {j :: s}
       {i :: s} {j :: t} {k :: t} {h :: s} {j :: t} (s0 :: COK sk j i)
       (t0 :: tk j k) (s1 :: COK sk h j) (t1 :: tk j j).
LaxProfunctor sk tk kk =>
(P sk tk kk s0 t0 :.: P sk tk kk s1 t1)
:~> P sk tk kk (O s0 s1) (O t0 t1)
laxComp)

type ProfSq p q f g = Sq '(PK p, FUN g) '(PK q, FUN f)

-- | The collage is a cotabulator with this 2-cell.
--
-- > J-InjR-Col
-- > |   v   |
-- > p---@   |
-- > |   v   |
-- > K-InjL-Col
isCotabulator :: (Profunctor p) => ProfSq p Collage (InjR p) (InjL p)
isCotabulator :: forall {j} {k} (p :: PRO j k).
Profunctor p =>
ProfSq p Collage (InjR p) (InjL p)
isCotabulator = (O (Companion PROFK (FUN (InjL p))) (PK p)
 ~> O (PK Collage) (Companion PROFK (FUN (InjR p))))
-> Sq '(PK p, FUN (InjL p)) '(PK Collage, FUN (InjR p))
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq ((O (Companion PROFK (FUN (InjL p))) (PK p)
  ~> O (PK Collage) (Companion PROFK (FUN (InjR p))))
 -> Sq '(PK p, FUN (InjL p)) '(PK Collage, FUN (InjR p)))
-> (O (Companion PROFK (FUN (InjL p))) (PK p)
    ~> O (PK Collage) (Companion PROFK (FUN (InjR p))))
-> Sq '(PK p, FUN (InjL p)) '(PK Collage, FUN (InjR p))
forall a b. (a -> b) -> a -> b
$ ((InjL p :.: p) :~> (Collage :.: InjR p))
-> Prof (PK (InjL p :.: p)) (PK (Collage :.: InjR p))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((InjL p :.: p) :~> (Collage :.: InjR p))
 -> Prof (PK (InjL p :.: p)) (PK (Collage :.: InjR p)))
-> ((InjL p :.: p) :~> (Collage :.: InjR p))
-> Prof (PK (InjL p :.: p)) (PK (Collage :.: InjR p))
forall a b. (a -> b) -> a -> b
$ \(InjL a ~> (InjL p % b)
f :.: p b b
p) -> a ~> (InjL p % b)
Collage a (L b)
f Collage a (L b) -> InjR p (L b) b -> (:.:) Collage (InjR 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
:.: (L b ~> (InjR p % b)) -> InjR p (L b) b
forall {k} {j} (b :: k) (p :: k +-> j) (a :: COLLAGE p).
Ob b =>
(a ~> (InjR p % b)) -> InjR p a b
InjR (p b b -> Collage (L b) (R b)
forall {k} {j} (p :: k +-> j) (a1 :: j) (b1 :: k).
p a1 b1 -> Collage (L a1) (R b1)
L2R p b b
p) ((Ob b, Ob b) => (:.:) Collage (InjR p) a b)
-> p b b -> (:.:) Collage (InjR p) a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p

-- | Any 2-cell of shape p(a, b) -> e(f a, g b) factors through the cotabulator 2-cell.
--
-- > J--f--H    J-Inj1-CG--X--H
-- > |  v  |    |   v   |  v  |
-- > p--@  | == p---@   |  |  |
-- > |  v  |    |   v   |  v  |
-- > K--g--H    K-Inj2-CG--X--H
type CotabulatorFactorizer :: Type -> forall (p :: j +-> k) -> (j +-> h) -> (k +-> h) -> COLLAGE p +-> h
data CotabulatorFactorizer s p f g a b where
  CF :: (Ob b) => a ~> CotabulatorFactorizer s p f g % b -> CotabulatorFactorizer s p f g a b

instance
  (Profunctor p, Representable f, Representable g, Reifies s (ProfSq p Id f g))
  => Profunctor (CotabulatorFactorizer s p f g)
  where
  dimap :: forall (c :: j) (a :: j) (b :: COLLAGE p) (d :: COLLAGE p).
(c ~> a)
-> (b ~> d)
-> CotabulatorFactorizer s p f g a b
-> CotabulatorFactorizer s p f g c d
dimap = (c ~> a)
-> (b ~> d)
-> CotabulatorFactorizer s p f g a b
-> CotabulatorFactorizer s p f g c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> CotabulatorFactorizer s p f g a b -> r
\\ CF a ~> (CotabulatorFactorizer s p f g % b)
x = r
(Ob a, Ob (CotabulatorFactorizer s p f g % b)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (CotabulatorFactorizer s p f g % b)) => r)
-> (a ~> (CotabulatorFactorizer s p f g % b)) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (CotabulatorFactorizer s p f g % b)
x
instance
  (Profunctor p, Representable f, Representable g, Reifies s (ProfSq p Id f g))
  => Representable (CotabulatorFactorizer s p f g)
  where
  type CotabulatorFactorizer s p f g % R a = f % a
  type CotabulatorFactorizer s p f g % L a = g % a
  index :: forall (a :: k) (b :: COLLAGE p).
CotabulatorFactorizer s p f g a b
-> a ~> (CotabulatorFactorizer s p f g % b)
index (CF a ~> (CotabulatorFactorizer s p f g % b)
f) = a ~> (CotabulatorFactorizer s p f g % b)
f
  tabulate :: forall (b :: COLLAGE p) (a :: k).
Ob b =>
(a ~> (CotabulatorFactorizer s p f g % b))
-> CotabulatorFactorizer s p f g a b
tabulate a ~> (CotabulatorFactorizer s p f g % b)
f = (a ~> (CotabulatorFactorizer s p f g % b))
-> CotabulatorFactorizer s p f g a b
forall {j} {k} {k} (p :: j +-> k) (b :: COLLAGE p) (a :: k) s
       (f :: j +-> k) (g :: k +-> k).
Ob b =>
(a ~> (CotabulatorFactorizer s p f g % b))
-> CotabulatorFactorizer s p f g a b
CF a ~> (CotabulatorFactorizer s p f g % b)
f ((Ob a, Ob (CotabulatorFactorizer s p f g % b)) =>
 CotabulatorFactorizer s p f g a b)
-> (a ~> (CotabulatorFactorizer s p f g % b))
-> CotabulatorFactorizer s p f g a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (CotabulatorFactorizer s p f g % b)
f
  repMap :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(a ~> b)
-> (CotabulatorFactorizer s p f g % a)
   ~> (CotabulatorFactorizer s p f g % b)
repMap = \case
    InL a1 ~> b1
f -> forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @g a1 ~> b1
f
    InR a1 ~> b1
f -> forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f a1 ~> b1
f
    L2R p a1 b1
p ->
      p a1 b1
p p a1 b1
-> ((Ob a1, Ob b1) => (g % a1) ~> (f % b1)) -> (g % a1) ~> (f % b1)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case [s] -> ProfSq p Id f g
forall {k} (s :: k) a (proxy :: k -> Type).
Reifies s a =>
proxy s -> a
forall (proxy :: Type -> Type). proxy s -> ProfSq p Id f g
reflect ([] @s) of Sq (Prof p :~> q
n) -> case p (g % a1) b1 -> q (g % a1) b1
p :~> q
n (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 @g (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @g (p a1 b1 -> a1 ~> a1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p a1 b1
p)) g (g % a1) a1 -> p a1 b1 -> (:.:) g p (g % a1) b1
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 a1 b1
p) of Id (g % a1) ~> b
g :.: f b b1
f -> f b b1 -> b ~> (f % b1)
forall (a :: k) (b :: j). 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 b b1
f (b ~> (f % b1)) -> ((g % a1) ~> b) -> (g % a1) ~> (f % b1)
forall (b :: k) (c :: k) (a :: 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
. (g % a1) ~> b
g

cotabulatorFactorize
  :: forall p f g r
   . (Profunctor p, Representable f, Representable g)
  => ProfSq p Id f g
  -> ( forall s
        . (Reifies s (ProfSq p Id f g))
       => ProfSq Id Id (CotabulatorFactorizer s p f g) (CotabulatorFactorizer s p f g)
       -> r
     )
  -> r
cotabulatorFactorize :: forall {h} {j} {k} (p :: PRO h j) (f :: j +-> k) (g :: h +-> k) r.
(Profunctor p, Representable f, Representable g) =>
ProfSq p Id f g
-> (forall s.
    Reifies s (ProfSq p Id f g) =>
    ProfSq
      Id
      Id
      (CotabulatorFactorizer s p f g)
      (CotabulatorFactorizer s p f g)
    -> r)
-> r
cotabulatorFactorize ProfSq p Id f g
sq forall s.
Reifies s (ProfSq p Id f g) =>
ProfSq
  Id
  Id
  (CotabulatorFactorizer s p f g)
  (CotabulatorFactorizer s p f g)
-> r
f = ProfSq p Id f g
-> (forall s. Reifies s (ProfSq p Id f g) => Proxy s -> r) -> r
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ProfSq p Id f g
sq ((forall s. Reifies s (ProfSq p Id f g) => Proxy s -> r) -> r)
-> (forall s. Reifies s (ProfSq p Id f g) => Proxy s -> r) -> r
forall a b. (a -> b) -> a -> b
$ \(Proxy @s) -> ProfSq
  Id
  Id
  (CotabulatorFactorizer s p f g)
  (CotabulatorFactorizer s p f g)
-> r
forall s.
Reifies s (ProfSq p Id f g) =>
ProfSq
  Id
  Id
  (CotabulatorFactorizer s p f g)
  (CotabulatorFactorizer s p f g)
-> r
f ((FUN (CotabulatorFactorizer s p f g)
 ~> FUN (CotabulatorFactorizer s p f g))
-> Sq
     '(I, FUN (CotabulatorFactorizer s p f g))
     '(I, FUN (CotabulatorFactorizer s p f g))
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(I, f) '(I, g)
vArr ((FUN (CotabulatorFactorizer s p f g)
  ~> FUN (CotabulatorFactorizer s p f g))
 -> Sq
      '(I, FUN (CotabulatorFactorizer s p f g))
      '(I, FUN (CotabulatorFactorizer s p f g)))
-> (FUN (CotabulatorFactorizer s p f g)
    ~> FUN (CotabulatorFactorizer s p f g))
-> Sq
     '(I, FUN (CotabulatorFactorizer s p f g))
     '(I, FUN (CotabulatorFactorizer s p f g))
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: SUBCAT ProfRep PROFK (COLLAGE p) k).
(CategoryOf (SUBCAT ProfRep PROFK (COLLAGE p) k), Ob a) =>
Obj a
obj @(FUN (CotabulatorFactorizer s p f g)))