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

The Hom functorπŸ”—

We prove that the assignment of in a Precategory is a functor, specifically a bifunctor from to The action of on a morphism is given by Since is acting by precomposition, the first coordinate is contravariant (

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 to the functor of map into with the transformation 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 to the transformation given by postcomposition; This is natural because we must show which is given by associativity in

γ‚ˆβ‚ : 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 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 One key reason is that the yoneda embedding into presheaves is covariant, whereas the embedding into functors 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 _