open import Cat.Univalent.Instances.Opposite
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Functor.Properties
open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Functor.Constant
open import Cat.Morphism.Duality
open import Cat.Diagram.Initial
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Instances.Elements.Covariant as Co
import Cat.Reasoning

module Cat.Functor.Hom.Representable {o ΞΊ} {C : Precategory o ΞΊ} where

private
module C = Cat.Reasoning C
module C^ = Cat.Reasoning Cat[ C ^op , Sets ΞΊ ]
module [C,Sets] = Cat.Reasoning Cat[ C , Sets ΞΊ ]
module Sets = Cat.Reasoning (Sets ΞΊ)
open Element-hom
open Functor
open Element
open _=>_


# Representable functorsπ

A functor (from a locally category) is said to be representable when it is naturally isomorphic to for an object (called the representing object) β that is, the functor classifies the maps into Note that we can evidently dualise the definition, to get what is called a corepresentable functor, one of the form but we refer informally to both of these situations as βrepresentablesβ and βrepresenting objectsβ.

record Representation (F : Functor (C ^op) (Sets ΞΊ)) : Type (o β ΞΊ) where
no-eta-equality
field
rep        : C.Ob
represents : F ββΏ Hom-into C rep

module rep = IsoβΏ represents

equiv : β {a} β C.Hom a rep β F Κ» a
equiv = Equiv.inverse (natural-isoβequiv represents _)

module Rep {a} = Equiv (equiv {a})

open Representation
open Representation using (module Rep) public


This definition is deceptively simple: the idea of representable functor (and of representing object) is key to understanding the idea of universal property, which could be called the most important concept in category theory. Most constructions in category theory specified in terms of the existence of certain maps are really instances of representing objects for functors: limits, colimits, coends, adjoint functors, Kan extensions, etc.

The first thing we will observe is an immediate consequence of the Yoneda lemma: representing objects are unique. Intuitively this is because β is a representation of β determines how reacts to being mapped into, and since the only thing we can probe objects in an arbitrary category by are morphisms, two objects which react to morphisms in the same way must be isomorphic.

representation-unique : {F : Functor (C ^op) (Sets ΞΊ)} (X Y : Representation F)
β X .rep C.β Y .rep
representation-unique X Y =
is-ffβessentially-injective {F = γ C} (γ-is-fully-faithful C) γXβγY where
γXβγY : γβ C (X .rep) C^.β γβ C (Y .rep)
γXβγY = (X .represents C^.Isoβ»ΒΉ) C^.βIso Y .represents


Therefore, if is a univalent category, then the type of representations for a functor is a proposition. This does not follow immediately from the lemma above: we also need to show that the isomorphism computed by the full-faithfulness of the Yoneda embedding commutes with the specified representation isomorphism. This follows by construction, but the proof needs to commute applications of functors and paths-from-isos, which is never pretty:

Representation-is-prop : β {F} β is-category C β is-prop (Representation F)
Representation-is-prop {F = F} c-cat x y = path where
module X = Representation x
module Y = Representation y

objs : X.rep β‘ Y.rep
objs = c-cat .to-path (representation-unique x y)

path : x β‘ y
path i .rep = objs i
path i .represents =
C^.β-pathp refl (ap (γβ C) objs) {f = X.represents} {g = Y.represents}
(Nat-pathp _ _ Ξ» a β Hom-pathp-reflr (Sets _)
{A = F .Fβ a} {q = Ξ» i β el! (C.Hom a (objs i))}
(funext Ξ» x β
ap (Ξ» e β e .Sets.to) (ap-Fβ-iso (Hom-from C a) c-cat _) $β _ Β·Β· sym (Y.rep.to .is-natural _ _ _)$β _
Β·Β· ap Y.Rep.from (sym (X.rep.from .is-natural _ _ _ $β _) Β·Β· ap X.Rep.to (C.idl _) Β·Β· X.Rep.Ξ΅ _))) i  ## As terminal objectsπ We begin to connect the idea of representing objects to other universal constructions by proving this alternative characterisation of representations: A functor is representable if, and only if, its category of elements has a terminal object. terminal-elementβrepresentation : {F : Functor (C ^op) (Sets ΞΊ)} β Terminal (β« C F) β Representation F terminal-elementβrepresentation {F} term = f-rep where module F = Functor F open Terminal term  From the terminal object in 1, we obtain a natural transformation given componentwise by interpreting each pair as an object of then taking the terminating morphism which satisfies (by definition) This natural transformation is componentwise invertible, as the calculation below shows, so it constitutes a natural isomorphism.  nat : F => γβ C (top .ob) nat .Ξ· ob section = hasβ€ (elem ob section) .centre .hom nat .is-natural x y f = funext Ξ» sect β ap hom$ hasβ€ _ .paths $elem-hom _$
F.β (hasβ€ _ .centre .hom C.β f) (top .section)   β‘β¨ happly (F.F-β _ _) _ β©β‘
F.β f (F.β (hasβ€ _ .centre .hom) (top .section)) β‘β¨ ap (F.β f) (hasβ€ _ .centre .commute) β©β‘
F.β f sect                                       β

