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\hom-sets in a Precategory C\ca{C} is a functor, specifically a bifunctor from Cop×CatC\ca{C}\op \times_\cat \ca{C} to Sets\sets. The action of (f,h)(f, h) on a morphism gg is given by hgfh \circ g \circ f; Since ff is acting by precomposition, the first coordinate is contravariant (Cop\ca{C}\op).

Hom[-,-] : Functor ((C ^op) ×Cat C) (Sets h)
Hom[-,-] .F₀ (a , b) = 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 ≡⟨ solve 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 = 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 cc to the functor hom(,c)\hom(-,c) of map into cc, with the transformation hom(x,y)hom(x,z)\hom(x,y) \to \hom(x,z) given by precomposition.

よ₀ : Ob  Functor (C ^op) (Sets h)
よ₀ c .F₀ x    = 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 ff to the transformation given by postcomposition; This is natural because we must show fxg=(fx)gf \circ x \circ g = (f \circ x) \circ g, which is given by associativity in CC.

よ₁ : 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 C\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
    module P = Functor P

  open El C P
  open Element
  open Element-hom

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

This is done by projecting out of P\int P into C\ca{C} via the canonical projection, and then embedding C\ca{C} into the category of presheaves over C\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)px : P(X). Then, to construct the injection map, we can just use the (contravariant) functorial action of PP to take a px:P(X)px : P(X) and a f:Hom(A,X)f : Hom(A, X) to a P(A)P(A). This map is natural by functoriality of PP.

  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 PP 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
      module K = Cocone K
      module  = Precategory 
      module Reassemble = Cocone Reassemble
      open Cocone-hom

We start by constructing the universal map from PP into the coapex of some other cocone KK. 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 P\int P, and then apply the function we construct to the identity morphism. Naturality follows from the fact that KK is a cocone, and the components of KK 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 KK. 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)\psh(C), in that if a pair f,gf, g of natural transformations that agrees on all representables, then f=gf = g all along.

  module _ {Y} (f : P => Y) where
      module Y = Functor Y
      open Cocone

The first thing we prove is that any map PYP \To Y of presheaves expresses YY as a cocone over (πP)\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{id} is initial the coslice category under PP.

    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:XYf, g : X \To Y are two maps such that, for every map with representable domain h:(A)Xh : \yo(A) \to X, fh=ghfh = gh, then f=gf = g. The quantifier structure of this sentence is a bit funky, so watch out for the formalisation below:

    : {f g : X => Y}
     (  {A : Ob} (h : よ₀ A => X)  f PSh.∘ h  g PSh.∘ h )
     f  g

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

The construction Map→cocone-under lets us express YY as a cocone under (πX)\yo (\pi X) in a way that ff becomes a cocone homomorphism XYX \to Y; The condition that gg agrees with ff on all generalised elements with representable domains ensures that gg is also a cocone homomorphism XYX \to Y; But XX is initial, so f=gf = 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:XYf, g : X \to Y in C\ca{C} extend to maps (f),(g):(X)(Y)\yo(f), \yo(g) : \yo(X) \to \yo(Y), and the functor ()\yo(-) is fully faithful, two maps in C\ca{C} are equal iff. they agree on all generalised elements:

private module _ where private
    :  {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:

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