{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Instance.Rift where

import Prelude (type (~))

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Colimit (HasColimits (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, rmap, (//), type (+->))
import Proarrow.Functor (Functor (..), FunctorForRep)
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..), corepUniv, withObCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Profunctor.Representable (Rep (..), RepCostar, Representable (..), repUniv, withObRep)
import Proarrow.Promonad (Procomonad (..), RelativeComonad (..))

-- Note: Ran and Rift are swapped compared to the profunctors package.

type p <| j = Rift (OP j) p

type Rift :: OPPOSITE (k +-> i) -> j +-> i -> j +-> k
data Rift j p a b where
  Rift :: (Ob a, Ob b) => {forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
Rift ('OP j) p a b -> forall (x :: i). j x a -> p x b
unRift :: forall x. j x a -> p x b} -> Rift (OP j) p a b

runRift :: (Profunctor j) => j x a -> Rift (OP j) p a b -> p x b
runRift :: forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift j x a
j (Rift forall (x :: i). j x a -> p x b
k) = j x a -> p x b
forall (x :: i). j x a -> p x b
k j x a
j x a
j ((Ob x, Ob a) => p x b) -> j x a -> p x b
forall (a :: i) (b :: k) r. ((Ob a, Ob b) => r) -> j a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ j x a
j

runRiftProf :: (Profunctor j, Profunctor p) => j :.: (p <| j) ~> p
runRiftProf :: forall {k} {i} {i} (j :: k +-> i) (p :: i +-> i).
(Profunctor j, Profunctor p) =>
(j :.: (p <| j)) ~> p
runRiftProf = ((j :.: (p <| j)) :~> p) -> Prof (j :.: (p <| j)) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(j a b
j :.: (<|) p j b b
r) -> j a b -> (<|) p j b b -> p a b
forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift j a b
j (<|) p j b b
r

riftUniv :: (Profunctor j, Profunctor g) => (j :.: g) ~> p -> g ~> p <| j
riftUniv :: forall {k} {i} {j} (j :: k +-> i) (g :: j +-> k)
       (p :: i -> j -> Type).
(Profunctor j, Profunctor g) =>
((j :.: g) ~> p) -> g ~> (p <| j)
riftUniv (Prof (j :.: g) :~> p
n) = (g :~> (p <| j)) -> Prof g (p <| j)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \g a b
g -> g a b
g g a b -> ((Ob a, Ob b) => (<|) p j a b) -> (<|) p j 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 :: i). j x a -> p x b) -> (<|) p j a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \j x a
j -> (:.:) j g x b -> p x b
(j :.: g) :~> p
n (j x a
j j x a -> g a b -> (:.:) j g x b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: g a b
g)

flipRift :: (FunctorForRep j, Profunctor p) => p <| Rep j ~> Corep j :.: p
flipRift :: forall {k} {j} {i} (j :: k +-> j) (p :: i +-> j).
(FunctorForRep j, Profunctor p) =>
(p <| Rep j) ~> (Corep j :.: p)
flipRift = ((p <| Rep j) :~> (Corep j :.: p))
-> Prof (p <| Rep j) (Corep j :.: p)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: j). j x a -> p x b
k) -> Corep j a (j @ a)
Corep j a (Corep j %% a)
forall (a :: k). Ob a => Corep j a (Corep j %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv Corep j a (j @ a) -> p (j @ a) b -> (:.:) (Corep j) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: j (j @ a) a -> p (j @ a) b
forall (x :: j). j x a -> p x b
k j (j @ a) a
j (j % a) a
forall (a :: k). Ob a => j (j % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv

flipRiftInv :: (FunctorForRep j, Profunctor p) => Corep j :.: p ~> p <| Rep j
flipRiftInv :: forall {k} {k} {j} (j :: k +-> k) (p :: j +-> k).
(FunctorForRep j, Profunctor p) =>
(Corep j :.: p) ~> (p <| Rep j)
flipRiftInv = ((Corep j :.: p) :~> (p <| Rep j))
-> Prof (Corep j :.: p) (p <| Rep j)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Corep j a b
g :.: p b b
p) -> Corep j a b
g Corep j a b
-> ((Ob a, Ob b) => (<|) p (Rep j) a b) -> (<|) p (Rep j) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// p b b
p p b b -> ((Ob b, Ob b) => (<|) p (Rep j) a b) -> (<|) p (Rep j) 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 :: k). Rep j x a -> p x b) -> (<|) p (Rep j) a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \Rep j x a
f -> (x ~> b) -> p b b -> p x b
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (Corep j a b -> (Corep j %% a) ~> b
forall (a :: k) (b :: k). Corep j a b -> (Corep j %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex Corep j a b
g ((j @ a) ~> b) -> (x ~> (j @ a)) -> x ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Rep j x a -> x ~> (Rep j % a)
forall (a :: k) (b :: k). Rep j a b -> a ~> (Rep j % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index Rep j x a
f) p b b
p

instance (Profunctor p, Profunctor j) => Profunctor (Rift (OP j) p) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Rift ('OP j) p a b -> Rift ('OP j) p c d
dimap c ~> a
l b ~> d
r (Rift forall (x :: i). j x a -> p x b
k) = b ~> d
r (b ~> d)
-> ((Ob b, Ob d) => Rift ('OP j) p c d) -> Rift ('OP j) p c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// c ~> a
l (c ~> a)
-> ((Ob c, Ob a) => Rift ('OP j) p c d) -> Rift ('OP j) p c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: i). j x c -> p x d) -> Rift ('OP j) p c d
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift ((b ~> d) -> p x b -> p x d
forall (b :: j) (d :: j) (a :: i). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r (p x b -> p x d) -> (j x c -> p x b) -> j x c -> p x d
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
. j x a -> p x b
j x a -> p x b
forall (x :: i). j x a -> p x b
k (j x a -> p x b) -> (j x c -> j x a) -> j x c -> p x 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
. (c ~> a) -> j x c -> j x a
forall (b :: k) (d :: k) (a :: i). (b ~> d) -> j a b -> j a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap c ~> a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Rift ('OP j) p a b -> r
\\ Rift{} = r
(Ob a, Ob b) => r
r

instance (Profunctor j) => Functor (Rift (OP j)) where
  map :: forall (a :: j +-> i) (b :: j +-> i).
(a ~> b) -> Rift ('OP j) a ~> Rift ('OP j) b
map (Prof a :~> b
n) = (Rift ('OP j) a :~> Rift ('OP j) b)
-> Prof (Rift ('OP j) a) (Rift ('OP j) b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: i). j x a -> a x b
k) -> (forall (x :: i). j x a -> b x b) -> Rift ('OP j) b a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift (a x b -> b x b
a :~> b
n (a x b -> b x b) -> (j x a -> a x b) -> j x a -> b x 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
. j x a -> a x b
j x a -> a x b
forall (x :: i). j x a -> a x b
k)

instance Functor Rift where
  map :: forall (a :: OPPOSITE (k +-> i)) (b :: OPPOSITE (k +-> i)).
(a ~> b) -> Rift a ~> Rift b
map (Op (Prof b1 :~> a1
n)) = (Rift ('OP a1) .~> Rift ('OP b1))
-> Nat (Rift ('OP a1)) (Rift ('OP b1))
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Rift ('OP a1) a :~> Rift ('OP b1) a)
-> Prof (Rift ('OP a1) a) (Rift ('OP b1) a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: i). j x a -> a x b
k) -> (forall (x :: i). b1 x a -> a x b) -> Rift ('OP b1) a a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift (a1 x a -> a x b
j x a -> a x b
forall (x :: i). j x a -> a x b
k (a1 x a -> a x b) -> (b1 x a -> a1 x a) -> b1 x a -> a x 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
. b1 x a -> a1 x a
b1 :~> a1
n))

-- | The right Kan lift is the right adjoint of the postcomposition functor.
instance (Profunctor j) => Corepresentable (Star (Rift (OP j))) where
  type Star (Rift (OP j)) %% p = j :.: p
  coindex :: forall (a :: k -> j -> Type) (b :: j +-> i).
Star (Rift ('OP j)) a b -> (Star (Rift ('OP j)) %% a) ~> b
coindex (Star (Prof a :~> Rift ('OP j) b
f)) = ((j :.: a) :~> b) -> Prof (j :.: a) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(j a b
j :.: a b b
p) -> j a b -> Rift ('OP j) b b b -> b a b
forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift j a b
j (a b b -> Rift ('OP j) b b b
a :~> Rift ('OP j) b
f a b b
p)
  cotabulate :: forall (a :: k -> j -> Type) (b :: j +-> i).
Ob a =>
((Star (Rift ('OP j)) %% a) ~> b) -> Star (Rift ('OP j)) a b
cotabulate (Prof (j :.: a) :~> b
f) = (a ~> Rift ('OP j) b) -> Star (Rift ('OP j)) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Rift ('OP j) b) -> Prof a (Rift ('OP j) b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> a a b
p a a b -> ((Ob a, Ob b) => Rift ('OP j) b a b) -> Rift ('OP j) b 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 :: i). j x a -> b x b) -> Rift ('OP j) b a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \j x a
q -> (:.:) j a x b -> b x b
(j :.: a) :~> b
f (j x a
q j x a -> a a b -> (:.:) j a x b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: a a b
p))
  corepMap :: forall (a :: k -> j -> Type) (b :: k -> j -> Type).
(a ~> b)
-> (Star (Rift ('OP j)) %% a) ~> (Star (Rift ('OP j)) %% b)
corepMap = (a ~> b)
-> (Star (Rift ('OP j)) %% a) ~> (Star (Rift ('OP j)) %% b)
(a ~> b) -> (j :.: a) ~> (j :.: b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k -> j -> Type) (b :: k -> j -> Type).
(a ~> b) -> (j :.: a) ~> (j :.: b)
map

instance (p ~ j, Profunctor p) => Promonad (Rift (OP j) p) where
  id :: forall (a :: k). Ob a => Rift ('OP j) p a a
id = (forall (x :: i). j x a -> p x a) -> Rift ('OP j) p a a
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift j x a -> p x a
j x a -> j x a
forall (x :: i). j x a -> p x a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Rift forall (x :: i). j x b -> p x c
l . :: forall (b :: k) (c :: k) (a :: k).
Rift ('OP j) p b c -> Rift ('OP j) p a b -> Rift ('OP j) p a c
. Rift forall (x :: i). j x a -> p x b
r = (forall (x :: i). j x a -> p x c) -> Rift ('OP j) p a c
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift (j x b -> j x c
j x b -> p x c
forall (x :: i). j x b -> p x c
l (j x b -> j x c) -> (j x a -> j x b) -> j x a -> j x c
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
. j x a -> j x b
j x a -> p x b
forall (x :: i). j x a -> p x b
r)

instance (HasColimits j k, Corepresentable d) => Corepresentable (Rift (OP j) (d :: k +-> i)) where
  type Rift (OP j) d %% a = Colimit j d %% a
  coindex :: forall (a :: k) (b :: k).
Rift ('OP j) d a b -> (Rift ('OP j) d %% a) ~> b
coindex = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @(Colimit j d) (Colimit j d a b -> (Colimit j d %% a) ~> b)
-> (Rift ('OP j) d a b -> Colimit j d a b)
-> Rift ('OP j) d a b
-> (Colimit j d %% a) ~> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {i} {a} (j :: a +-> i) k (d :: k +-> i) (p :: k +-> a).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
forall (j :: k +-> i) k (d :: k +-> i) (p :: k +-> k).
(HasColimits j k, Corepresentable d, Profunctor p) =>
((j :.: p) :~> d) -> p :~> Colimit j d
colimitUniv @j @k @d (\(j a b
j :.: Rift forall (x :: i). j x b -> d x b
k') -> j a b -> d a b
forall (x :: i). j x b -> d x b
k' j a b
j a b
j)
  corepUniv :: forall (a :: k). Ob a => Rift ('OP j) d a (Rift ('OP j) d %% a)
corepUniv @a = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @(Colimit j d) @a ((forall (x :: i). j x a -> d x (Colimit j d %% a))
-> Rift ('OP j) d a (Colimit j d %% a)
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \j x a
j -> (:.:) j (Colimit j d) x (Colimit j d %% a)
-> d x (Colimit j d %% a)
(j :.: Colimit j d) :~> d
forall {i} {a} (j :: a +-> i) k (d :: k +-> i).
(HasColimits j k, Corepresentable d) =>
(j :.: Colimit j d) :~> d
forall (d :: k +-> i).
Corepresentable d =>
(j :.: Colimit j d) :~> d
colimit (j x a
j j x a
-> Colimit j d a (Colimit j d %% a)
-> (:.:) j (Colimit j d) x (Colimit j d %% a)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Colimit j d a (Colimit j d %% a)
forall (a :: k). Ob a => Colimit j d a (Colimit j d %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv))

type PWLan j p a = (p <| j) %% a

-- PWLan j p a ~> b = forall x. j x ~> a -> p x ~> b
-- PWLan j p a ~> b = forall x. ((j x ~> a) .* p x) ~> b
-- PWLan j p a = exists x. ((j x ~> a) .* p x)
class (Corepresentable j, Corepresentable p, Corepresentable (p <| j)) => PointwiseLeftKanExtension j p
instance (Corepresentable j, Corepresentable p, Corepresentable (p <| j)) => PointwiseLeftKanExtension j p

type PWRift j p a = (p <| j) % a

-- a ~> PWRift j p b = forall x. x ~> j a -> x ~> p b
-- a ~> PWRift j p b = j a ~> p b
class (Representable p, Representable j, Representable (p <| j)) => PointwiseRightKanLift j p
instance (Representable p, Representable j, Representable (p <| j)) => PointwiseRightKanLift j p

instance (Representable g, Representable f, Profunctor j, f ~ j <| g) => RelativeComonad j (RepCostar f :.: RepCostar g) where
  relExtract :: forall (a :: k). Ob a => j ((RepCostar f :.: RepCostar g) %% a) a
relExtract @a = let f :: f (f % a) a
f = forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @f @a in g (g % ((j <| g) % a)) ((j <| g) % a)
-> Rift ('OP g) j ((j <| g) % a) a -> j (g % ((j <| g) % a)) a
forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> i) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @g) f (f % a) a
Rift ('OP g) j ((j <| g) % a) a
f ((Ob ((j <| g) % a), Ob a) => j (g % ((j <| g) % a)) a)
-> f ((j <| g) % a) a -> j (g % ((j <| g) % a)) a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> f 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
\\ f (f % a) a
f ((j <| g) % a) a
f
  relExtend :: forall (a :: k) (b :: k).
Ob a =>
j ((RepCostar f :.: RepCostar g) %% a) b
-> ((RepCostar f :.: RepCostar g) %% a)
   ~> ((RepCostar f :.: RepCostar g) %% b)
relExtend @a @b j ((RepCostar f :.: RepCostar g) %% a) b
j = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @f @a (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> i) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @g @(f % a) @(f % b) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @f @_ @b ((forall (x :: i). g x ((j <| g) % a) -> j x b)
-> Rift ('OP g) j ((j <| g) % a) b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift (\g x ((j <| g) % a)
g -> (x ~> (g % ((j <| g) % a))) -> j (g % ((j <| g) % a)) b -> j x b
forall (c :: i) (a :: i) (b :: k). (c ~> a) -> j a b -> j c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (g x ((j <| g) % a) -> x ~> (g % ((j <| g) % a))
forall (a :: i) (b :: k). g a b -> a ~> (g % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index g x ((j <| g) % a)
g) j ((RepCostar f :.: RepCostar g) %% a) b
j (g % ((j <| g) % a)) b
j)))) ((Ob (g % ((j <| g) % a)), Ob b) =>
 (g % ((j <| g) % a)) ~> (g % ((j <| g) % b)))
-> j (g % ((j <| g) % a)) b
-> (g % ((j <| g) % a)) ~> (g % ((j <| g) % b))
forall (a :: i) (b :: k) r. ((Ob a, Ob b) => r) -> j a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ j ((RepCostar f :.: RepCostar g) %% a) b
j (g % ((j <| g) % a)) b
j

riftCompose :: (Profunctor i, Profunctor j, Profunctor p) => (p <| j) <| i ~> p <| (j :.: i)
riftCompose :: forall {k} {j} {k} {j} (i :: k +-> j) (j :: j +-> k)
       (p :: j +-> k).
(Profunctor i, Profunctor j, Profunctor p) =>
((p <| j) <| i) ~> (p <| (j :.: i))
riftCompose = (((p <| j) <| i) :~> (p <| (j :.: i)))
-> Prof ((p <| j) <| i) (p <| (j :.: i))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(<|) (p <| j) i a b
k -> (<|) (p <| j) i a b
k (<|) (p <| j) i a b
-> ((Ob a, Ob b) => (<|) p (j :.: i) a b) -> (<|) p (j :.: i) 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 :: k). (:.:) j i x a -> p x b) -> (<|) p (j :.: i) a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \(j x b
j :.: i b a
i) -> j x b -> Rift ('OP j) p b b -> p x b
forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift j x b
j (i b a -> (<|) (p <| j) i a b -> Rift ('OP j) p b b
forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift i b a
i (<|) (p <| j) i a b
k)

riftComposeInv :: (Profunctor i, Profunctor j, Profunctor p) => p <| (j :.: i) ~> (p <| j) <| i
riftComposeInv :: forall {k} {i} {i} {j} (i :: k +-> i) (j :: i +-> i)
       (p :: j +-> i).
(Profunctor i, Profunctor j, Profunctor p) =>
(p <| (j :.: i)) ~> ((p <| j) <| i)
riftComposeInv = ((p <| (j :.: i)) :~> ((p <| j) <| i))
-> Prof (p <| (j :.: i)) ((p <| j) <| i)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(<|) p (j :.: i) a b
k -> (<|) p (j :.: i) a b
k (<|) p (j :.: i) a b
-> ((Ob a, Ob b) => (<|) (p <| j) i a b) -> (<|) (p <| j) i 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 :: i). i x a -> (<|) p j x b) -> (<|) (p <| j) i a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \i x a
i -> i x a
i i x a -> ((Ob x, Ob a) => (<|) p j x b) -> (<|) p j x 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 :: i). j x x -> p x b) -> (<|) p j x b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \j x x
j -> (:.:) j i x a -> (<|) p (j :.: i) a b -> p x b
forall {k} {i} {j} (j :: k +-> i) (x :: i) (a :: k) (p :: j +-> i)
       (b :: j).
Profunctor j =>
j x a -> Rift ('OP j) p a b -> p x b
runRift (j x x
j j x x -> i x a -> (:.:) j i x a
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: i x a
i) (<|) p (j :.: i) a b
k

riftHom :: (Profunctor p) => p ~> p <| (~>)
riftHom :: forall {j} {k} (p :: j +-> k). Profunctor p => p ~> (p <| (~>))
riftHom = (p :~> (p <| (~>))) -> Prof p (p <| (~>))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \p a b
p -> p a b
p p a b -> ((Ob a, Ob b) => (<|) p (~>) a b) -> (<|) p (~>) 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 :: k). (x ~> a) -> p x b) -> (<|) p (~>) a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift ((x ~> a) -> p a b -> p x b
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
`lmap` p a b
p)

riftHomInv :: (Profunctor p) => p <| (~>) ~> p
riftHomInv :: forall {j} {k} (p :: j +-> k). Profunctor p => (p <| (~>)) ~> p
riftHomInv = ((p <| (~>)) :~> p) -> Prof (p <| (~>)) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Rift forall (x :: k). j x a -> p x b
k) -> j a a -> p a b
forall (x :: k). j x a -> p x b
k j a a
forall (a :: k). Ob a => j a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

compAsRift :: (Promonad p, Ob a) => ((p <| p) <| p) a a
compAsRift :: forall {k} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
(<|) (p <| p) p a a
compAsRift = (forall (x :: k). p x a -> (<|) p p x a)
-> Rift ('OP p) (p <| p) a a
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift \p x a
p -> p x a
p p x a -> ((Ob x, Ob a) => (<|) p p x a) -> (<|) p p x a
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: k). p x x -> p x a) -> (<|) p p x a
forall {k} {j} {i} (a :: k) (b :: j) (j :: k +-> i) (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j x a -> p x b) -> Rift ('OP j) p a b
Rift (p x a
p p x a -> p x x -> p x a
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
.)

instance (Procomonad j) => Promonad (Star (Rift (OP j))) where
  id :: forall (a :: k -> j -> Type). Ob a => Star (Rift ('OP j)) a a
id = (a ~> Rift ('OP j) a) -> Star (Rift ('OP j)) a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (Nat (Rift ('OP (~>))) (Rift ('OP j))
-> Rift ('OP (~>)) .~> Rift ('OP j)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat (('OP (~>) ~> 'OP j) -> Rift ('OP (~>)) ~> Rift ('OP j)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: OPPOSITE (k +-> k)) (b :: OPPOSITE (k +-> k)).
(a ~> b) -> Rift a ~> Rift b
map (Prof j (~>) -> Op Prof ('OP (~>)) ('OP j)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((j :~> (~>)) -> Prof j (~>)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof j a b -> a ~> b
j :~> (~>)
forall k (p :: k +-> k). Procomonad p => p :~> (~>)
proextract))) Prof (Rift ('OP (~>)) a) (Rift ('OP j) a)
-> Prof a (Rift ('OP (~>)) a) -> Prof a (Rift ('OP j) a)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k -> j -> Type) (c :: k -> j -> Type)
       (a :: k -> j -> Type).
Prof b c -> Prof a b -> Prof a c
. a ~> Rift ('OP (~>)) a
Prof a (Rift ('OP (~>)) a)
forall {j} {k} (p :: j +-> k). Profunctor p => p ~> (p <| (~>))
riftHom)
  Star b ~> Rift ('OP j) c
l . :: forall (b :: k -> j -> Type) (c :: k -> j -> Type)
       (a :: k -> j -> Type).
Star (Rift ('OP j)) b c
-> Star (Rift ('OP j)) a b -> Star (Rift ('OP j)) a c
. Star a ~> Rift ('OP j) b
r = (a ~> Rift ('OP j) c) -> Star (Rift ('OP j)) a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (Nat (Rift ('OP (j :.: j))) (Rift ('OP j))
-> Rift ('OP (j :.: j)) .~> Rift ('OP j)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat (('OP (j :.: j) ~> 'OP j) -> Rift ('OP (j :.: j)) ~> Rift ('OP j)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: OPPOSITE (k +-> k)) (b :: OPPOSITE (k +-> k)).
(a ~> b) -> Rift a ~> Rift b
map (Prof j (j :.: j) -> Op Prof ('OP (j :.: j)) ('OP j)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((j :~> (j :.: j)) -> Prof j (j :.: j)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof j a b -> (:.:) j j a b
j :~> (j :.: j)
forall k (p :: k +-> k). Procomonad p => p :~> (p :.: p)
produplicate))) Prof (Rift ('OP (j :.: j)) c) (Rift ('OP j) c)
-> Prof a (Rift ('OP (j :.: j)) c) -> Prof a (Rift ('OP j) c)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k -> j -> Type) (c :: k -> j -> Type)
       (a :: k -> j -> Type).
Prof b c -> Prof a b -> Prof a c
. (Rift ('OP j) c <| j) ~> Rift ('OP (j :.: j)) c
Prof (Rift ('OP j) c <| j) (Rift ('OP (j :.: j)) c)
forall {k} {j} {k} {j} (i :: k +-> j) (j :: j +-> k)
       (p :: j +-> k).
(Profunctor i, Profunctor j, Profunctor p) =>
((p <| j) <| i) ~> (p <| (j :.: i))
riftCompose Prof (Rift ('OP j) c <| j) (Rift ('OP (j :.: j)) c)
-> Prof a (Rift ('OP j) c <| j) -> Prof a (Rift ('OP (j :.: j)) c)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k -> j -> Type) (c :: k -> j -> Type)
       (a :: k -> j -> Type).
Prof b c -> Prof a b -> Prof a c
. (b ~> Rift ('OP j) c) -> Rift ('OP j) b ~> (Rift ('OP j) c <| j)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k -> j -> Type) (b :: k -> j -> Type).
(a ~> b) -> Rift ('OP j) a ~> Rift ('OP j) b
map b ~> Rift ('OP j) c
l Prof (Rift ('OP j) b) (Rift ('OP j) c <| j)
-> Prof a (Rift ('OP j) b) -> Prof a (Rift ('OP j) c <| j)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k -> j -> Type) (c :: k -> j -> Type)
       (a :: k -> j -> Type).
Prof b c -> Prof a b -> Prof a c
. a ~> Rift ('OP j) b
Prof a (Rift ('OP j) b)
r)