Yoneda (#632)

In two separate files we

(i) defined covariant representable functors for precategories and
representable natural transformations between them
(ii) proved the Yoneda lemma for precategories.

---------

Co-authored-by: emilyriehl <emilyriehl@math.jhu.edu>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

src/category-theory.lagda.md

@@ -67,7 +67,9 @@ open import category-theory.pregroupoids public
 open import category-theory.products-of-precategories public
 open import category-theory.products-precategories public
 open import category-theory.pullbacks-precategories public
+open import category-theory.representable-functors-precategories public
 open import category-theory.sieves-categories public
 open import category-theory.slice-precategories public
 open import category-theory.terminal-objects-precategories public
+open import category-theory.yoneda-lemma-precategories public
 ```

src/category-theory/representable-functors-precategories.lagda.md

@@ -0,0 +1,67 @@
+# Representable functors between precategories
+
+```agda
+module category-theory.representable-functors-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.functors-precategories
+open import category-theory.natural-transformations-precategories
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a precategory `C` and an object `c`, there is a functor from `C` to the
+precategory of Sets represented by `c` that:
+
+- sends an object `x` of `C` to the set `hom c x` and
+- sends a morphism `g : hom x y` of `C` to the function `hom c x → hom c y`
+  defined by postcomposition with `g`.
+
+The functoriality axioms follow, by function extensionality, from associativity
+and the left unit law for the precategory `C`.
+
+## Definition
+
+```agda
+rep-functor-Precategory :
+  {l1 l2 : Level} (C : Precategory l1 l2) (c : obj-Precategory C) →
+  functor-Precategory C (Set-Precategory l2)
+pr1 (rep-functor-Precategory C c) = hom-Precategory C c
+pr1 (pr2 (rep-functor-Precategory C c)) g = postcomp-hom-Precategory C g c
+pr1 (pr2 (pr2 (rep-functor-Precategory C c))) h g =
+  eq-htpy (associative-comp-hom-Precategory C h g)
+pr2 (pr2 (pr2 (rep-functor-Precategory C c))) _ =
+  eq-htpy (left-unit-law-comp-hom-Precategory C)
+```
+
+## Natural transformations between representable functors
+
+A morphism `f : hom b c` in a precategory `C` defines a natural transformation
+from the functor represented by `c` to the functor represented by `b`. Its
+components `hom c x → hom b x` are defined by precomposition with `f`.
+
+```agda
+rep-natural-transformation-Precategory :
+  {l1 l2 : Level} (C : Precategory l1 l2) (b c : obj-Precategory C)
+  (f : type-hom-Precategory C b c) →
+  natural-transformation-Precategory
+    ( C)
+    ( Set-Precategory l2)
+    ( rep-functor-Precategory C c)
+    ( rep-functor-Precategory C b)
+pr1 (rep-natural-transformation-Precategory C b c f) =
+  precomp-hom-Precategory C f
+pr2 (rep-natural-transformation-Precategory C b c f) h =
+  eq-htpy (inv-htpy (λ g → associative-comp-hom-Precategory C h g f))
+```

src/category-theory/yoneda-lemma-precategories.lagda.md

@@ -0,0 +1,109 @@
+# Yoneda lemma for precategories
+
+```agda
+module category-theory.yoneda-lemma-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.functors-precategories
+open import category-theory.natural-transformations-precategories
+open import category-theory.precategories
+open import category-theory.representable-functors-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.sets
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a precategory `C`, an object `c`, and a functor `F` from `C` to the
+precategory of Sets, there is an equivalence between the set of natural
+transformations from the functor represented by `c` to `F` and the set `F c`.
+
+More precisely, the Yoneda lemma asserts that the map from the type of natural
+transformations to the type `F c` defined by evaluating the component of the
+natural transformation at the object `c` at the identity arrow on `c` is an
+equivalence.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level} (C : Precategory l1 l1) (c : obj-Precategory C)
+  (F : functor-Precategory C (Set-Precategory l1))
+  where
+
+  yoneda-evid-Precategory :
+    natural-transformation-Precategory
+      ( C)
+      ( Set-Precategory l1)
+      ( rep-functor-Precategory C c)
+      ( F) →
+    type-Set (obj-functor-Precategory C (Set-Precategory l1) F c)
+  yoneda-evid-Precategory α =
+    components-natural-transformation-Precategory
+      ( C)
+      ( Set-Precategory l1)
+      ( rep-functor-Precategory C c)
+      ( F)
+      ( α)
+      ( c)
+      ( id-hom-Precategory C)
+
+  yoneda-extension-Precategory :
+    type-Set (obj-functor-Precategory C (Set-Precategory l1) F c) →
+    natural-transformation-Precategory
+      C (Set-Precategory l1) (rep-functor-Precategory C c) F
+  pr1 (yoneda-extension-Precategory u) x f =
+    hom-functor-Precategory C (Set-Precategory l1) F f u
+  pr2 (yoneda-extension-Precategory u) g =
+    eq-htpy
+      ( λ f →
+        htpy-eq
+          ( inv
+            ( preserves-comp-functor-Precategory C (Set-Precategory l1) F g f))
+          ( u))
+
+  sec-yoneda-evid-Precategory :
+    sec yoneda-evid-Precategory
+  pr1 sec-yoneda-evid-Precategory = yoneda-extension-Precategory
+  pr2 sec-yoneda-evid-Precategory =
+    htpy-eq (preserves-id-functor-Precategory C (Set-Precategory _) F c)
+
+  retr-yoneda-evid-Precategory :
+    retr yoneda-evid-Precategory
+  pr1 retr-yoneda-evid-Precategory = yoneda-extension-Precategory
+  pr2 retr-yoneda-evid-Precategory α =
+    eq-pair-Σ
+      ( eq-htpy
+        ( λ x →
+          eq-htpy
+            ( λ f →
+              htpy-eq ((pr2 α) f) ((id-hom-Precategory C {c})) ∙
+              ap (pr1 α x) (right-unit-law-comp-hom-Precategory C f))))
+      ( eq-is-prop'
+        ( is-prop-is-natural-transformation-Precategory
+          ( C)
+          ( Set-Precategory l1)
+          ( rep-functor-Precategory C c)
+          ( F)
+          ( pr1 α))
+        ( _)
+        ( pr2 α))
+
+  yoneda-lemma-Precategory : is-equiv yoneda-evid-Precategory
+  pr1 yoneda-lemma-Precategory = sec-yoneda-evid-Precategory
+  pr2 yoneda-lemma-Precategory = retr-yoneda-evid-Precategory
+```