{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory.Prof where

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

import Proarrow.Category.Bicategory (Bicategory(..), Monad(..), Bimodule(..), Adjunction(..))
import Proarrow.Category.Bicategory.Kan (RightKanExtension(..), RightKanLift (..))
import Proarrow.Core (PRO, CategoryOf(..), Profunctor(..), (:~>), CAT, Promonad (..), dimapDefault, lmap, rmap, UN, Is, arr, IsCategoryOf, (//))
import Proarrow.Profunctor.Representable (Representable)
import Proarrow.Profunctor.Corepresentable (Corepresentable)
import Proarrow.Category.Instance.Prof ()
import Proarrow.Profunctor.Composition ((:.:)(..))
import Proarrow.Object (src, tgt)
import Proarrow.Adjunction qualified as A
import Proarrow.Profunctor.Ran qualified as R
import Proarrow.Profunctor.Rift qualified as R
import Proarrow.Category.Opposite (OPPOSITE(..))


type data ProfCl = ProfC | ProfRepC | ProfCorepC

type family ProfConstraint (cl :: ProfCl) :: PRO j k -> Constraint
type instance ProfConstraint ProfC = Profunctor
type instance ProfConstraint ProfRepC = Representable
type instance ProfConstraint ProfCorepC = Corepresentable

type data ProfK (cl :: ProfCl) j k = PK (PRO j k)
type instance UN PK (PK p) = p
type PROFK = ProfK ProfC

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

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

class ProfConstraint cl (p :.: q) => ComposeConstraint cl i j k (p :: PRO i j) (q :: PRO j k)
instance ProfConstraint cl (p :.: q) => ComposeConstraint cl i j k (p :: PRO i j) (q :: PRO j k)

instance (forall i j k (p :: PRO i j) (q :: PRO j k). (ProfConstraint cl p, ProfConstraint cl q) => ComposeConstraint cl i j k p q) => Bicategory (ProfK cl) where
  type Ob0 (ProfK cl) k = (CategoryOf k, ProfConstraint cl ((~>) :: CAT k))
  type I = PK (~>)
  type p `O` q = PK (UN PK p :.: UN PK q)
  Prof UN PK a :~> UN PK b
m o :: forall {k1} i j (a :: ProfK cl i j) (b :: ProfK cl i j)
       (c :: ProfK cl j k1) (d :: ProfK cl j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Prof UN PK c :~> UN PK d
n = (UN PK (PK (UN PK a :.: UN PK c))
 :~> UN PK (PK (UN PK b :.: UN PK d)))
-> Prof (PK (UN PK a :.: UN PK c)) (PK (UN PK b :.: UN PK d))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK (UN PK a :.: UN PK c))
  :~> UN PK (PK (UN PK b :.: UN PK d)))
 -> Prof (PK (UN PK a :.: UN PK c)) (PK (UN PK b :.: UN PK d)))
-> (UN PK (PK (UN PK a :.: UN PK c))
    :~> UN PK (PK (UN PK b :.: UN PK d)))
-> Prof (PK (UN PK a :.: UN PK c)) (PK (UN PK b :.: UN PK d))
forall a b. (a -> b) -> a -> b
$ \(UN PK a a b
p :.: UN PK c b b
q) -> UN PK a a b -> UN PK b a b
UN PK a :~> UN PK b
m UN PK a a b
p UN PK b a b -> UN PK d b b -> (:.:) (UN PK b) (UN PK d) a b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: UN PK c b b -> UN PK d b b
UN PK c :~> UN PK d
n UN PK c b b
q
  (Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r
r \\\ :: forall i j (ps :: ProfK cl i j) (qs :: ProfK cl i j) r.
((Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Prof{} = r
(Ob0 (ProfK cl) i, Ob0 (ProfK cl) j, Ob ps, Ob qs) => r
r
  leftUnitor :: forall i j (a :: ProfK cl i j). Obj a -> O I a ~> a
leftUnitor Prof{} = (UN PK (PK ((~>) :.: UN PK a)) :~> UN PK (PK (UN PK a)))
-> Prof (PK ((~>) :.: UN PK a)) (PK (UN PK a))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK ((~>) :.: UN PK a)) :~> UN PK (PK (UN PK a)))
 -> Prof (PK ((~>) :.: UN PK a)) (PK (UN PK a)))
-> (UN PK (PK ((~>) :.: UN PK a)) :~> UN PK (PK (UN PK a)))
-> Prof (PK ((~>) :.: UN PK a)) (PK (UN PK a))
forall a b. (a -> b) -> a -> b
$ \(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 cl i j). Obj a -> a ~> O I a
leftUnitorInv Prof{} = (UN PK (PK (UN PK a)) :~> UN PK (PK ((~>) :.: UN PK a)))
-> Prof (PK (UN PK a)) (PK ((~>) :.: UN PK a))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK (UN PK a)) :~> UN PK (PK ((~>) :.: UN PK a)))
 -> Prof (PK (UN PK a)) (PK ((~>) :.: UN PK a)))
