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

The Hom functor🔗

We prove that the assignment of $Hom -sets$ in a Precategory $C$ is a functor, specifically a bifunctor from $C^{op} \times C$ to $Sets .$ The action of $(f, h)$ on a morphism $g$ is given by $h \circ g \circ f;$ Since $f$ is acting by precomposition, the first coordinate is contravariant ( $C^{op}).$

Hom[-,-] : Functor ((C ^op) ×ᶜ C) (Sets h)
Hom[-,-] .F₀ (a , b) = el (Hom a b) (Hom-set a b)
Hom[-,-] .F₁ (f , h) g = h ∘ g ∘ f
Hom[-,-] .F-id = funext λ x → ap (_ ∘_) (idr _) ∙ idl _
Hom[-,-] .F-∘ (f , h) (f' , h') = funext λ where
  g → (h ∘ h') ∘ g ∘ f' ∘ f ≡⟨ cat! C ⟩
      h ∘ (h' ∘ g ∘ f') ∘ f ∎

We also can define “partially applied” versions of the hom functor:

Hom[_,-] : Ob → Functor C (Sets h)
Hom[ x ,-] .F₀ y = el (Hom x y) (Hom-set x y)
Hom[ x ,-] .F₁ f g = f ∘ g
Hom[ x ,-] .F-id = funext (λ f → idl f)
Hom[ x ,-] .F-∘ f g = funext λ h → sym (assoc f g h)

The Yoneda embedding🔗

Abstractly and nonsensically, one could say that the Yoneda embedding よ is the exponential transpose of flipping the Hom[-,-] bifunctor. However, this construction generates awful terms, so in the interest of computational efficiency we build up the functor explicitly.

module _ where private
  よ : Functor C (Cat[ C ^op , Sets h ])
  よ = Curry Flip where
    open import
      Cat.Functor.Bifunctor {C = C ^op} {D = C} {E = Sets h} Hom[-,-]

We can describe the object part of this functor as taking an object $c$ to the functor $Hom (-, c)$ of map into $c,$ with the transformation $Hom (x, y) \to Hom (x, z)$ given by precomposition.

よ₀ : Ob → Functor (C ^op) (Sets h)
よ₀ c .F₀ x    = el (Hom x c) (Hom-set _ _)
よ₀ c .F₁ f    = _∘ f
よ₀ c .F-id    = funext idr
よ₀ c .F-∘ f g = funext λ h → assoc _ _ _

We also define a synonym for よ₀ to better line up with the covariant direction.

Hom[-,_] : Ob → Functor (C ^op) (Sets h)
Hom[-,_] x = よ₀ x

The morphism part takes a map $f$ to the transformation given by postcomposition; This is natural because we must show $f \circ x \circ g = (f \circ x) \circ g,$ which is given by associativity in $C .$

よ₁ : Hom a b → よ₀ a => よ₀ b
よ₁ f .η _ g            = f ∘ g
よ₁ f .is-natural x y g = funext λ x → assoc f x g

The other category laws from $C$ ensure that this assignment of natural transformations is indeed functorial:

よ : Functor C Cat[ C ^op , Sets h ]
よ .F₀      = よ₀
よ .F₁      = よ₁
よ .F-id    = ext λ _ g → idl g
よ .F-∘ f g = ext λ _ h → sym (assoc f g h)

The morphism mapping よ₁ 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 isom where
  open is-iso

  isom : is-iso よ₁
  isom .inv nt = nt .η _ id
  isom .rinv nt = ext λ c g →
    happly (sym (nt .is-natural _ _ _)) _ ∙ ap (nt .η c) (idl g)
  isom .linv _ = idr _

The covariant yoneda embedding🔗

One common point of confusion is why category theorists prefer presheaves over covariant functors into $Sets .$ One key reason is that the yoneda embedding into presheaves is covariant, whereas the embedding into functors $C \to Sets$ is contravariant. This makes the covariant yoneda embedding much less pleasant to work with, though we define it anyways for posterity.

よcov₁ : Hom a b → Hom-from b => Hom-from a
よcov₁ f .η _ g = g ∘ f
よcov₁ f .is-natural x y g = funext λ x → sym (assoc g x f)

よcov : Functor (C ^op) Cat[ C , Sets h ]
よcov .F₀ = Hom-from
よcov .F₁ = よcov₁
よcov .F-id = ext λ _ g → idr g
よcov .F-∘ f g = ext λ _ h → (assoc h g f)

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

よcov-is-fully-faithful : is-fully-faithful よcov
よcov-is-fully-faithful = is-iso→is-equiv isom where
  open is-iso

  isom : is-iso よcov₁
  isom .inv nt = nt .η _ id
  isom .rinv nt = ext λ c g →
    sym (nt .is-natural _ _ _) $ₚ _ ∙ ap (nt .η c) (idr g)
  isom .linv _ = idl _