open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Diagram.Initial
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Instances.Elements as El
import Cat.Reasoning

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


# The Hom functor🔗

We prove that the assignment of $\hom$-sets in a Precategory $\ca{C}$ is a functor, specifically a bifunctor from $\ca{C}\op \times_\cat \ca{C}$ to $\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 ($\ca{C}\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 $c$ to the functor $\hom(-,c)$ of map into $c$, with the transformation $\hom(x,y) \to \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 $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 $\ca{C}$ ensure that this assigment 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 Coyoneda Lemma🔗

The Coyoneda lemma is, like its dual, a statement about presheaves. It states that “every presheaf is a colimit of representables”, which, in less abstract terms, means that every presheaf arises as some way of gluing together a bunch of (things isomorphic to) hom functors!

module _ (P : Functor (C ^op) (Sets h)) where
private
module P = Functor P

open El C P
open Element
open Element-hom


We start by fixing some presheaf $P$, and constructing a Cocone whose coapex is $P$. This involves a clever choice of diagram category: specifically, the category of elements of $P$. This may seem like a somewhat odd choice, but recall that the data contained in $\int P$ is the same data as $P$, just melted into a soup of points. The cocone we construct will then glue all those points back together into $P$.

This is done by projecting out of $\int P$ into $\ca{C}$ via the canonical projection, and then embedding $\ca{C}$ into the category of presheaves over $\ca{C}$ via the yoneda embedding. Concretely, what this diagram gives us is a bunch of copies of the hom functor, one for each $px : P(X)$. Then, to construct the injection map, we can just use the (contravariant) functorial action of $P$ to take a $px : P(X)$ and a $f : Hom(A, X)$ to a $P(A)$. This map is natural by functoriality of $P$.

  Reassemble : Cocone (よ F∘ πₚ)
Reassemble .Cocone.coapex = P
Reassemble .Cocone.ψ x .η y f = P.F₁ f (x .section)
Reassemble .Cocone.ψ x .is-natural y z f =
funext (λ g → happly (P.F-∘ f g) (x .section))
Reassemble .Cocone.commutes {x = x} {y = y} f =
Nat-path λ z → funext λ g →
P.F₁ (f .hom ∘ g) (y .section)      ≡⟨ happly (P.F-∘ g (f .hom)) (y .section) ⟩≡
P.F₁ g (P.F₁ (f .hom) (y .section)) ≡⟨ ap (P.F₁ g) (f .commute) ⟩≡
P.F₁ g (x .section)                 ∎


Now that we’ve constructed a cocone, all that remains is to see that this is a colimiting cocone. Intuitively, it makes sense that Reassemble should be colimiting: all we’ve done is taken all the data associated with $P$ and glued it back together. However, proving this does involve futzing about with various naturality + cocone commuting conditions.

  coyoneda : is-colimit (よ F∘ πₚ) Reassemble
coyoneda K = contr (cocone-hom universal factors) unique
where
module K = Cocone K
module ∫ = Precategory ∫
module Reassemble = Cocone Reassemble
open Cocone-hom


We start by constructing the universal map from $P$ into the coapex of some other cocone $K$. The components of this natural transformation are obtained in a similar manner to the yoneda lemma; we bundle up the data to construct an object of $\int P$, and then apply the function we construct to the identity morphism. Naturality follows from the fact that $K$ is a cocone, and the components of $K$ are natural.

      universal : P => K.coapex
universal .η x px = K.ψ (elem x px) .η x id
universal .is-natural x y f = funext λ px →
K.ψ (elem y (P.F₁ f px)) .η y id        ≡˘⟨ (λ i → K.commutes (induce f px) i .η y id) ⟩≡˘
K.ψ (elem x px) .η y (f ∘ id)           ≡⟨ ap (K.ψ (elem x px) .η y) id-comm ⟩≡
K.ψ (elem x px) .η y (id ∘ f)           ≡⟨ happly (K.ψ (elem x px) .is-natural x y f) id ⟩≡
F₁ K.coapex f (K.ψ (elem x px) .η x id) ∎


Next, we need to show that this morphism factors each of the components of $K$. The tricky bit of the proof here is that we need to use induce to regard f as a morphism in the category of elements.

      factors : ∀ o → universal ∘nt Reassemble.ψ o ≡ K.ψ o
factors o = Nat-path λ x → funext λ f →
K.ψ (elem x (P.F₁ f (o .section))) .η x id ≡˘⟨ (λ i → K.commutes (induce f (o .section)) i .η x id) ⟩≡˘
K.ψ o .η x (f ∘ id)                        ≡⟨ ap (K.ψ o .η x) (idr f) ⟩≡
K.ψ o .η x f ∎


Finally, uniqueness: This just follows by the commuting conditions on α.

      unique : (α : Cocone-hom (よ F∘ πₚ) Reassemble K)
→ cocone-hom universal factors ≡ α
unique α = Cocone-hom-path (よ F∘ πₚ) $Nat-path λ x → funext λ px → K.ψ (elem x px) .η x id ≡˘⟨ (λ i → α .commutes (elem x px) i .η x id) ⟩≡˘ α .hom .η x (Reassemble.ψ (elem x px) .η x id) ≡⟨ ap (α .hom .η x) (happly (P.F-id) px) ⟩≡ α .hom .η x px ∎  And that’s it! The important takeaway here is not the shuffling around of natural transformations required to prove this lemma, but rather the idea that, unlike Humpty Dumpty, if a presheaf falls off a wall, we can put it back together again. An important consequence of being able to disassemble presheaves into colimits of representables is that representables generate $\psh(C)$, in that if a pair $f, g$ of natural transformations that agrees on all representables, then $f = g$ all along.  module _ {Y} (f : P => Y) where private module Y = Functor Y open Cocone  The first thing we prove is that any map $P \To Y$ of presheaves expresses $Y$ as a cocone over $\yo (\pi P)$. The special case Reassemble above is this procedure for the identity map — whence we see that coyoneda is essentially a restatement of the fact that $\id{id}$ is initial the coslice category under $P$.  Map→cocone-under : Cocone (よ F∘ πₚ) Map→cocone-under .coapex = Y Map→cocone-under .ψ (elem ob sect) .η x i = f .η x (P.₁ i sect) Map→cocone-under .ψ (elem ob sect) .is-natural x y h = funext λ a → f .η _ (P.₁ (a ∘ h) sect) ≡⟨ happly (f .is-natural _ _ _) _ ⟩≡ Y.₁ (a ∘ h) (f .η _ sect) ≡⟨ happly (Y.F-∘ _ _) _ ⟩≡ Y.₁ h (Y.₁ a (f .η _ sect)) ≡˘⟨ ap (Y .F₁ h) (happly (f .is-natural _ _ _) _) ⟩≡˘ Y.₁ h (f .η _ (P.₁ a sect)) ∎ Map→cocone-under .commutes {x} {y} o = Nat-path λ i → funext λ a → ap (f .η _)$
P.₁ (o .hom ∘ a) (y .section)     ≡⟨ happly (P.F-∘ _ _) _ ⟩≡
P.₁ a (P.₁ (o .hom) (y .section)) ≡⟨ ap (P.F₁ _) (o .commute) ⟩≡
P.₁ a (x .section)                ∎


We can now prove that, if $f, g : X \To Y$ are two maps such that, for every map with representable domain $h : \yo(A) \to X$, $fh = gh$, then $f = g$. The quantifier structure of this sentence is a bit funky, so watch out for the formalisation below:

  Representables-generate-presheaf
: {f g : X => Y}
→ ( ∀ {A : Ob} (h : よ₀ A => X) → f PSh.∘ h ≡ g PSh.∘ h )
→ f ≡ g


A map $h : \yo(A) \To X$ can be seen as a “generalised element” of $X$, so that the precondition for $f = g$ can be read as “$f$ and $g$ agree for all generalised elements with domain any representable”. The proof is deceptively simple: Since $X$ is a colimit, it is an initial object in the category of cocones under $\yo (\pi X)$.

The construction Map→cocone-under lets us express $Y$ as a cocone under $\yo (\pi X)$ in a way that $f$ becomes a cocone homomorphism $X \to Y$; The condition that $g$ agrees with $f$ on all generalised elements with representable domains ensures that $g$ is also a cocone homomorphism $X \to Y$; But $X$ is initial, so $f = g$!

  Representables-generate-presheaf {f} {g} sep =
ap hom $is-contr→is-prop (coyoneda X (Map→cocone-under X f)) f′ g′ where f′ : Cocone-hom (よ F∘ El.πₚ C X) (Reassemble X) (Map→cocone-under X f) f′ .hom = f f′ .commutes o = Nat-path (λ _ → refl) g′ : Cocone-hom (よ F∘ El.πₚ C X) (Reassemble X) (Map→cocone-under X f) g′ .hom = g g′ .commutes o = Nat-path λ x → ap (λ e → e .η x)$ sym $sep$
NT (λ i a → P.₁ a (o .section)) λ x y h →
funext λ _ → happly (P.F-∘ _ _) _


An immediate consequence is that, since any pair of maps $f, g : X \to Y$ in $\ca{C}$ extend to maps $\yo(f), \yo(g) : \yo(X) \to \yo(Y)$, and the functor $\yo(-)$ is fully faithful, two maps in $\ca{C}$ are equal iff. they agree on all generalised elements:

private module _ where private
よ-cancelr
: ∀ {X Y : Ob} {f g : Hom X Y}
→ (∀ {Z} (h : Hom Z X) → f ∘ h ≡ g ∘ h)
→ f ≡ g
よ-cancelr sep =
fully-faithful→faithful {F = よ} よ-is-fully-faithful \$
Representables-generate-presheaf λ h → Nat-path λ x → funext λ a →
sep (h .η x a)


However note that we have eliminated a mosquito using a low-orbit ion cannon:

よ-cancelr
: ∀ {X Y : Ob} {f g : Hom X Y}
→ (∀ {Z} (h : Hom Z X) → f ∘ h ≡ g ∘ h)
→ f ≡ g
よ-cancelr sep = sym (idr _) ∙ sep id ∙ idr _