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 h∘g∘fh \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 f∘x∘g=(f∘x)∘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 Pβ‡’YP \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:Xβ‡’Yf, 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 Xβ†’YX \to Y; The condition that gg agrees with ff on all generalised elements with representable domains ensures that gg is also a cocone homomorphism Xβ†’YX \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:Xβ†’Yf, 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 _