open import Cat.Instances.Elements open import Cat.Instances.Functor open import Cat.Diagram.Terminal open import Cat.Instances.Sets open import Cat.Functor.Base open import Cat.Functor.Hom open import Cat.Prelude import Cat.Reasoning module Cat.Functor.Hom.Representable {o ΞΊ} {C : Precategory o ΞΊ} where

# Representable functorsπ

A functor
$F : \mathcal{C}{^{{\mathrm{op}}}}\to {{\mathbf{Sets}}}_\kappa$
(from a locally
$\kappa$-small
category) is said to be **representable** when it is naturally
isomorphic to
${\mathbf{Hom}}(-, X)$
for an object
$X : \mathcal{C}$
(called the **representing object**) β that is, the functor
$F$
classifies the *maps into*
$X$.
Note that we can evidently dualise the definition, to get what is called
a **corepresentable functor**, one of the form
${\mathbf{Hom}}(X, -)$,
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 C^.β γβ C rep equiv : β {a} β C.Hom a rep β β£ F .Fβ a β£ equiv = IsoβEquiv Ξ» where .fst β represents .C^.from .Ξ· _ .snd .is-iso.inv β represents .C^.to .Ξ· _ .snd .is-iso.rinv x β represents .C^.invr Ξ·β _ $β x .snd .is-iso.linv x β represents .C^.invl Ξ·β _ $β x module rep = C^._β _ 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 β$X$ is a representation of $F$β determines how $X$ 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 $\mathcal{C}$ is a univalent category, then the type of representations for a functor $F$ 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 c-cat (Hom[_,-] C a) _) $β _ Β·Β· 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 $F$ is representable if, and only if, its category of elements $\int F$ 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
$\int F$^{1}, we obtain a natural transformation
$\eta_y : F(y) \to {\mathbf{Hom}}(y,X)$,
given componentwise by interpreting each pair
$(y, s)$
as an object of
$\int F$,
then taking the terminating morphism
$(y, s) \to (X, F(X))$,
which satisfies (by definition)
$F(!)(F(X)) = s$.
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 $ componentwise-invertibleβinvertible nat inv

## Universal constructionsπ

We now show a partial converse to the calculation above: That terminal objects are representing objects for a particular functor. Consider, to be more specific, the constant functor $F : \mathcal{C}{^{{\mathrm{op}}}}\to {{\mathbf{Sets}}}$ which sends everything to the terminal set. When is $F$ representable?

Well, unfolding the definition, itβs when we have an object
$X : \mathcal{C}$
with a natural isomorphism
${\mathbf{Hom}}(-,X) \cong F$.
Unfolding *that*, itβs an object
$X$
for which, given any other object
$Y$,
we have an isomorphism of sets
${\mathbf{Hom}}(Y,X) \cong \{*\}$^{2}. Hence, a representing object for
the βconstantly
$\{*\}$β
functor is precisely a terminal object. It turns out the

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)