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) => InitUniversal (r :: j +-> k) (a :: k) where
  type L r a :: j
  initUnivArr :: (Ob a) => 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) => TermUniversal (l :: j +-> k) (b :: j) where
  type R l b :: k
  termUnivArr :: (Ob b) => l (R l b) b
  termUnivProp :: l a b -> a ~> R l b

newtype AsRightAdjoint p a b = AsRightAdjoint {forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
AsRightAdjoint p a b -> p a b
unAsRightAdjoint :: 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) -> AsRightAdjoint p a b -> AsRightAdjoint p c d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AsRightAdjoint p a b -> r)
-> Profunctor (AsRightAdjoint p)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> AsRightAdjoint p a b -> AsRightAdjoint p c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsRightAdjoint p a b -> r
forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf k
forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf j
forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor p =>
(c ~> a)
-> (b ~> d) -> AsRightAdjoint p a b -> AsRightAdjoint p c d
forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> AsRightAdjoint 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) -> AsRightAdjoint p a b -> AsRightAdjoint p c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> AsRightAdjoint p a b -> AsRightAdjoint p c d
$c\\ :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> AsRightAdjoint p a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsRightAdjoint p a b -> r
Profunctor, Profunctor (AsRightAdjoint p)
Profunctor (AsRightAdjoint p) =>
(forall (a :: k) (b :: j).
 AsRightAdjoint p a b -> a ~> (AsRightAdjoint p % b))
-> (forall (b :: j) (a :: k).
    Ob b =>
    (a ~> (AsRightAdjoint p % b)) -> AsRightAdjoint p a b)
-> (forall (a :: j) (b :: j).
    (a ~> b) -> (AsRightAdjoint p % a) ~> (AsRightAdjoint p % b))
-> Representable (AsRightAdjoint p)
forall (a :: k) (b :: j).
AsRightAdjoint p a b -> a ~> (AsRightAdjoint p % b)
forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsRightAdjoint p % b)) -> AsRightAdjoint p a b
forall (a :: j) (b :: j).
(a ~> b) -> (AsRightAdjoint p % a) ~> (AsRightAdjoint p % b)
forall k j (p :: k -> j -> Type).
Representable p =>
Profunctor (AsRightAdjoint p)
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Representable p =>
AsRightAdjoint p a b -> a ~> (AsRightAdjoint p % b)
forall k j (p :: k -> j -> Type) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (AsRightAdjoint p % b)) -> AsRightAdjoint p a b
forall k j (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (AsRightAdjoint p % a) ~> (AsRightAdjoint 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 =>
AsRightAdjoint p a b -> a ~> (AsRightAdjoint p % b)
index :: forall (a :: k) (b :: j).
AsRightAdjoint p a b -> a ~> (AsRightAdjoint p % b)
$ctabulate :: forall k j (p :: k -> j -> Type) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (AsRightAdjoint p % b)) -> AsRightAdjoint p a b
tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsRightAdjoint p % b)) -> AsRightAdjoint p a b
$crepMap :: forall k j (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (AsRightAdjoint p % a) ~> (AsRightAdjoint p % b)
repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (AsRightAdjoint p % a) ~> (AsRightAdjoint p % b)
Representable)
instance (forall a. InitUniversal r a) => Corepresentable (AsRightAdjoint r) 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
f) = 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
f
  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} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> AsRightAdjoint p 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, Ob a) =>
r a (L r a)
initUnivArr)
  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 :: k -> j -> Type) (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, Ob a) =>
r a (L r a)
forall (r :: k -> j -> Type) (a :: k).
(InitUniversal r a, Ob 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 p a b = AsLeftAdjoint {forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
AsLeftAdjoint p a b -> p a b
unAsLeftAdjoint :: 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) -> AsLeftAdjoint p a b -> AsLeftAdjoint p c d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AsLeftAdjoint p a b -> r)
-> Profunctor (AsLeftAdjoint p)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AsLeftAdjoint p a b -> AsLeftAdjoint p c d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsLeftAdjoint p a b -> r
forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf k
forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf j
forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> AsLeftAdjoint p a b -> AsLeftAdjoint p c d
forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> AsLeftAdjoint 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) -> AsLeftAdjoint p a b -> AsLeftAdjoint p c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AsLeftAdjoint p a b -> AsLeftAdjoint p c d
$c\\ :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> AsLeftAdjoint p a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsLeftAdjoint p a b -> r
Profunctor, Profunctor (AsLeftAdjoint p)
Profunctor (AsLeftAdjoint p) =>
(forall (a :: k) (b :: j).
 AsLeftAdjoint p a b -> (AsLeftAdjoint p %% a) ~> b)
-> (forall (a :: k) (b :: j).
    Ob a =>
    ((AsLeftAdjoint p %% a) ~> b) -> AsLeftAdjoint p a b)
-> (forall (a :: k) (b :: k).
    (a ~> b) -> (AsLeftAdjoint p %% a) ~> (AsLeftAdjoint p %% b))
-> Corepresentable (AsLeftAdjoint p)
forall (a :: k) (b :: k).
(a ~> b) -> (AsLeftAdjoint p %% a) ~> (AsLeftAdjoint p %% b)
forall (a :: k) (b :: j).
Ob a =>
((AsLeftAdjoint p %% a) ~> b) -> AsLeftAdjoint p a b
forall (a :: k) (b :: j).
AsLeftAdjoint p a b -> (AsLeftAdjoint p %% a) ~> b
forall k j (p :: k -> j -> Type).
Corepresentable p =>
Profunctor (AsLeftAdjoint p)
forall k j (p :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (AsLeftAdjoint p %% a) ~> (AsLeftAdjoint p %% b)
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((AsLeftAdjoint p %% a) ~> b) -> AsLeftAdjoint p a b
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable p =>
AsLeftAdjoint p a b -> (AsLeftAdjoint 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 =>
AsLeftAdjoint p a b -> (AsLeftAdjoint p %% a) ~> b
coindex :: forall (a :: k) (b :: j).
AsLeftAdjoint p a b -> (AsLeftAdjoint p %% a) ~> b
$ccotabulate :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((AsLeftAdjoint p %% a) ~> b) -> AsLeftAdjoint p a b
cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((AsLeftAdjoint p %% a) ~> b) -> AsLeftAdjoint p a b
$ccorepMap :: forall k j (p :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (AsLeftAdjoint p %% a) ~> (AsLeftAdjoint p %% b)
corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (AsLeftAdjoint p %% a) ~> (AsLeftAdjoint p %% b)
Corepresentable)
instance (forall b. TermUniversal l b) => 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
f) = 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
f
  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} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> AsLeftAdjoint p 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, Ob b) =>
l (R l b) b
termUnivArr)
  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 :: k -> j -> Type) (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, Ob b) =>
l (R l b) b
forall (l :: k -> j -> Type) (b :: j).
(TermUniversal l b, Ob 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 (p :: k -> j -> Type). Profunctor p => CategoryOf k
forall k j (p :: k -> j -> Type). Profunctor p => 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) => InitUniversal (FromAdjunction p) a where
  type L (FromAdjunction p) a = p %% a
  initUnivArr :: Ob a => 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) => TermUniversal (FromAdjunction p) b where
  type R (FromAdjunction p) b = p % b
  termUnivArr :: Ob b => 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