{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Representable where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Category.Enriched.ThinCategory (Discrete, Thin, ThinProfunctor (..), withEq)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (:~>), type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Object (Obj, obj, tgt, src)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), dimapCorep, trivialCorep)
import Proarrow.Category.Instance.Prof (Prof(..))

infixl 8 %

type Representable :: forall {j} {k}. j +-> k -> Constraint
class (Profunctor p) => Representable (p :: j +-> k) where
  type p % (a :: j) :: k
  index :: p a b -> a ~> p % b
  tabulate :: (Ob b) => (a ~> p % b) -> p a b
  repMap :: (a ~> b) -> p % a ~> p % b

instance Representable (->) where
  type (->) % a = a
  index :: forall a b. (a -> b) -> a ~> ((->) % b)
index a -> b
f = a ~> ((->) % b)
a -> b
f
  tabulate :: forall b a. Ob b => (a ~> ((->) % b)) -> a -> b
tabulate a ~> ((->) % b)
f = a ~> ((->) % b)
a -> b
f
  repMap :: forall a b. (a ~> b) -> ((->) % a) ~> ((->) % b)
repMap a ~> b
f = a ~> b
((->) % a) ~> ((->) % b)
f

repObj :: forall p a. (Representable p, Ob a) => Obj (p % a)
repObj :: forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

withRepOb :: forall p a r. (Representable p, Ob a) => ((Ob (p % a)) => r) -> r
withRepOb :: forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb Ob (p % a) => r
r = r
Ob (p % a) => r
(Ob (p % a), Ob (p % a)) => r
r ((Ob (p % a), Ob (p % a)) => r) -> ((p % a) ~> (p % a)) -> r
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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj @p @a

dimapRep :: forall p a b c d. (Representable p) => (c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep c ~> a
l b ~> d
r = forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p ((c ~> (p % d)) -> p c d)
-> (p a b -> c ~> (p % d)) -> p a b -> p c 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
. (c ~> a) -> ((p % b) ~> (p % d)) -> (a ~> (p % b)) -> c ~> (p % d)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p b ~> d
r) ((a ~> (p % b)) -> c ~> (p % d))
-> (p a b -> a ~> (p % b)) -> p a b -> c ~> (p % 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
. p a b -> a ~> (p % b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((Ob b, Ob d) => p a b -> p c d) -> (b ~> d) -> p a b -> p c d
forall (a :: j) (b :: j) 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
\\ b ~> d
r

trivialRep :: forall p a. (Representable p, Ob a) => p (p % a) a
trivialRep :: forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep = ((p % a) ~> (p % a)) -> p (p % a) a
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj @p @a)

type CorepStar :: (k +-> j) -> (j +-> k)
data CorepStar p a b where
  CorepStar :: (Ob b) => {forall {k} {j} (b :: k) (a :: j) (p :: j +-> k).
CorepStar p a b -> a ~> (p %% b)
unCorepStar :: a ~> p %% b} -> CorepStar p a b
instance (Corepresentable p) => Profunctor (CorepStar p) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> CorepStar p a b -> CorepStar p c d
dimap = (c ~> a) -> (b ~> d) -> CorepStar p a b -> CorepStar p c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> CorepStar p a b -> r
\\ CorepStar a ~> (p %% b)
f = r
(Ob a, Ob (p %% b)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (p %% b)) => r) -> (a ~> (p %% b)) -> r
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 ~> (p %% b)
f
instance (Corepresentable p) => Representable (CorepStar p) where
  type CorepStar p % a = p %% a
  index :: forall (a :: k) (b :: j). CorepStar p a b -> a ~> (CorepStar p % b)
index (CorepStar a ~> (p %% b)
f) = a ~> (p %% b)
a ~> (CorepStar p % b)
f
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (CorepStar p % b)) -> CorepStar p a b
tabulate = (a ~> (p %% b)) -> CorepStar p a b
(a ~> (CorepStar p % b)) -> CorepStar p a b
forall {k} {j} (b :: k) (a :: j) (p :: j +-> k).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (CorepStar p % a) ~> (CorepStar p % b)
repMap = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k +-> j) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p

