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

The Hom functorπŸ”—

We prove that the assignment of Hom\mathbf{Hom}-sets in a Precategory C\mathcal{C} is a functor, specifically a bifunctor from CopΓ—C\mathcal{C}^{\mathrm{op}} \times \mathcal{C} to Sets\mathbf{Sets}. The action of (f,h)(f, h) on a morphism gg is given by h∘g∘fh \circ g \circ f; Since ff is acting by precomposition, the first coordinate is contravariant (Cop\mathcal{C}^{\mathrm{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 cc to the functor Hom(βˆ’,c)\mathbf{Hom}(-,c) of map into cc, with the transformation Hom(x,y)β†’Hom(x,z)\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

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

γ‚ˆβ‚ : 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\mathcal{C} ensure that this assignment of natural transformations is indeed functorial:

γ‚ˆ : Functor C Cat[ C ^op , Sets h ]
γ‚ˆ .Fβ‚€      = γ‚ˆβ‚€
γ‚ˆ .F₁      = γ‚ˆβ‚
γ‚ˆ .F-id    = Nat-path Ξ» _ i g β†’ idl g i
γ‚ˆ .F-∘ f g = Nat-path Ξ» _ i h β†’ assoc f g h (~ i)

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 = Nat-path Ξ» c β†’ funext Ξ» 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\mathbf{Sets}. One key reason is that the yoneda embedding into presheaves is covariant, whereas the embedding into functors C→Sets\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 = Nat-path Ξ» _ β†’ funext Ξ» g β†’ idr g
γ‚ˆcov .F-∘ f g = Nat-path Ξ» _ β†’ funext Ξ» 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 = Nat-path Ξ» c β†’ funext Ξ» g β†’
    sym (nt .is-natural _ _ _) $β‚š _ βˆ™ ap (nt .Ξ· c) (idr g)
  isom .linv _ = idl _