-> (UN PK (PK (UN PK a)) :~> UN PK (PK ((~>) :.: UN PK a)))
-> Prof (PK (UN PK a)) (PK ((~>) :.: UN PK a))
forall a b. (a -> b) -> a -> b
$ \UN PK (PK (UN PK a)) a b
p -> 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
UN PK (PK (UN PK a)) a b
p (a ~> a) -> UN PK a a b -> (:.:) (~>) (UN PK a) a b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: UN PK a a b
UN PK (PK (UN PK a)) a b
p
  rightUnitor :: forall i j (a :: ProfK cl i j). Obj a -> O a I ~> a
rightUnitor Prof{} = (UN PK (PK (UN PK a :.: (~>))) :~> UN PK (PK (UN PK a)))
-> Prof (PK (UN PK a :.: (~>))) (PK (UN PK a))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK (UN PK a :.: (~>))) :~> UN PK (PK (UN PK a)))
 -> Prof (PK (UN PK a :.: (~>))) (PK (UN PK a)))
-> (UN PK (PK (UN PK a :.: (~>))) :~> UN PK (PK (UN PK a)))
-> Prof (PK (UN PK a :.: (~>))) (PK (UN PK a))
forall a b. (a -> b) -> a -> b
$ \(UN PK a a b
p :.: 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 cl i j). Obj a -> a ~> O a I
rightUnitorInv Prof{} = (UN PK (PK (UN PK a)) :~> UN PK (PK (UN PK a :.: (~>))))
-> Prof (PK (UN PK a)) (PK (UN PK a :.: (~>)))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK (UN PK a)) :~> UN PK (PK (UN PK a :.: (~>))))
 -> Prof (PK (UN PK a)) (PK (UN PK a :.: (~>))))