inv : β x β Sets.is-invertible (nat .Ξ· x)
inv x = Sets.make-invertible
(Ξ» f β F.β f (top .section))
(funext Ξ» x β ap hom $hasβ€ _ .paths (elem-hom x refl)) (funext Ξ» x β hasβ€ _ .centre .commute) f-rep : Representation F f-rep .rep = top .ob f-rep .represents = C^.invertibleβiso nat$
invertibleβinvertibleβΏ nat inv


In the other direction, we take the terminal element to be the image of the identity on the representing object.

representationβterminal-element
: {F : Functor (C ^op) (Sets ΞΊ)}
β Representation F β Terminal (β« C F)
representationβterminal-element {F} F-rep = term where
module F = Functor F
module R = rep F-rep
open Terminal

term : Terminal (β« C F)
term .top .ob = F-rep .rep
term .top .section = R.from .Ξ· _ C.id
term .hasβ€ (elem o s) .centre .hom = R.to .Ξ· _ s
term .hasβ€ (elem o s) .centre .commute =
F.β (R.to .Ξ· o s) (R.from .Ξ· _ C.id) β‘Λβ¨ R.from .is-natural _ _ _ $β _ β©β‘Λ R.from .Ξ· _ β C.id C.β R.to .Ξ· o s β β‘β¨ ap! (C.idl _) β©β‘ R.from .Ξ· _ (R.to .Ξ· o s) β‘β¨ unext R.invr o s β©β‘ s β term .hasβ€ (elem o s) .paths h = ext$
R.to .Ξ· o β s β                  β‘Λβ¨ apΒ‘ comm β©β‘Λ
R.to .Ξ· o (R.from .Ξ· _ (h .hom)) β‘β¨ unext R.invl o _ β©β‘
h .hom                           β
where
comm =
R.from .Ξ· _ β h .hom β          β‘Λβ¨ apΒ‘ (C.idl _) β©β‘Λ
R.from .Ξ· _ (C.id C.β h .hom)   β‘β¨ R.from .is-natural _ _ _ $β _ β©β‘ F.β (h .hom) (R.from .Ξ· _ C.id) β‘β¨ h .commute β©β‘ s β  ## Universal constructionsπ In particular, we can show that terminal objects are representing objects for a particular functor. Consider, to be more specific, the constant functor which sends everything to the terminal set. When is representable? Well, unfolding the definition, itβs when we have an object with a natural isomorphism Unfolding that, itβs an object for which, given any other object we have an isomorphism of sets 2. Hence, a representing object for the βconstantly β functor is precisely a terminal object. representable-unitβterminal : Representation (Const (el (Lift _ β€) (hlevel 2))) β Terminal C representable-unitβterminal repr .Terminal.top = repr .rep representable-unitβterminal repr .Terminal.hasβ€ ob = retractβis-contr (Rep.from repr) (Ξ» _ β lift tt) (Rep.Ξ· repr) (hlevel 0)  This can be seen as a special case of the construction above: is representable just when its category of elements has a terminal object, but in this case the category of elements of is just ## Corepresentable functorsπ As noted earlier, we can dualise the definition of a representable functor to the covariant setting to get corepresentable functors. record Corepresentation (F : Functor C (Sets ΞΊ)) : Type (o β ΞΊ) where no-eta-equality field corep : C.Ob corepresents : F β βΏ Hom-from C corep module corep = IsoβΏ corepresents coequiv : β {a} β C.Hom corep a β F Κ» a coequiv = Equiv.inverse (natural-isoβequiv corepresents _) module Corep {a} = Equiv (coequiv {a}) open Corepresentation open Corepresentation using (module Corep) public  Much like their contravariant cousins, corepresenting objects are unique up to isomorphism. corepresentation-unique : {F : Functor C (Sets ΞΊ)} (X Y : Corepresentation F) β X .corep C.β Y .corep  We omit the proof, as it is identical to the representable case. corepresentation-unique X Y = is-ffβessentially-injective {F = Functor.op (γcov C)} (γcov-is-fully-faithful C) (isoβco-iso (Cat[ C , Sets ΞΊ ]) ni) where ni : Hom-from C (Y .corep) β βΏ Hom-from C (X .corep) ni = (Y .corepresents niβ»ΒΉ) βni X .corepresents  This implies that the type of corepresentations is a proposition when is univalent. Corepresentation-is-prop : β {F} β is-category C β is-prop (Corepresentation F)  We opt to not show the proof, as it is even nastier than the proof for representables due to the fact that the yoneda embedding for covariant functors is itself contravariant. Corepresentation-is-prop {F = F} c-cat X Y = path where objs : X .corep β‘ Y .corep objs = c-cat .to-path (corepresentation-unique X Y) path : X β‘ Y path i .corep = objs i path i .corepresents = [C,Sets].β -pathp refl (ap (Hom-from C) objs) {f = X .corepresents} {g = Y .corepresents} (Nat-pathp _ _ Ξ» a β Hom-pathp-reflr (Sets _) {A = F .Fβ a} {q = Ξ» i β el! (C.Hom (objs i) a)} (funext Ξ» x β ap (Ξ» e β e .Sets.to) (ap-Fβ-iso (Hom-into C a) (opposite-is-category c-cat) _)$β _
Β·Β· sym (corep.to Y .is-natural _ _ _ $β _) Β·Β· ap (Corep.from Y) (sym (corep.from X .is-natural _ _ _$β _)
Β·Β· ap (Corep.to X) (C.idr _)
Β·Β· Corep.Ξ΅ X _)))
i


