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:Copβ†’SetsΞΊ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 Hom(βˆ’,X){\mathbf{Hom}}(-, X) for an object X:CX : \mathcal{C} (called the representing object) β€” that is, the functor FF classifies the maps into XX. Note that we can evidently dualise the definition, to get what is called a corepresentable functor, one of the form Hom(X,βˆ’){\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 β€œXX is a representation of FF” determines how XX 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 C\mathcal{C} is a univalent category, then the type of representations for a functor FF 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 FF is representable if, and only if, its category of elements ∫F\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 ∫F\int F1, we obtain a natural transformation Ξ·y:F(y)β†’Hom(y,X)\eta_y : F(y) \to {\mathbf{Hom}}(y,X), given componentwise by interpreting each pair (y,s)(y, s) as an object of ∫F\int F, then taking the terminating morphism (y,s)β†’(X,F(X))(y, s) \to (X, F(X)), which satisfies (by definition) F(!)(F(X))=sF(!)(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:Cop→SetsF : \mathcal{C}{^{{\mathrm{op}}}}\to {{\mathbf{Sets}}} which sends everything to the terminal set. When is FF representable?

Well, unfolding the definition, it’s when we have an object X:CX : \mathcal{C} with a natural isomorphism Hom(βˆ’,X)β‰…F{\mathbf{Hom}}(-,X) \cong F. Unfolding that, it’s an object XX for which, given any other object YY, we have an isomorphism of sets Hom(Y,X)β‰…{βˆ—}{\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)

  1. Which, recall, consists of an object X:CX : \mathcal{C} and a section F(X):SetsF(X) : {{\mathbf{Sets}}}β†©οΈŽ

  2. which varies naturally in YY, but this naturality is not used in this simple caseβ†©οΈŽ