{-# LANGUAGE DerivingStrategies #-}

module Proarrow.Profunctor.Ran where

import Prelude (type (~))

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Limit (HasLimits (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, rmap, (//), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Costar (Costar (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Profunctor.Star (Star (..))

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

type j |> p = Ran (OP j) p

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

runRan :: (Profunctor j) => j b x -> Ran (OP j) p a b -> p a x
runRan :: forall {i} {j} {k} (j :: i +-> j) (b :: j) (x :: i) (p :: i +-> k)
       (a :: k).
Profunctor j =>
j b x -> Ran ('OP j) p a b -> p a x
runRan j b x
j (Ran forall (x :: i). j b x -> p a x
k) = j b x -> p a x
forall (x :: i). j b x -> p a x
k j b x
j b x
j ((Ob b, Ob x) => p a x) -> j b x -> p a x
forall (a :: j) (b :: i) 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 b x
j

runRanProf :: (Profunctor j, Profunctor p) => Ran (OP j) p :.: j ~> p
runRanProf :: forall {i} {j} {k} (j :: i +-> j) (p :: i +-> k).
(Profunctor j, Profunctor p) =>
(Ran ('OP j) p :.: j) ~> p
runRanProf = ((Ran ('OP j) p :.: j) :~> p) -> Prof (Ran ('OP j) p :.: j) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Ran ('OP j) p a b
r :.: j b b
j) -> j b b -> Ran ('OP j) p a b -> p a b
forall {i} {j} {k} (j :: i +-> j) (b :: j) (x :: i) (p :: i +-> k)
       (a :: k).
Profunctor j =>
j b x -> Ran ('OP j) p a b -> p a x
runRan j b b
j Ran ('OP j) p a b
r

flipRan :: (Functor j, Profunctor p) => Costar j |> p ~> p :.: Star j
flipRan :: forall {i} {k2} {k} (j :: i -> k2) (p :: k2 +-> k).
(Functor j, Profunctor p) =>
(Costar j |> p) ~> (p :.: Star j)
flipRan = ((Costar j |> p) :~> (p :.: Star j))
-> Prof (Costar j |> p) (p :.: Star j)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Ran forall (x :: k2). j b x -> p a x
k) -> j b (j b) -> p a (j b)
forall (x :: k2). j b x -> p a x
k ((j b ~> j b) -> Costar j b (j b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar j b ~> j b
forall (a :: k2). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) p a (j b) -> Star j (j b) b -> (:.:) p (Star j) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (j b ~> j b) -> Star j (j b) b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star j b ~> j b
forall (a :: k2). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

flipRanInv :: (Functor j, Profunctor p) => p :.: Star j ~> Costar j |> p
flipRanInv :: forall {j} {i} {k} (j :: j -> i) (p :: i +-> k).
(Functor j, Profunctor p) =>
(p :.: Star j) ~> (Costar j |> p)
flipRanInv = ((p :.: Star j) :~> (Costar j |> p))
-> Prof (p :.: Star j) (Costar j |> p)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(p a b
p :.: Star b ~> j b
f) -> p a b
p p a b
-> ((Ob a, Ob b) => (|>) (Costar j) p a b) -> (|>) (Costar j) 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 :: i). Costar j b x -> p a x) -> (|>) (Costar j) p a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: i +-> j) (p :: i +-> k).
(Ob a, Ob b) =>
(forall (x :: i). j b x -> p a x) -> Ran ('OP j) p a b
Ran \(Costar j b ~> x
g) -> (b ~> x) -> p a b -> p a x
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (j b ~> x
g (j b ~> x) -> (b ~> j b) -> b ~> x
forall (b :: i) (c :: i) (a :: i). (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
. b ~> j b
f) p a b
p

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

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

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

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

instance (HasLimits j k, Representable d) => Representable (Ran (OP j) (d :: i +-> k)) where
  type Ran (OP j) d % a = Limit j d % a
  index :: forall (a :: k) (b :: j).
Ran ('OP j) d a b -> a ~> (Ran ('OP j) d % b)
index = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @(Limit j d) (Limit j d a b -> a ~> (Limit j d % b))
-> (Ran ('OP j) d a b -> Limit j d a b)
-> Ran ('OP j) d a b
-> a ~> (Limit j d % 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 {a} {i} (j :: i +-> a) k (d :: i +-> k) (p :: a +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
forall (j :: i +-> j) k (d :: i +-> k) (p :: j +-> k).
(HasLimits j k, Representable d, Profunctor p) =>
((p :.: j) :~> d) -> p :~> Limit j d
limitUniv @j @k @d (\(Ran forall (x :: i). j b x -> d a x
k' :.: j b b
j) -> j b b -> d a b
forall (x :: i). j b x -> d a x
k' j b b
j b b
j)
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (Ran ('OP j) d % b)) -> Ran ('OP j) d a b
tabulate a ~> (Ran ('OP j) d % b)
f = (forall (x :: i). j b x -> d a x) -> Ran ('OP j) d a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: i +-> j) (p :: i +-> k).
(Ob a, Ob b) =>
(forall (x :: i). j b x -> p a x) -> Ran ('OP j) p a b
Ran (\j b x
j -> (:.:) (Limit j d) j a x -> d a x
(Limit j d :.: j) :~> d
forall {a} {i} (j :: i +-> a) k (d :: i +-> k).
(HasLimits j k, Representable d) =>
(Limit j d :.: j) :~> d
forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d
limit ((a ~> (Limit j d % b)) -> Limit j d a b
forall (b :: j) (a :: k).
Ob b =>
(a ~> (Limit j d % b)) -> Limit j d a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a ~> (Limit j d % b)
a ~> (Ran ('OP j) d % b)
f Limit j d a b -> j b x -> (:.:) (Limit j d) 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)) ((Ob a, Ob (Limit j d % b)) => Ran ('OP j) d a b)
-> (a ~> (Limit j d % b)) -> Ran ('OP j) d a b
forall (a :: k) (b :: k) 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 ~> (Limit j d % b)
a ~> (Ran ('OP j) d % b)
f
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (Ran ('OP j) d % a) ~> (Ran ('OP j) d % b)
repMap = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Limit j d)

type PWRan j p a = (j |> p) % a

-- a ~> PWRan j p b = forall x. (b ~> j x) -> a ~> p x
-- a ~> PWRan j p b = forall x. a ~> (p x ^ (b ~> j x))
-- PWRan j p b = forall x. p x ^ (b ~> j x)
class (Representable p, Representable j, Representable (j |> p)) => PointwiseRightKanExtension j p
instance (Representable p, Representable j, Representable (j |> p)) => PointwiseRightKanExtension j p

type PWLift j p a = (j |> p) %% a

-- PWLift j p a ~> b = forall x. (j b ~> x) -> p a ~> x
-- PWLift j p a ~> b = p a ~> j b
class (Corepresentable j, Corepresentable p, Corepresentable (j |> p)) => PointwiseLeftKanLift j p
instance (Corepresentable j, Corepresentable p, Corepresentable (j |> p)) => PointwiseLeftKanLift j p

instance (Profunctor j) => Corepresentable (Star (Ran (OP j))) where
  type Star (Ran (OP j)) %% p = p :.: j
  coindex :: forall (a :: k -> j -> Type) (b :: i +-> k).
Star (Ran ('OP j)) a b -> (Star (Ran ('OP j)) %% a) ~> b
coindex (Star (Prof a :~> Ran ('OP j) b
f)) = ((a :.: j) :~> b) -> Prof (a :.: 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 :.: j b b
j) -> j b b -> Ran ('OP j) b a b -> b a b
forall {i} {j} {k} (j :: i +-> j) (b :: j) (x :: i) (p :: i +-> k)
       (a :: k).
Profunctor j =>
j b x -> Ran ('OP j) p a b -> p a x
runRan j b b
j (a a b -> Ran ('OP j) b a b
a :~> Ran ('OP j) b
f a a b
p)
  cotabulate :: forall (a :: k -> j -> Type) (b :: i +-> k).
Ob a =>
((Star (Ran ('OP j)) %% a) ~> b) -> Star (Ran ('OP j)) a b
cotabulate (Prof (a :.: j) :~> b
f) = (a ~> Ran ('OP j) b) -> Star (Ran ('OP j)) a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Ran ('OP j) b) -> Prof a (Ran ('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) => Ran ('OP j) b a b) -> Ran ('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 b x -> b a x) -> Ran ('OP j) b a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: i +-> j) (p :: i +-> k).
(Ob a, Ob b) =>
(forall (x :: i). j b x -> p a x) -> Ran ('OP j) p a b
Ran \j b x
q -> (:.:) a j a x -> b a x
(a :.: j) :~> b
f (a a b
p a a b -> j b x -> (:.:) a 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
q))
  corepMap :: forall (a :: k -> j -> Type) (b :: k -> j -> Type).
(a ~> b) -> (Star (Ran ('OP j)) %% a) ~> (Star (Ran ('OP j)) %% b)
corepMap (Prof a :~> b
f) = ((a :.: j) :~> (b :.: j)) -> Prof (a :.: j) (b :.: j)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(a a b
p :.: j b b
j) -> a a b -> b a b
a :~> b
f a a b
p b a b -> j b b -> (:.:) b j a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: j b b
j

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

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

ranHom :: (Profunctor p) => p ~> (~>) |> p
ranHom :: forall {i} {k} (p :: i +-> k). Profunctor p => p ~> ((~>) |> p)
ranHom = (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 :: i). (b ~> x) -> p a x) -> (|>) (~>) p a b
forall {k} {j} {i} (a :: k) (b :: j) (j :: i +-> j) (p :: i +-> k).
(Ob a, Ob b) =>
(forall (x :: i). j b x -> p a x) -> Ran ('OP j) p a b
Ran \b ~> x
j -> (b ~> x) -> p a b -> p a x
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> x
j p a b
p

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