mapCorepStar :: (Corepresentable p, Corepresentable q) => p ~> q -> CorepStar q ~> CorepStar p
mapCorepStar :: forall {k} {j} (p :: k +-> j) (q :: k +-> j).
(Corepresentable p, Corepresentable q) =>
(p ~> q) -> CorepStar q ~> CorepStar p
mapCorepStar (Prof p :~> q
n) = (CorepStar q :~> CorepStar p) -> Prof (CorepStar q) (CorepStar p)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(CorepStar @a a ~> (q %% b)
f) -> (a ~> (p %% b)) -> CorepStar p a b
forall {k} {j} (b :: k) (a :: j) (p :: j +-> k).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (q b (p %% b) -> (q %% b) ~> (p %% b)
forall (a :: j) (b :: k). q a b -> (q %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex (p b (p %% b) -> q b (p %% b)
p :~> q
n (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: k +-> j) (a :: j).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @_ @a)) ((q %% b) ~> (p %% b)) -> (a ~> (q %% b)) -> a ~> (p %% 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
. a ~> (q %% b)
f)

type RepCostar :: (k +-> j) -> (j +-> k)
data RepCostar p a b where
  RepCostar :: (Ob a) => {forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
RepCostar p a b -> (p % a) ~> b
unRepCostar :: p % a ~> b} -> RepCostar p a b
instance (Representable p) => Profunctor (RepCostar p) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> RepCostar p a b -> RepCostar p c d
dimap = (c ~> a) -> (b ~> d) -> RepCostar p a b -> RepCostar p c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> RepCostar p a b -> r
\\ RepCostar (p % a) ~> b
f = r
(Ob a, Ob b) => r
(Ob (p % a), Ob b) => r
r ((Ob (p % a), Ob b) => r) -> ((p % a) ~> b) -> r
forall (a :: j) (b :: j) 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 % a) ~> b
f
instance (Representable p) => Corepresentable (RepCostar p) where
  type RepCostar p %% a = p % a
  coindex :: forall (a :: k) (b :: j).
RepCostar p a b -> (RepCostar p %% a) ~> b
coindex (RepCostar (p % a) ~> b
f) = (RepCostar p %% a) ~> b
(p % a) ~> b
f
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((RepCostar p %% a) ~> b) -> RepCostar p a b
cotabulate = ((RepCostar p %% a) ~> b) -> RepCostar p a b
((p % a) ~> b) -> RepCostar p a b
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (RepCostar p %% a) ~> (RepCostar p %% b)
corepMap = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> j) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p
instance (Representable p, Discrete j, Thin k) => ThinProfunctor (RepCostar p :: j +-> k) where
  type HasArrow (RepCostar p) a b = (p % a) ~ b
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (RepCostar p) a b) =>
RepCostar p a b
arr = ((p % a) ~> b) -> RepCostar p a b
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar b ~> b
(p % a) ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  withArr :: forall (a :: k) (b :: j) r.
RepCostar p a b -> (HasArrow (RepCostar p) a b => r) -> r
withArr (RepCostar (p % a) ~> b
f) HasArrow (RepCostar p) a b => r
r = ((p % a) ~> b) -> (((p % a) ~ b) => r) -> r
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq (p % a) ~> b
f r
((p % a) ~ b) => r
HasArrow (RepCostar p) a b => r
r

