module Proarrow.Universal where

import Data.Kind (Constraint)

import Proarrow.Adjunction (Adjunction)
import Proarrow.Core (CategoryOf (..), Profunctor (..), lmap, rmap, type (+->))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep)
import Proarrow.Profunctor.Representable (Representable (..), trivialRep)

-- | The initial universal property of a functor @r@ (as a representable profunctor) and an object @a@.
type InitUniversal :: forall {j} {k}. (j +-> k) -> k -> Constraint
class (Representable r, Ob a) => InitUniversal (r :: j +-> k) (a :: k) where
  type L r a :: j
  initUnivArr :: r a (L r a)
  initUnivProp :: r a b -> L r a ~> b

-- | The terminal universal property of a functor @l@ (as a corepresentable profunctor) and an object @b@.
type TermUniversal :: forall {j} {k}. (j +-> k) -> j -> Constraint
class (Corepresentable l, Ob b) => TermUniversal (l :: j +-> k) (b :: j) where
  type R l b :: k
  termUnivArr :: l (R l b) b
  termUnivProp :: l a b -> a ~> R l b

newtype AsRightAdjoint r a b = AsRightAdjoint {forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
AsRightAdjoint r a b -> r a b
unAsRightAdjoint :: r a b}
  deriving newtype (CategoryOf k
CategoryOf j
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a)
 -> (b ~> d) -> AsRightAdjoint r a b -> AsRightAdjoint r c d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AsRightAdjoint r a b -> r)
-> Profunctor (AsRightAdjoint r)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> AsRightAdjoint r a b -> AsRightAdjoint r c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsRightAdjoint r a b -> r
forall k j (r :: k -> j -> Type). Profunctor r => CategoryOf k
forall k j (r :: k -> j -> Type). Profunctor r => CategoryOf j
forall k j (r :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor r =>
(c ~> a)
-> (b ~> d) -> AsRightAdjoint r a b -> AsRightAdjoint r c d
forall k j (r :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor r =>
((Ob a, Ob b) => r) -> AsRightAdjoint r a b -> r
forall {j} {k} (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
$cdimap :: forall k j (r :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor r =>
(c ~> a)
-> (b ~> d) -> AsRightAdjoint r a b -> AsRightAdjoint r c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> AsRightAdjoint r a b -> AsRightAdjoint r c d
$c\\ :: forall k j (r :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor r =>
((Ob a, Ob b) => r) -> AsRightAdjoint r a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsRightAdjoint r a b -> r
Profunctor, Profunctor (AsRightAdjoint r)
Profunctor (AsRightAdjoint r) =>
(forall (a :: k) (b :: j).
 AsRightAdjoint r a b -> a ~> (AsRightAdjoint r % b))
-> (forall (b :: j) (a :: k).
    Ob b =>
    (a ~> (AsRightAdjoint r % b)) -> AsRightAdjoint r a b)
-> (forall (a :: j) (b :: j).
    (a ~> b) -> (AsRightAdjoint r % a) ~> (AsRightAdjoint r % b))
-> Representable (AsRightAdjoint r)
forall (a :: k) (b :: j).
AsRightAdjoint r a b -> a ~> (AsRightAdjoint r % b)
forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsRightAdjoint r % b)) -> AsRightAdjoint r a b
forall (a :: j) (b :: j).
(a ~> b) -> (AsRightAdjoint r % a) ~> (AsRightAdjoint r % b)
forall k j (r :: k -> j -> Type).
Representable r =>
Profunctor (AsRightAdjoint r)
forall k j (r :: k -> j -> Type) (a :: k) (b :: j).
Representable r =>
AsRightAdjoint r a b -> a ~> (AsRightAdjoint r % b)
forall k j (r :: k -> j -> Type) (b :: j) (a :: k).
(Representable r, Ob b) =>
(a ~> (AsRightAdjoint r % b)) -> AsRightAdjoint r a b
forall k j (r :: k -> j -> Type) (a :: j) (b :: j).
Representable r =>
(a ~> b) -> (AsRightAdjoint r % a) ~> (AsRightAdjoint r % b)
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> a ~> (p % b))
-> (forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b)
-> (forall (a :: j) (b :: j). (a ~> b) -> (p % a) ~> (p % b))
-> Representable p
$cindex :: forall k j (r :: k -> j -> Type) (a :: k) (b :: j).
Representable r =>
AsRightAdjoint r a b -> a ~> (AsRightAdjoint r % b)
index :: forall (a :: k) (b :: j).
AsRightAdjoint r a b -> a ~> (AsRightAdjoint r % b)
$ctabulate :: forall k j (r :: k -> j -> Type) (b :: j) (a :: k).
(Representable r, Ob b) =>
(a ~> (AsRightAdjoint r % b)) -> AsRightAdjoint r a b
tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsRightAdjoint r % b)) -> AsRightAdjoint r a b
$crepMap :: forall k j (r :: k -> j -> Type) (a :: j) (b :: j).
Representable r =>
(a ~> b) -> (AsRightAdjoint r % a) ~> (AsRightAdjoint r % b)
repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (AsRightAdjoint r % a) ~> (AsRightAdjoint r % b)
Representable)
instance (forall (a :: k). Ob a => InitUniversal r a, Representable r) => Corepresentable (AsRightAdjoint (r :: j +-> k)) where
  type AsRightAdjoint r %% a = L r a
  coindex :: forall (a :: k) (b :: j).
