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}$-sets in a Precategory $\mathcal{C}$ is a functor, specifically a bifunctor from $\mathcal{C}^{\mathrm{op}} \times \mathcal{C}$ to $\mathbf{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 ($\mathcal{C}^{\mathrm{op}}$).

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 $c$ to the functor $\mathbf{Hom}(-,c)$ of map into $c$, 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$, 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 $\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 $\mathbf{Sets}$. 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 = 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 _