module Proarrow.Category.Bicategory.Prof where

import Data.Kind (Constraint)

import Proarrow.Adjunction qualified as A
import Proarrow.Category.Bicategory
  ( Adj (..)
  , Adjunction_ (..)
  , Bicategory (..)
  , Bimodule (..)
  , Comonad (..)
  , Monad (..)
  )
import Proarrow.Category.Bicategory.Co (COK (..), Co (..))
import Proarrow.Category.Bicategory.Kan (RightKanExtension (..), RightKanLift (..))
import Proarrow.Category.Bicategory.Limit qualified as Bi
import Proarrow.Category.Bicategory.Sub (IsOb, IsOb0, SUBCAT (..), Sub (..), WithObO2 (..))
import Proarrow.Category.Colimit qualified as L
import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), Tight, TightAdjoint)
import Proarrow.Category.Equipment.Limit (HasColimits (..), HasLimits (..))
import Proarrow.Category.Instance.Cat qualified as C
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof qualified as Prof
import Proarrow.Category.Instance.Unit qualified as U
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
  , rmap
  , src
  , tgt
  , (//)
  , (:~>)
  , type (+->)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Ran qualified as R
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), RepCostar (..), Representable (..))
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 :: 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 (ZonkAny 0) (ZonkAny 1)), Ob (q (ZonkAny 0) (ZonkAny 1))) =>
r
(Ob a, Ob b) => r
r ((Ob (p (ZonkAny 0) (ZonkAny 1)),
  Ob (q (ZonkAny 0) (ZonkAny 1))) =>
 r)
-> (p (ZonkAny 0) (ZonkAny 1) -> q (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
\\ p (ZonkAny 0) (ZonkAny 1) -> q (ZonkAny 0) (ZonkAny 1)
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 :: 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 :: 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 Functor PK where
  map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> PK a ~> PK b
map (Prof.Prof a :~> b
f) = (a :~> b) -> Prof (PK a) (PK b)
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof a a b -> b a b
a :~> b
f

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)
  withOb2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) r.
(Ob a, Ob b, Ob0 PROFK i, Ob0 PROFK j, Ob0 PROFK k) =>
(Ob (O a b) => r) -> r
withOb2 Ob (O a b) => r
r = r
Ob (O a b) => r
r
  withOb0s :: forall {j} {k} (a :: PROFK j k) r.
Ob a =>
((Ob0 PROFK j, Ob0 PROFK k) => r) -> r
withOb0s (Ob0 PROFK j, Ob0 PROFK k) => r
r = r
(Ob0 PROFK j, Ob0 PROFK k) => r
r
  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 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 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 :: j +-> k) (c :: k) (a :: k) (b :: j).
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 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 {j} {k} (a :: k) (b :: j) (p :: j +-> k).
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 a b
p :.: Id b ~> b
h) -> (b ~> b) -> UN PK a a b -> UN PK a 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 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 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 :: k1 +-> k2).
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 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 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 instance IsOb0 ProfRep k = ()

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 (Sub (Prof n)) = Prof n
--   withObCompanion r = r
--   compToId = Prof id
--   compFromId = Prof id
--   compToCompose f g = Prof id \\ f \\ g
--   compFromCompose f g = Prof id \\ f \\ g

-- instance Equipment PROFK FUNK where
--   type Conjoint PROFK p = PK (RepCostar (UNFUN p))
--   mapConjoint (Sub (Prof @p n)) = Prof \(RepCostar @a f) -> RepCostar (f . index (n (trivialRep @p @a)))
--   withObConjoint r = r
--   conjToId = Prof (Id . unRepCostar)
--   conjFromId = Prof \(Id f) -> RepCostar f \\ f
--   conjToCompose (Sub Prof{}) (Sub (Prof @g _)) = Prof \(RepCostar @b h) -> RepCostar id :.: RepCostar h \\ repObj @g @b
--   conjFromCompose (Sub (Prof @f _)) (Sub Prof{}) = Prof \(RepCostar f :.: RepCostar g) -> RepCostar (g . repMap @f f)

type instance IsOb Tight p = Representable (UN PK p)
type instance IsOb Cotight p = Corepresentable (UN PK p)
type instance TightAdjoint p = PK (CorepStar (UN PK p))
type instance CotightAdjoint p = PK (RepCostar (UN PK p))
instance WithObO2 Tight PROFK where
  withObO2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) r.