mapRepCostar :: (Representable p, Representable q) => p ~> q -> RepCostar q ~> RepCostar p
mapRepCostar :: forall {k} {j} (p :: k +-> j) (q :: k +-> j).
(Representable p, Representable q) =>
(p ~> q) -> RepCostar q ~> RepCostar p
mapRepCostar (Prof p :~> q
n) = (RepCostar q :~> RepCostar p) -> Prof (RepCostar q) (RepCostar p)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(RepCostar @a (q % a) ~> b
f) -> ((p % a) ~> b) -> RepCostar p a b
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((q % a) ~> b
f ((q % a) ~> b) -> ((p % a) ~> (q % a)) -> (p % a) ~> b
forall (b :: j) (c :: j) (a :: j). (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
. q (p % a) a -> (p % a) ~> (q % a)
forall (a :: j) (b :: k). q a b -> a ~> (q % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (p (p % a) a -> q (p % a) a
p :~> q
n (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> j) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
trivialRep @_ @a)))

flipRep :: forall p. (Representable p) => (~>) :~> p -> RepCostar p :~> (~>)
flipRep :: forall {k1} (p :: k1 +-> k1).
Representable p =>
((~>) :~> p) -> RepCostar p :~> (~>)
flipRep (~>) :~> p
n RepCostar p a b
p = RepCostar p a b -> (RepCostar p %% a) ~> b
forall (a :: k1) (b :: k1).
RepCostar p a b -> (RepCostar p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex RepCostar p a b
p ((p % a) ~> b) -> (a ~> (p % a)) -> a ~> b
forall (b :: k1) (c :: k1) (a :: k1).
(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 a -> a ~> (p % a)
forall (a :: k1) (b :: k1). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((a ~> a) -> p a a
(~>) :~> p
n (RepCostar p a b -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src RepCostar p a b
p))

unflipRep :: forall p. (Representable p) => RepCostar p :~> (~>) -> (~>) :~> p
unflipRep :: forall {k1} (p :: k1 +-> k1).
Representable p =>
(RepCostar p :~> (~>)) -> (~>) :~> p
unflipRep RepCostar p :~> (~>)
n a ~> b
f = (a ~> (p % b)) -> p a b
forall (b :: k1) (a :: k1). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (RepCostar p a (p % b) -> a ~> (p % b)
RepCostar p :~> (~>)
n (((p % a) ~> (p % b)) -> RepCostar p a (p % b)
forall {j} {k} (a :: j) (p :: j +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k1 +-> k1) (a :: k1) (b :: k1).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f))) ((Ob a, Ob b) => p a b) -> (a ~> b) -> p a b
forall (a :: k1) (b :: k1) 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

flipCorep :: forall p. (Corepresentable p) => (~>) :~> p -> CorepStar p :~> (~>)
flipCorep :: forall {k1} (p :: k1 +-> k1).
Corepresentable p =>
((~>) :~> p) -> CorepStar p :~> (~>)
flipCorep (~>) :~> p
n CorepStar p a b
p = p b b -> (p %% b) ~> b
forall (a :: k1) (b :: k1). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((b ~> b) -> p b b
(~>) :~> p
n (CorepStar p a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt CorepStar p a b
p)) ((p %% b) ~> b) -> (a ~> (p %% b)) -> a ~> b
forall (b :: k1) (c :: k1) (a :: k1).
(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
. CorepStar p a b -> a ~> (CorepStar p % b)
forall (a :: k1) (b :: k1).
CorepStar p a b -> a ~> (CorepStar p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index CorepStar p a b
p

unflipCorep :: forall p. (Corepresentable p) => CorepStar p :~> (~>) -> (~>) :~> p
unflipCorep :: forall {k1} (p :: k1 +-> k1).
Corepresentable p =>
(CorepStar p :~> (~>)) -> (~>) :~> p
unflipCorep CorepStar p :~> (~>)
n a ~> b
f = ((p %% a) ~> b) -> p a b
forall (a :: k1) (b :: k1). Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (CorepStar p (p %% a) b -> (p %% a) ~> b
CorepStar p :~> (~>)
n (((p %% a) ~> (p %% b)) -> CorepStar p (p %% a) b
forall {k} {j} (b :: k) (a :: j) (p :: j +-> k).
Ob b =>
(a ~> (p %% b)) -> CorepStar p a b
CorepStar (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k1 +-> k1) (a :: k1) (b :: k1).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p a ~> b
f))) ((Ob a, Ob b) => p a b) -> (a ~> b) -> p a b
forall (a :: k1) (b :: k1) 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

type Rep :: (j +-> k) -> j +-> k
data Rep f a b where
  Rep :: forall f a b. (Ob b) => {forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Rep f a b -> a ~> (f @ b)
unRep :: a ~> f @ b} -> Rep f a b
instance (FunctorForRep f) => Profunctor (Rep f) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Rep f a b -> Rep f c d
dimap = (c ~> a) -> (b ~> d) -> Rep f a b -> Rep f c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Rep f a b -> r
\\ Rep a ~> (f @ b)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (f @ b)) => r
r ((Ob a, Ob (f @ b)) => r) -> (a ~> (f @ b)) -> r
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 ~> (f @ b)
f
instance (FunctorForRep f) => Representable (Rep f) where
  type Rep f % a = f @ a
  index :: forall (a :: k) (b :: j). Rep f a b -> a ~> (Rep f % b)
index (Rep a ~> (f @ b)
f) = a ~> (f @ b)
a ~> (Rep f % b)
f
  tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (Rep f % b)) -> Rep f a b
tabulate = (a ~> (f @ b)) -> Rep f a b
(a ~> (Rep f % b)) -> Rep f a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep
  repMap :: forall (a :: j) (b :: j). (a ~> b) -> (Rep f % a) ~> (Rep f % b)
repMap = forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @f