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 ${\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}}}}$).

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


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 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 $\mathcal{C}$ via the canonical projection, and then embedding $\mathcal{C}$ into the category of presheaves over $\mathcal{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 ${{\mathrm{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 {\Rightarrow}Y$ of presheaves expresses $Y$ as a cocone over ${γ}(\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 ${{\mathrm{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 {\Rightarrow}Y$ are two maps such that, for every map with representable domain $h : {γ}(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 : {γ}(A) {\Rightarrow}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 ${γ}(\pi X)$.

The construction Mapβcocone-under lets us express $Y$ as a cocone under ${γ}(\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 β sym (sep$
NT (Ξ» i a β P.β a (o .section)) Ξ» x y h β
funext Ξ» a β P.F-β _ _ $β o .section) Ξ·β x  An immediate consequence is that, since any pair of maps $f, g : X \to Y$ in $\mathcal{C}$ extend to maps ${γ}(f), {γ}(g) : {γ}(X) \to {γ}(Y)$, and the functor ${γ}(-)$ is fully faithful, two maps in $\mathcal{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 _