AsRightAdjoint r a b -> (AsRightAdjoint r %% a) ~> b
coindex (AsRightAdjoint r a b
r) = r a b -> L r a ~> b
forall (b :: j). r a b -> L r a ~> b
forall {j} {k} (r :: j +-> k) (a :: k) (b :: j).
InitUniversal r a =>
r a b -> L r a ~> b
initUnivProp r a b
r ((Ob a, Ob b) => L r a ~> b) -> r a b -> L r a ~> b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> 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
\\ r a b
r
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((AsRightAdjoint r %% a) ~> b) -> AsRightAdjoint r a b
cotabulate (AsRightAdjoint r %% a) ~> b
f = r a b -> AsRightAdjoint r a b
forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
r a b -> AsRightAdjoint r a b
AsRightAdjoint ((L r a ~> b) -> r a (L r a) -> r 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 (AsRightAdjoint r %% a) ~> b
L r a ~> b
f r a (L r a)
forall {j} {k} (r :: j +-> k) (a :: k).
InitUniversal r a =>
r a (L r a)
initUnivArr) ((Ob (L r a), Ob b) => AsRightAdjoint r a b)
-> (L r a ~> b) -> AsRightAdjoint r a b
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
\\ (AsRightAdjoint r %% a) ~> b
L r a ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (AsRightAdjoint r %% a) ~> (AsRightAdjoint r %% b)
corepMap @a @b a ~> b
f = forall {j} {k} (r :: j +-> k) (a :: k) (b :: j).
InitUniversal r a =>
r a b -> L r a ~> b
forall (r :: j +-> k) (a :: k) (b :: j).
InitUniversal r a =>
r a b -> L r a ~> b
initUnivProp @r @a ((a ~> b) -> r b (L r b) -> r a (L r 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 (forall {j} {k} (r :: j +-> k) (a :: k).
InitUniversal r a =>
r a (L r a)
forall (r :: j +-> k) (a :: k). InitUniversal r a => r a (L r a)
initUnivArr @r @b)) ((Ob a, Ob b) => L r a ~> L r b) -> (a ~> b) -> L r a ~> L r 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 ~> b
f

newtype AsLeftAdjoint l a b = AsLeftAdjoint {forall {k} {k} (l :: k -> k -> Type) (a :: k) (b :: k).
AsLeftAdjoint l a b -> l a b
unAsLeftAdjoint :: l a b}
  deriving newtype (CategoryOf k
CategoryOf j
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AsLeftAdjoint l a b -> r)
-> Profunctor (AsLeftAdjoint l)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsLeftAdjoint l a b -> r
forall k j (r :: k -> j -> Type). Profunctor r => CategoryOf k
forall k j (r :: k -> j -> Type). Profunctor r => CategoryOf j
forall k j (l :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor l =>
(c ~> a) -> (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c d
forall k j (l :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor l =>
((Ob a, Ob b) => r) -> AsLeftAdjoint l a b -> r
forall {j} {k} (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
$cdimap :: forall k j (l :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor l =>
(c ~> a) -> (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AsLeftAdjoint l a b -> AsLeftAdjoint l c d
$c\\ :: forall k j (l :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor l =>
((Ob a, Ob b) => r) -> AsLeftAdjoint l a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsLeftAdjoint l a b -> r
Profunctor, Profunctor (AsLeftAdjoint l)
Profunctor (AsLeftAdjoint l) =>
(forall (a :: k) (b :: j).
 AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b)
-> (forall (a :: k) (b :: j).
    Ob a =>
    ((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b)
-> (forall (a :: k) (b :: k).
    (a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b))
-> Corepresentable (AsLeftAdjoint l)
forall (a :: k) (b :: k).
(a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b)
forall (a :: k) (b :: j).
Ob a =>
((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b
forall (a :: k) (b :: j).
AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b
forall k j (l :: k -> j -> Type).
Corepresentable l =>
Profunctor (AsLeftAdjoint l)
forall k j (l :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable l =>
(a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b)
forall k j (l :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable l, Ob a) =>
((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b
forall k j (l :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable l =>
AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> (p %% a) ~> b)
-> (forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b)
-> (forall (a :: k) (b :: k). (a ~> b) -> (p %% a) ~> (p %% b))
-> Corepresentable p
$ccoindex :: forall k j (l :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable l =>
AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b
coindex :: forall (a :: k) (b :: j).
AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b
$ccotabulate :: forall k j (l :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable l, Ob a) =>
((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b
cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b
$ccorepMap :: forall k j (l :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable l =>
(a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b)
corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b)
Corepresentable)
instance (forall b. Ob b => TermUniversal l b, Corepresentable l) => Representable (AsLeftAdjoint l) where
  type AsLeftAdjoint l % b = R l b
  index :: forall (a :: k) (b :: j).
AsLeftAdjoint l a b -> a ~> (AsLeftAdjoint l % b)
index (AsLeftAdjoint l a b
l) = l a b -> a ~> R l b
forall (a :: k). l a b -> a ~> R l b
forall {j} {k} (l :: j +-> k) (b :: j) (a :: k).
TermUniversal l b =>
l a b -> a ~> R l b
termUnivProp l a b
l ((Ob a, Ob b) => a ~> R l b) -> l a b -> a ~> R l b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> l 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
\\ l a b
l
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsLeftAdjoint l % b)) -> AsLeftAdjoint l a b
tabulate a ~> (AsLeftAdjoint l % b)
f = l a b -> AsLeftAdjoint l a b
forall {k} {k} (l :: k -> k -> Type) (a :: k) (b :: k).
l a b -> AsLeftAdjoint l a b
AsLeftAdjoint ((a ~> R l b) -> l (R l b) b -> 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 ~> (AsLeftAdjoint l % b)
a ~> R l b
f l (R l b) b
forall {j} {k} (l :: j +-> k) (b :: j).
TermUniversal l b =>
l (R l b) b
termUnivArr) ((Ob a, Ob (R l b)) => AsLeftAdjoint l a b)
-> (a ~> R l b) -> AsLeftAdjoint l 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 ~> (AsLeftAdjoint l % b)
a ~> R l b
f
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (AsLeftAdjoint l % a) ~> (AsLeftAdjoint l % b)
repMap @a @b a ~> b
f = forall {j} {k} (l :: j +-> k) (b :: j) (a :: k).
TermUniversal l b =>
l a b -> a ~> R l b
forall (l :: j +-> k) (b :: j) (a :: k).
TermUniversal l b =>
l a b -> a ~> R l b
termUnivProp @l @b ((a ~> b) -> l (R l a) a -> l (R l 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 a ~> b
f (forall {j} {k} (l :: j +-> k) (b :: j).
TermUniversal l b =>
l (R l b) b
forall (l :: j +-> k) (b :: j). TermUniversal l b => l (R l b) b
termUnivArr @l @a)) ((Ob a, Ob b) => R l a ~> R l b) -> (a ~> b) -> R l a ~> R l b
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
\\ a ~> b
f

newtype FromAdjunction p a b = FromAdjunction {forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
FromAdjunction p a b -> p a b
unFromAdjunction :: p a b}
  deriving newtype (CategoryOf k
CategoryOf j
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a)
 -> (b ~> d) -> FromAdjunction p a b -> FromAdjunction p c d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> FromAdjunction p a b -> r)
-> Profunctor (FromAdjunction p)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> FromAdjunction p a b -> FromAdjunction p c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> FromAdjunction p a b -> r
forall k j (r :: k -> j -> Type). Profunctor r => CategoryOf k
forall k j (r :: k -> j -> Type). Profunctor r => CategoryOf j
forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor p =>
(c ~> a)
-> (b ~> d) -> FromAdjunction p a b -> FromAdjunction p c d
forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> FromAdjunction p a b -> r
forall {j} {k} (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
$cdimap :: forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor p =>
(c ~> a)
-> (b ~> d) -> FromAdjunction p a b -> FromAdjunction p c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> FromAdjunction p a b -> FromAdjunction p c d
$c\\ :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> FromAdjunction p a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> FromAdjunction p a b -> r
Profunctor, Profunctor (FromAdjunction p)
Profunctor (FromAdjunction p) =>
(forall (a :: k) (b :: j).
 FromAdjunction p a b -> a ~> (FromAdjunction p % b))
-> (forall (b :: j) (a :: k).
    Ob b =>
    (a ~> (FromAdjunction p % b)) -> FromAdjunction p a b)
-> (forall (a :: j) (b :: j).
    (a ~> b) -> (FromAdjunction p % a) ~> (FromAdjunction p % b))
-> Representable (FromAdjunction p)
forall (a :: k) (b :: j).
FromAdjunction p a b -> a ~> (FromAdjunction p % b)
forall (b :: j) (a :: k).
Ob b =>
(a ~> (FromAdjunction p % b)) -> FromAdjunction p a b
forall (a :: j) (b :: j).
(a ~> b) -> (FromAdjunction p % a) ~> (FromAdjunction p % b)
forall k j (p :: k -> j -> Type).
Representable p =>
Profunctor (FromAdjunction p)
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Representable p =>
FromAdjunction p a b -> a ~> (FromAdjunction p % b)
forall k j (p :: k -> j -> Type) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (FromAdjunction p % b)) -> FromAdjunction p a b
forall k j (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (FromAdjunction p % a) ~> (FromAdjunction p % b)
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> a ~> (p % b))
-> (forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b)
-> (forall (a :: j) (b :: j). (a ~> b) -> (p % a) ~> (p % b))
-> Representable p
$cindex :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Representable p =>
FromAdjunction p a b -> a ~> (FromAdjunction p % b)
index :: forall (a :: k) (b :: j).
FromAdjunction p a b -> a ~> (FromAdjunction p % b)
$ctabulate :: forall k j (p :: k -> j -> Type) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (FromAdjunction p % b)) -> FromAdjunction p a b
tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (FromAdjunction p % b)) -> FromAdjunction p a b
$crepMap :: forall k j (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (FromAdjunction p % a) ~> (FromAdjunction p % b)
repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (FromAdjunction p % a) ~> (FromAdjunction p % b)
Representable, Profunctor (FromAdjunction p)
Profunctor (FromAdjunction p) =>
(forall (a :: k) (b :: j).
 FromAdjunction p a b -> (FromAdjunction p %% a) ~> b)
-> (forall (a :: k) (b :: j).
    Ob a =>
    ((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b)
-> (forall (a :: k) (b :: k).
    (a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b))
-> Corepresentable (FromAdjunction p)
forall (a :: k) (b :: k).
(a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b)
forall (a :: k) (b :: j).
Ob a =>
((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b
forall (a :: k) (b :: j).
FromAdjunction p a b -> (FromAdjunction p %% a) ~> b
forall k j (p :: k -> j -> Type).
Corepresentable p =>
Profunctor (FromAdjunction p)
forall k j (p :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b)
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable p =>
FromAdjunction p a b -> (FromAdjunction p %% a) ~> b
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> (p %% a) ~> b)
-> (forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b)
-> (forall (a :: k) (b :: k). (a ~> b) -> (p %% a) ~> (p %% b))
-> Corepresentable p
$ccoindex :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable p =>
FromAdjunction p a b -> (FromAdjunction p %% a) ~> b
coindex :: forall (a :: k) (b :: j).
FromAdjunction p a b -> (FromAdjunction p %% a) ~> b
$ccotabulate :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b
cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b
$ccorepMap :: forall k j (p :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b)
corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b)
Corepresentable)
instance (Adjunction p, Ob a) => InitUniversal (FromAdjunction p) a where
  type L (FromAdjunction p) a = p %% a
  initUnivArr :: FromAdjunction p a (L (FromAdjunction p) a)
initUnivArr = FromAdjunction p a (FromAdjunction p %% a)
FromAdjunction p a (L (FromAdjunction p) a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep
  initUnivProp :: forall (b :: j).
FromAdjunction p a b -> L (FromAdjunction p) a ~> b
initUnivProp = FromAdjunction p a b -> (FromAdjunction p %% a) ~> b
FromAdjunction p a b -> L (FromAdjunction p) a ~> b
forall (a :: k) (b :: j).
FromAdjunction p a b -> (FromAdjunction p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex
instance (Adjunction p, Ob b) => TermUniversal (FromAdjunction p) b where
  type R (FromAdjunction p) b = p % b
  termUnivArr :: FromAdjunction p (R (FromAdjunction p) b) b
termUnivArr = FromAdjunction p (FromAdjunction p % b) b
FromAdjunction p (R (FromAdjunction p) b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep
  termUnivProp :: forall (a :: k).
FromAdjunction p a b -> a ~> R (FromAdjunction p) b
termUnivProp = FromAdjunction p a b -> a ~> (FromAdjunction p % b)
FromAdjunction p a b -> a ~> R (FromAdjunction p) b
forall (a :: k) (b :: j).
FromAdjunction p a b -> a ~> (FromAdjunction p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index