-> (UN PK (PK (UN PK a)) :~> UN PK (PK (UN PK a :.: (~>))))
-> Prof (PK (UN PK a)) (PK (UN PK a :.: (~>)))
forall a b. (a -> b) -> a -> b
$ \UN PK (PK (UN PK a)) a b
p -> UN PK a a b
UN PK (PK (UN PK a)) a b
p UN PK a a b -> (b ~> b) -> (:.:) (UN PK a) (~>) a b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: 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
UN PK (PK (UN PK a)) a b
p
  associator :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1)
       (c :: ProfK cl j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Prof{} Prof{} Prof{} = (UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c))
 :~> UN PK (PK (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 {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK ((UN PK a :.: UN PK b) :.: UN PK c))
  :~> UN PK (PK (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 (PK ((UN PK a :.: UN PK b) :.: UN PK c))
    :~> UN PK (PK (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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: UN PK c b b
r)
  associatorInv :: forall {j1} {k1} i j2 (a :: ProfK cl i j2) (b :: ProfK cl j2 j1)
       (c :: ProfK cl j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Prof{} Prof{} Prof{} = (UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c)))
 :~> UN PK (PK ((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 {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof ((UN PK (PK (UN PK a :.: (UN PK b :.: UN PK c)))
  :~> UN PK (PK ((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 (PK (UN PK a :.: (UN PK b :.: UN PK c)))
    :~> UN PK (PK ((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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: UN PK c b b
r

instance Promonad p => Monad (PK p :: PROFK k k) where
  eta :: I ~> PK p
eta = (UN PK (PK (~>)) :~> UN PK (PK p)) -> Prof (PK (~>)) (PK p)
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof UN PK (PK (~>)) a b -> UN PK (PK p) a b
(a ~> b) -> p a b
UN PK (PK (~>)) :~> UN PK (PK p)
forall {k} (p :: PRO k k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr
  mu :: O (PK p) (PK p) ~> PK p
mu = (UN PK (PK (p :.: p)) :~> UN PK (PK p))
-> Prof (PK (p :.: p)) (PK p)
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p 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 (IsCategoryOf j cj, IsCategoryOf k ck, Profunctor p) =>
    Bimodule (PK cj) (PK ck) (PK p :: PROFK j k) where
  leftAction :: O (PK cj) (PK p) ~> PK p
leftAction = (UN PK (PK (cj :.: p)) :~> UN PK (PK p))
-> Prof (PK (cj :.: p)) (PK p)
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \(cj 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 cj a b
a ~> b
f p b b
p
  rightAction :: O (PK p) (PK ck) ~> PK p
rightAction = (UN PK (PK (p :.: ck)) :~> UN PK (PK p))
-> Prof (PK (p :.: ck)) (PK p)
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \(p a b
p :.: ck 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 ck 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 = (UN PK (PK (~>)) :~> UN PK (PK (r :.: l)))
-> Prof (PK (~>)) (PK (r :.: l))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \UN PK (PK (~>)) 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 UN PK (PK (~>)) a b
a ~> b
f (:.:) r l b b
forall (a :: d). 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 :: d) (b :: d) 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
\\ UN PK (PK (~>)) a b
a ~> b
f
  counit :: O (PK l) (PK r) ~> I
counit = (UN PK (PK (l :.: r)) :~> UN PK (PK (~>)))
-> Prof (PK (l :.: r)) (PK (~>))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof UN PK (PK (l :.: r)) a b -> UN PK (PK (~>)) a b
(:.:) l r a b -> a ~> b
UN PK (PK (l :.: r)) :~> UN PK (PK (~>))
(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 j) f)
  ran :: O (PK j) (Ran (PK j) (PK f)) ~> PK f
ran = (UN PK (PK (j :.: Ran ('OP j) f)) :~> UN PK (PK f))
-> Prof (PK (j :.: Ran ('OP j) f)) (PK f)
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \(j a b
j :.: Ran ('OP j) f b b
r) -> j a b -> Ran ('OP j) f b b -> f a b
forall {i} {j1} {k} (j2 :: PRO i j1) (x :: i) (a :: j1)
       (p :: PRO i k) (b :: k).
Profunctor j2 =>
j2 x a -> Ran ('OP j2) p a b -> p x b
R.runRan j a b
j Ran ('OP j) f b b
r
  ranUniv :: forall (g :: ProfK ProfC d e).
Ob g =>
(O (PK j) g ~> PK f) -> g ~> Ran (PK j) (PK f)
ranUniv (Prof UN PK (PK (j :.: UN PK g)) :~> UN PK (PK f)
n) = (UN PK (PK (UN PK g)) :~> UN PK (PK (Ran ('OP j) f)))
-> Prof (PK (UN PK g)) (PK (Ran ('OP j) f))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \UN PK (PK (UN PK g)) a b
g -> UN PK g a b
UN PK (PK (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 x a -> f x b) -> Ran ('OP j) f a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO i j)
       (p :: PRO i k).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 x a -> p x b) -> Ran ('OP j2) p a b
R.Ran \j x a
j -> UN PK (PK (j :.: UN PK g)) x b -> UN PK (PK f) x b
UN PK (PK (j :.: UN PK g)) :~> UN PK (PK f)
n (j x a
j j x a -> UN PK g a b -> (:.:) j (UN PK g) x b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: UN PK g a b
UN PK (PK (UN PK g)) a b
g)

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 j) f)
  rift :: O (Rift (PK j) (PK f)) (PK j) ~> PK f
rift = (UN PK (PK (Rift ('OP j) f :.: j)) :~> UN PK (PK f))
-> Prof (PK (Rift ('OP j) f :.: j)) (PK f)
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \(Rift ('OP j) f a b
r :.: j b b
j) -> j b b -> Rift ('OP j) f a b -> f a b
forall {k} {i} {j1} (j2 :: PRO k i) (b :: k) (x :: i)
       (p :: PRO j1 i) (a :: j1).
Profunctor j2 =>
j2 b x -> Rift ('OP j2) p a b -> p a x
R.runRift j b b
j Rift ('OP j) f a b
r
  riftUniv :: forall (g :: ProfK ProfC e d).
Ob g =>
(O g (PK j) ~> PK f) -> g ~> Rift (PK j) (PK f)
riftUniv (Prof UN PK (PK (UN PK g :.: j)) :~> UN PK (PK f)
n) = (UN PK (PK (UN PK g)) :~> UN PK (PK (Rift ('OP j) f)))
-> Prof (PK (UN PK g)) (PK (Rift ('OP j) f))
forall {cl :: ProfCl} {j} {k} (p :: ProfK cl j k)
       (q :: ProfK cl j k).
(Ob p, Ob q) =>
(UN PK p :~> UN PK q) -> Prof p q
Prof \UN PK (PK (UN PK g)) a b
g -> UN PK g a b
UN PK (PK (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 b x -> f a x) -> Rift ('OP j) f a b
forall {j} {k} {i} (a :: j) (b :: k) (j2 :: PRO k i)
       (p :: PRO j i).
(Ob a, Ob b) =>
(forall (x :: i). Ob x => j2 b x -> p a x) -> Rift ('OP j2) p a b
R.Rift \j b x
j -> UN PK (PK (UN PK g :.: j)) a x -> UN PK (PK f) a x
UN PK (PK (UN PK g :.: j)) :~> UN PK (PK f)
n (UN PK g a b
UN PK (PK (UN PK g)) a b
g UN PK g a b -> j b x -> (:.:) (UN PK g) j a x
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: j b x
j)