🔍

Equations Inline Footnotes

open import Cat.Functor.Properties
open import Cat.Functor.Bifunctor
open import Cat.Instances.Product
open import Cat.Functor.Closed
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Hom {o h} (C : Precategory o h) where

The Hom functor🔗

open import Cat.Reasoning C
open Functor
open _=>_
private variable
  a b : Ob

The assignment of $\mathbf{Hom}\text{-sets}$ in a precategory $\mathcal{C}\text{,}$ thought of as a function of two arguments valued in sets, extends naturally to a bifunctor ${\mathcal{C}}^{\mathrm{op}}\to \mathcal{C}\to \mathbf{Sets}\text{.}$ A morphism $a\to b$ acts on the left by precomposition, $\mathbf{Hom}(b,x)\to \mathbf{Hom}(a,x)\text{,}$ and on the right by postcompoosition, $\mathbf{Hom}(x,a)\to \mathbf{Hom}(x,b)\text{.}$

Hom[-,-] : Bifunctor (C ^op) C (Sets h)
Hom[-,-] = make-bifunctor record where
  F₀ X Y = el! (Hom X Y)

  lmap     f = _∘ f
  rmap     f = f ∘_

Both functoriality constraints, as well as the interchange law lrmap, boil down to the category laws.

  lmap-∘ f g = ext λ h →
    h ∘ g ∘ f   ≡⟨ assoc _ _ _ ⟩≡
    (h ∘ g) ∘ f ∎
  lmap-id    = ext λ h → idr _

  rmap-∘ f g = ext λ h → sym (assoc _ _ _)
  rmap-id    = ext λ h → idl _

  lrmap  f g = ext λ h → sym (assoc _ _ _)

As a bifunctor, $\mathbf{Hom}(-,-)$ has associated partial applications on either side. We use the intuitive names Hom-from and Hom-into, instead of directional names referring to “left” and “right”.

open Bifunctor Hom[-,-] public using ()
  renaming (Left to Hom-into)

open Functor Hom[-,-] public using ()
  renaming (F₀ to Hom-from)

The Yoneda embedding🔗

Since $\mathbf{Hom}(-,-)$ is a functor ${\mathcal{C}}^{\mathrm{op}}\to [\mathcal{C},\mathbf{Sets}]\text{,}$ it flips to give a functor $\mathcal{C}\to [{\mathcal{C}}^{\mathrm{op}},\mathbf{Sets}]\text{:}$ this is $\mathcal{C}\text{’s}$ Yoneda embedding.

よ : Bifunctor C (C ^op) (Sets h)
よ = Flip Hom[-,-]

open Functor よ renaming (F₀ to よ₀) using () public

_ : ∀ {X} → Hom-into X ≡ よ₀ X
_ = refl

The action of よ on morphisms has an inverse, given by evaluating the natural transformation with the identity map; Hence, the Yoneda embedding functor is fully faithful.

よ-is-fully-faithful : is-fully-faithful よ
よ-is-fully-faithful = is-iso→is-equiv λ where
  .is-iso.from nt → nt .η _ id
  .is-iso.rinv nt → ext λ c g →
    nt .η _ id ∘ g   ≡⟨ sym (nt .is-natural _ _ _) $ₚ _ ⟩≡
    nt .η c (id ∘ g) ≡⟨ ap (nt .η c) (idl g) ⟩≡
    nt .η c g        ∎
  .is-iso.linv _  → idr _

よ-is-faithful : is-faithful よ
よ-is-faithful = ff→faithful {F = よ} (よ-is-fully-faithful)

The covariant yoneda embedding🔗

One common point of confusion is why category theorists prefer presheaves over covariant functors into $\mathbf{Sets}\text{.}$ One key reason is that the yoneda embedding into presheaves is covariant, whereas the $\mathbf{Hom}(-,-)$ functor, thought of as an embedding into functors $\mathcal{C}\to \mathbf{Sets}$ is contravariant. This makes the “covariant Yoneda embedding” much less pleasant to work with, though we define it anyways for posterity.

よcov : Functor (C ^op) Cat[ C , Sets h ]
よcov = Hom[-,-]

As expected, the covariant yoneda embedding is also fully faithful.

Hom[-,-]-is-fully-faithful : is-fully-faithful Hom[-,-]
Hom[-,-]-is-fully-faithful = is-iso→is-equiv λ where
  .is-iso.from nt → nt .η _ id
  .is-iso.rinv nt → ext λ c g → sym (nt .is-natural _ _ _) $ₚ _ ∙ ap (nt .η c) (idr g)
  .is-iso.linv h  → idl h

Hom[-,-]-is-faithful : is-faithful Hom[-,-]
Hom[-,-]-is-faithful = ff→faithful {F = Hom[-,-]} (Hom[-,-]-is-fully-faithful)