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 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 (

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 β

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

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 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 _

γ-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 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 _

γcov-is-faithful : is-faithful γcov
γcov-is-faithful = ffβfaithful {F = γcov} (γcov-is-fully-faithful)