(Ob a, Ob b, IsOb Tight a, IsOb Tight b) =>
((IsOb Tight (O a b), Ob (O a b)) => r) -> r
withObO2 (IsOb Tight (O a b), Ob (O a b)) => r
r = r
(IsOb Tight (O a b), Ob (O a b)) => r
r
instance WithObO2 Cotight PROFK where
  withObO2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) r.
(Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) =>
((IsOb Cotight (O a b), Ob (O a b)) => r) -> r
withObO2 (IsOb Cotight (O a b), Ob (O a b)) => r
r = r
(IsOb Cotight (O a b), Ob (O a b)) => r
r
instance Equipment PROFK where
  withTightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r.
IsCotight f =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint (Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r = r
(Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r
  withCotightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r.
IsTight f =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint (Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r = r
(Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r

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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: j +-> k) (c :: k) (a :: k) (b :: j).
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 :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap cj b b
b ~> b
f p a b
p

instance (A.Proadjunction l r) => Adjunction_ (PK l :: PROFK c d) (PK r) where
  adj :: Adj (PK l) (PK r)
adj =
    Adj
      { adjUnit :: I ~> O (PK r) (PK l)
adjUnit = (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 :: j +-> k) (c :: k) (a :: k) (b :: j).
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 :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
      , adjCounit :: O (PK l) (PK r) ~> I
adjCounit = ((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 :: 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 :: j +-> k) (q :: k +-> j).
Proadjunction 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 {i} {j1} {k} (j2 :: i +-> j1) (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 :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: c). 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). 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 {k} {i} {j1} (j2 :: k +-> i) (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 :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: c). 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). 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 (PK j) k where
  type Limit (PK j) (PK d) = PK (L.Limit j d)
  withObLimit :: forall (d :: PROFK i k) r.
IsTight d =>
(IsTight (Limit (PK j) d) => r) -> r
withObLimit IsTight (Limit (PK j) d) => r
r = r
IsTight (Limit (PK j) d) => r
r
  limit :: forall (d :: PROFK i k).
IsTight d =>
O (Limit (PK j) d) (PK j) ~> d
limit = ((Limit j (UN PK d) :.: j) :~> UN PK d)
-> Prof (PK (Limit j (UN PK d) :.: j)) (PK (UN PK 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 d)) j a b -> UN PK d a b
(Limit j (UN PK d) :.: j) :~> UN PK 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 :: PROFK i k) (p :: PROFK a k).
(IsTight d, Ob p) =>
(O p (PK j) ~> d) -> p ~> Limit (PK j) d
limitUniv (Prof p :~> q
n) = (UN PK p :~> Limit j (UN PK d))
-> Prof (PK (UN PK p)) (PK (Limit j (UN PK d)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((UN PK p :.: j) :~> UN PK d) -> UN PK p :~> Limit j (UN PK d)
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 (d :: i +-> k) (p :: a +-> k).
(Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
L.limitUniv p a b -> q a b
(:.:) (UN PK p) j a b -> UN PK d a b
p :~> q
(UN PK p :.: j) :~> UN PK d
n)

instance (L.HasColimits j k, Ob j) => HasColimits (PK j) k where
  type Colimit (PK j) (PK d) = PK (L.Colimit j d)
  withObColimit :: forall (d :: PROFK k i) r.
IsCotight d =>
(IsCotight (Colimit (PK j) d) => r) -> r
withObColimit IsCotight (Colimit (PK j) d) => r
r = r
IsCotight (Colimit (PK j) d) => r
r
  colimit :: forall (d :: PROFK k i).
IsCotight d =>
O (PK j) (Colimit (PK j) d) ~> d
colimit = ((j :.: Colimit j (UN PK d)) :~> UN PK d)
-> Prof (PK (j :.: Colimit j (UN PK d))) (PK (UN PK d))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (:.:) j (Colimit j (UN PK d)) a b -> UN PK d a b
(j :.: Colimit j (UN PK d)) :~> UN PK 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
L.colimit
  colimitUniv :: forall (d :: PROFK k i) (p :: PROFK k a).
(IsCotight d, Ob p) =>
(O (PK j) p ~> d) -> p ~> Colimit (PK j) d
colimitUniv (Prof p :~> q
n) = (UN PK p :~> Colimit j (UN PK d))
-> Prof (PK (UN PK p)) (PK (Colimit j (UN PK d)))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof (((j :.: UN PK p) :~> UN PK d) -> UN PK p :~> Colimit j (UN PK d)
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 (d :: k +-> i) (p :: k +-> a).
(Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
L.colimitUniv p a b -> q a b
(:.:) j (UN PK p) a b -> UN PK d a b
p :~> q
(j :.: UN PK p) :~> UN PK d
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 {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
Prof.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 :: 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 {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
Prof.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 :: tk k k), Comonad (c :: sk i i), Ob0 sk i, Ob0 tk k, 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 :: 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 :: k) (j :: t).
(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 :: 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 :: k} {i :: k} {j :: t} {k :: t} {h :: k} {j :: t}
       (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 Col.Collage (Rep (Col.InjR p)) (Rep (Col.InjL p))
-- isCotabulator = Sq (Prof \(Rep f :.: p) -> f :.: Rep (Col.L2R p) \\ 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) -> Col.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 = dimapRep
--   r \\ CF x = r \\ 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 % Col.R a = f % a
--   type CotabulatorFactorizer s p f g % Col.L a = g % a
--   index (CF f) = f
--   tabulate f = CF f \\ f
--   repMap = \case
--     Col.InL f -> repMap @g f
--     Col.InR f -> repMap @f f
--     Col.L2R p ->
--       p // case reflect ([] @s) of Sq (Prof n) -> case n (trivialRep :.: p) of Id g :.: f -> index f . 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 sq f = reify sq \(Proxy @s) -> f (vArr (obj @(FUN (CotabulatorFactorizer s p f g))))

type instance Bi.TerminalObject FUNK = ()
instance Bi.HasTerminalObject FUNK where
  type Terminate FUNK j = FUN (Rep C.Terminate)
  terminate :: forall j. Ob0 FUNK j => Obj (Terminate FUNK j)
terminate = (PK (Rep Terminate) ~> PK (Rep Terminate))
-> Sub (SUB (PK (Rep Terminate))) (SUB (PK (Rep Terminate)))
forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((Rep Terminate :~> Rep Terminate)
-> Prof (PK (Rep Terminate)) (PK (Rep Terminate))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof Rep Terminate a b -> Rep Terminate a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
Rep Terminate :~> Rep Terminate
id)
  termUniv :: forall j (f :: FUNK j (TerminalObject FUNK))
       (g :: FUNK j (TerminalObject FUNK)).
(Ob0 FUNK j, Ob f, Ob g) =>
f ~> g
termUniv @_ @_ @g = (PK (UN PK (UN SUB f)) ~> PK (UN PK (UN SUB g)))
-> Sub (SUB (PK (UN PK (UN SUB f)))) (SUB (PK (UN PK (UN SUB g))))
forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((UN PK (UN SUB f) :~> UN PK (UN SUB g))
-> Prof (PK (UN PK (UN SUB f))) (PK (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) a b
f -> (a ~> (UN PK (UN SUB g) % b)) -> UN PK (UN SUB g) a b
forall (b :: j) (a :: ()).
Ob b =>
(a ~> (UN PK (UN SUB g) % b)) -> UN PK (UN SUB g) a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a ~> (UN PK (UN SUB g) % b)
Unit '() '()
U.Unit ((Ob a, Ob b) => UN PK (UN SUB g) a b)
-> UN PK (UN SUB f) a b -> UN PK (UN SUB g) a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ()) (b :: j) r.
((Ob a, Ob b) => r) -> UN PK (UN SUB f) a b -> r
\\ UN PK (UN SUB f) a b
f ((Ob (UN PK (UN SUB g) % b), Ob (UN PK (UN SUB g) % b)) =>
 UN PK (UN SUB g) a b)
-> Unit (UN PK (UN SUB g) % b) (UN PK (UN SUB g) % b)
-> UN PK (UN SUB g) a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ()) (b :: ()) r. ((Ob a, Ob b) => r) -> Unit a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> ()) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(UNFUN g) (UN PK (UN SUB f) a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt UN PK (UN SUB f) a b
f))

type instance Bi.Product FUNK a b = (a, b)
instance Bi.HasBinaryProducts FUNK where
  type Fst FUNK a b = FUN (Rep C.FstCat)
  type Snd FUNK a b = FUN (Rep C.SndCat)
  fstObj :: forall a b. (Ob0 FUNK a, Ob0 FUNK b) => Obj (Fst FUNK a b)
fstObj = (PK (Rep FstCat) ~> PK (Rep FstCat))
-> Sub (SUB (PK (Rep FstCat))) (SUB (PK (Rep FstCat)))
forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((Rep FstCat :~> Rep FstCat)
-> Prof (PK (Rep FstCat)) (PK (Rep FstCat))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof Rep FstCat a b -> Rep FstCat a b
Rep FstCat :~> Rep FstCat
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  sndObj :: forall a b. (Ob0 FUNK a, Ob0 FUNK b) => Obj (Snd FUNK a b)
sndObj = (PK (Rep SndCat) ~> PK (Rep SndCat))
-> Sub (SUB (PK (Rep SndCat))) (SUB (PK (Rep SndCat)))
forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub ((Rep SndCat :~> Rep SndCat)
-> Prof (PK (Rep SndCat)) (PK (Rep SndCat))
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
(Ob p, Ob q) =>
(p :~> q) -> Prof (PK p) (PK q)
Prof Rep SndCat a b -> Rep SndCat a b
Rep SndCat :~> Rep SndCat
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  type f &&& g = FUN (UNFUN f C.:&&&: UNFUN g)
  prodObj :: forall j a b (f :: FUNK j a) (g :: FUNK j b).
(Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob f, Ob g) =>
Obj (f &&& g)
prodObj = (PK (UN PK (UN SUB f) :&&&: UN PK (UN SUB g))
 ~> PK (UN PK (UN SUB f) :&&&: UN PK (UN SUB g)))
-> Sub
     (SUB (PK (UN PK (UN SUB f) :&&&: UN PK (UN SUB g))))
     (SUB (PK (UN PK (UN SUB f) :&&&: UN PK (UN SUB g))))
forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub (((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
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
(UN PK (UN SUB f) :&&&: UN PK (UN SUB g))
:~> (UN PK (UN SUB f) :&&&: UN PK (UN SUB g))
id)
  prodUniv :: forall j a b (h :: FUNK j (Product FUNK a b))
       (k :: FUNK j (Product FUNK a b)).
(Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob h, Ob k) =>
(O (Fst FUNK a b) h ~> O (Fst FUNK a b) k)
-> (O (Snd FUNK a b) h ~> O (Snd FUNK a b) k) -> h ~> k
prodUniv @_ @_ @_ @_ @k (Sub (Prof p :~> q
n)) (Sub (Prof p :~> q
m)) =
    (PK (UN PK (UN SUB h)) ~> PK (UN PK (UN SUB k)))
-> Sub (SUB (PK (UN PK (UN SUB h)))) (SUB (PK (UN PK (UN SUB k))))
forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j)
       (b1 :: kk i j).
(IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub
      ( (UN PK (UN SUB h) :~> UN PK (UN SUB k))
-> Prof (PK (UN PK (UN SUB h))) (PK (UN PK (UN SUB k)))
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 h) a b
h ->
              UN PK (UN SUB h) a b
h UN PK (UN SUB h) a b
-> ((Ob a, Ob b) => UN PK (UN SUB k) a b) -> UN PK (UN SUB k) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> (a, b)) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(UNFUN k) (UN PK (UN SUB h) a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt UN PK (UN SUB h) a b
h) (:**:) (~>) (~>) (UN PK (UN SUB k) % b) (UN PK (UN SUB k) % b)
-> ((Ob (UN PK (UN SUB k) % b), Ob (UN PK (UN SUB k) % b)) =>
    UN PK (UN SUB k) a b)
-> UN PK (UN SUB k) 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 p (Fst a) b -> q (Fst a) b
p :~> q
n ((Fst a ~> (FstCat @ a)) -> Rep FstCat (Fst a) a
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep Fst a ~> (FstCat @ a)
Fst a ~> Fst a
forall (a :: a). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Rep FstCat (Fst a) a
-> UN PK (UN SUB h) a b
-> (:.:) (Rep FstCat) (UN PK (UN SUB h)) (Fst 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 (UN SUB h) a b
h) of
                Rep Fst a ~> (FstCat @ b)
f :.: (UN PK (UN SUB k) b b -> b ~> (UN PK (UN SUB k) % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (a :: (a, b)) (b :: j).
UN PK (UN SUB k) a b -> a ~> (UN PK (UN SUB k) % b)
index -> a1 ~> b1
k :**: a2 ~> b2
_) ->
                  case p (Snd a) b -> q (Snd a) b
p :~> q
m ((Snd a ~> (SndCat @ a)) -> Rep SndCat (Snd a) a
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep Snd a ~> (SndCat @ a)
Snd a ~> Snd a
forall (a :: b). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Rep SndCat (Snd a) a
-> UN PK (UN SUB h) a b
-> (:.:) (Rep SndCat) (UN PK (UN SUB h)) (Snd 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 (UN SUB h) a b
h) of
                    Rep Snd a ~> (SndCat @ b)
g :.: (UN PK (UN SUB k) b b -> b ~> (UN PK (UN SUB k) % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (a :: (a, b)) (b :: j).
UN PK (UN SUB k) a b -> a ~> (UN PK (UN SUB k) % b)
index -> a1 ~> b1
_ :**: a2 ~> b2
k') ->
                      (a ~> (UN PK (UN SUB k) % b)) -> UN PK (UN SUB k) a b
forall (b :: j) (a :: (a, b)).
Ob b =>
(a ~> (UN PK (UN SUB k) % b)) -> UN PK (UN SUB k) a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate ((a1 ~> b1
Fst b ~> b1
k (Fst b ~> b1) -> (Fst a ~> Fst b) -> Fst a ~> b1
forall (b :: a) (c :: a) (a :: 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
. Fst a ~> (FstCat @ b)
Fst a ~> Fst b
f) (Fst a ~> b1)
-> (Snd a ~> b2) -> (:**:) (~>) (~>) '(Fst a, Snd a) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2
Snd b ~> b2
k' (Snd b ~> b2) -> (Snd a ~> Snd b) -> Snd a ~> b2
forall (b :: b) (c :: b) (a :: b). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Snd a ~> (SndCat @ b)
Snd a ~> Snd b
g))
          )
      )

-- type instance TerminalObject PROFK FUNK = ()
-- instance HasTerminalObject PROFK FUNK where
--   type Terminate PROFK FUNK j = FUN (Rep C.Terminate)
--   terminate = Sub (Prof id)
--   termUniv = Sq (Prof \(Rep U.Unit :.: f) -> (Id U.Unit :.: Rep U.Unit) \\ f)

-- type instance InitialObject PROFK FUNK = VOID
-- instance HasInitialObject PROFK FUNK where
--   type Initiate PROFK FUNK j = FUN (Rep C.Initiate)
--   initiate = Sub (Prof id)
--   initUniv = Sq (Prof \case {})

-- type instance Product PROFK FUNK a b = (a, b)
-- instance HasBinaryProducts PROFK FUNK where
--   type Fst PROFK FUNK a b = FUN (Rep C.FstCat)
--   type Snd PROFK FUNK a b = FUN (Rep C.SndCat)
--   fstObj = Sub (Prof id)
--   sndObj = Sub (Prof id)
--   type ProdV PROFK FUNK (SUB (PK f)) (SUB (PK g)) = SUB (PK (f C.:&&&: g))
--   type ProdH PROFK FUNK (PK p) (PK q) = PK (p :**: q)
--   prodObj = Sub (Prof id)
--   prodUniv (Sq (Prof n)) (Sq (Prof m)) =
--     Sq
--       ( Prof
--           (\((f' C.:&&&: g') :.: p) -> case (n (f' :.: p), m (g' :.: p)) of (a :.: f, b :.: g) -> (a :**: b) :.: (f C.:&&&: g))
--       )

-- type instance Coproduct PROFK FUNK a b = COPRODUCT a b
-- instance HasBinaryCoproducts PROFK FUNK where
--   type Lft PROFK FUNK a b = FUN (Rep C.LftCat)
--   type Rgt PROFK FUNK a b = FUN (Rep C.RgtCat)
--   lftObj = Sub (Prof id)
--   rgtObj = Sub (Prof id)
--   type CoprodV PROFK FUNK (SUB (PK f)) (SUB (PK g)) = SUB (PK (f C.:|||: g))
--   type CoprodH PROFK FUNK (PK p) (PK q) = PK (p :++: q)
--   coprodObj = Sub (Prof id)
--   coprodUniv (Sq (Prof n)) (Sq (Prof m)) =
--     Sq
--       ( Prof
--           ( \(x :.: y) ->
--               case x of
--                 C.InjLP f' -> case y of InjL p -> case n (f' :.: p) of p' :.: f -> p' :.: C.InjLP f
--                 C.InjRP g' -> case y of InjR q -> case m (g' :.: q) of p' :.: g -> p' :.: C.InjRP g
--           )
--       )