open import Cat.Functor.Properties
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🔗

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

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

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 ∎

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 $\mathbf{Hom}(-,c)$ of map into $c\text{,}$ with the transformation $\mathbf{Hom}(x,y)\to \mathbf{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

Hom-from : Ob → Functor C (Sets h)
Hom-from = Hom[_,-]

Hom-into : Ob → Functor (C ^op) (Sets h)
Hom-into = よ₀

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\text{,}$ which is given by associativity in $C\text{.}$

よ₁ : 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 $\mathcal{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 _

よ-is-faithful : is-faithful よ
よ-is-faithful = fully-faithful→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 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₁ : 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 _

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