Dualising the representable case, we have that a functor is corepresentable if and only if its covariant category of elements has an initial object.

initial-elementβcorepresentation
: {F : Functor C (Sets ΞΊ)}
β Initial (Co.β« F) β Corepresentation F

corepresentationβinitial-element
: {F : Functor C (Sets ΞΊ)}
β Corepresentation F β Initial (Co.β« F)

The proofs are again entirely analogous to the representable case.
initial-elementβcorepresentation {F} init = f-corep where
module F = Functor F
open Initial init
open Co.Element
open Co.Element-hom
nat : F => Hom-from C (bot .ob)
nat .Ξ· ob section = hasβ₯ (Co.elem ob section) .centre .hom
nat .is-natural x y f = funext Ξ» sect β ap hom $hasβ₯ _ .paths$ Co.elem-hom _ $F.β (f C.β hasβ₯ _ .centre .hom) (bot .section) β‘β¨ happly (F.F-β _ _) _ β©β‘ F.β f (F.β (hasβ₯ _ .centre .hom) (bot .section)) β‘β¨ ap (F.β f) (hasβ₯ _ .centre .commute) β©β‘ F.β f sect β inv : β x β Sets.is-invertible (nat .Ξ· x) inv x = Sets.make-invertible (Ξ» f β F.β f (bot .section)) (funext Ξ» x β ap hom$ hasβ₯ _ .paths (Co.elem-hom x refl))
(funext Ξ» x β hasβ₯ _ .centre .commute)

f-corep : Corepresentation F
f-corep .corep = bot .ob
f-corep .corepresents = [C,Sets].invertibleβiso nat $invertibleβinvertibleβΏ nat inv corepresentationβinitial-element {F} F-corep = init where module F = Functor F module R = corep F-corep open Initial open Co.Element open Co.Element-hom init : Initial (Co.β« F) init .bot .ob = F-corep .corep init .bot .section = R.from .Ξ· _ C.id init .hasβ₯ (Co.elem o s) .centre .hom = R.to .Ξ· _ s init .hasβ₯ (Co.elem o s) .centre .commute = F.β (R.to .Ξ· o s) (R.from .Ξ· _ C.id) β‘Λβ¨ R.from .is-natural _ _ _$β _ β©β‘Λ
R.from .Ξ· _ β R.to .Ξ· o s C.β C.id β β‘β¨ ap! (C.idr _) β©β‘
R.from .Ξ· _ (R.to .Ξ· o s)            β‘β¨ unext R.invr o s β©β‘
s                                    β
init .hasβ₯ (Co.elem o s) .paths h = ext $R.to .Ξ· o β s β β‘Λβ¨ apΒ‘ comm β©β‘Λ R.to .Ξ· o (R.from .Ξ· _ (h .hom)) β‘β¨ unext R.invl o _ β©β‘ h .hom β where comm = R.from .Ξ· _ β h .hom β β‘Λβ¨ apΒ‘ (C.idr _) β©β‘Λ R.from .Ξ· _ (h .hom C.β C.id) β‘β¨ R.from .is-natural _ _ _$β _ β©β‘
F.β (h .hom) (R.from .Ξ· _ C.id) β‘β¨ h .commute β©β‘
s                               β


## Corepresentable functors preserve limitsπ

A useful fact about corepresentable functors is that they preserve all limits. To show this, we first need to show that the covariant hom functor preserves limits.

To get an intuition for why this is true, consider how the functor behaves on products. The set of morphisms is equivalent to the set of pairs of morphisms (See product-repr for a proof of this equivalence).

Hom-from-preserves-limits
: β {o' ΞΊ'}
β (c : C.Ob)
β is-continuous o' ΞΊ' (Hom-from C c)
Hom-from-preserves-limits c {Diagram = Dia} {K} {eps} lim =
to-is-limitp ml (funext Ξ» _ β refl) where
open make-is-limit
module lim = is-limit lim

ml : make-is-limit _ _
ml .Ο j f = lim.Ο j C.β f
ml .commutes f = funext Ξ» g β
C.pulll (sym (eps .is-natural _ _ _))
ml .universal eps p x =
lim.universal (Ξ» j β eps j x) (Ξ» f β p f $β x) ml .factors _ _ = funext Ξ» _ β lim.factors _ _ ml .unique eps p other q = funext Ξ» x β lim.unique _ _ _ Ξ» j β q j$β x


Preservation of limits by corepresentable functors then follows from a general fact about functors: if preserves limits, and is naturally isomorphic to then must also preserve limits.

corepresentable-preserves-limits
: β {o' ΞΊ'} {F}
β Corepresentation F
β is-continuous o' ΞΊ' F
corepresentable-preserves-limits F-corep lim =
natural-isoβpreserves-limits
(F-corep .corepresents niβ»ΒΉ)
(Hom-from-preserves-limits (F-corep .corep))
lim


We can show a similar fact for representable functors, but with a twist: they reverse colimits! This is due to the fact that a representable functor is contravariant. Specifically, will take limits in to limits in but limits in are colimits, so will take colimits in to limits in

A less formal perspective on this is that the collection of maps out of a colimit is still defined as a limit in For instance, to give a out of a coproduct, we are required to give a pair of maps and

γ-reverses-colimits
: β {o' ΞΊ'}
β (c : C.Ob)
β is-cocontinuous o' ΞΊ' (Functor.op (γβ C c))
γ-reverses-colimits c {Diagram = Dia} {K} {eta} colim =
to-is-colimitp mc (funext Ξ» _ β refl) where
open make-is-colimit
module colim = is-colimit colim

mc : make-is-colimit _ _
mc .Ο j f = f C.β colim.Ο j
mc .commutes f = funext Ξ» g β
C.pullr (eta .is-natural _ _ _)
mc .universal eta p x =
colim.universal (Ξ» j β eta j x) (Ξ» f β p f $β x) mc .factors eta p = funext Ξ» _ β colim.factors _ _ mc .unique eta p other q = funext Ξ» x β colim.unique _ _ _ Ξ» j β q j$β x

representable-reverses-colimits
: β {o' ΞΊ'} {F}
β Representation F
β is-cocontinuous o' ΞΊ' (Functor.op F)
representable-reverses-colimits F-rep colim =
natural-isoβpreserves-colimits
((F-rep .represents ni^op) niβ»ΒΉ)
(γ-reverses-colimits (F-rep .rep))
colim


1. Which, recall, consists of an object and a section β©οΈ

2. which varies naturally in but this naturality is not used in this simple caseβ©οΈ