Yoneda's lemma for categories (UniMath#783)

fredrik-bakke · Sep 17, 2023 · 539174a · 539174a
1 parent 0106784
commit 539174a
Show file tree

Hide file tree

Showing 9 changed files with 484 additions and 117 deletions.
diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
@@ -77,9 +77,11 @@ open import category-theory.pregroupoids public
 open import category-theory.products-in-precategories public
 open import category-theory.products-of-precategories public
 open import category-theory.pullbacks-in-precategories public
+open import category-theory.representable-functors-categories public
 open import category-theory.representable-functors-precategories public
 open import category-theory.sieves-in-categories public
 open import category-theory.slice-precategories public
 open import category-theory.terminal-objects-in-precategories public
+open import category-theory.yoneda-lemma-categories public
 open import category-theory.yoneda-lemma-precategories public
 ```
diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md
@@ -118,6 +118,26 @@ module _
   is-category-Category = pr2 C
 ```
 
+### Precomposition by a morphism
+
+```agda
+precomp-hom-Category :
+  {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
+  (f : type-hom-Category C x y) (z : obj-Category C) →
+  type-hom-Category C y z → type-hom-Category C x z
+precomp-hom-Category C = precomp-hom-Precategory (precategory-Category C)
+```
+
+### Postcomposition by a morphism
+
+```agda
+postcomp-hom-Category :
+  {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
+  (f : type-hom-Category C x y) (z : obj-Category C) →
+  type-hom-Category C z x → type-hom-Category C z y
+postcomp-hom-Category C = postcomp-hom-Precategory (precategory-Category C)
+```
+
 ## Properties
 
 ### The objects in a category form a 1-type

diff --git a/src/category-theory/natural-transformations-categories.lagda.md b/src/category-theory/natural-transformations-categories.lagda.md
@@ -11,15 +11,22 @@ open import category-theory.categories
 open import category-theory.functors-categories
 open import category-theory.natural-transformations-precategories
 
+open import foundation.embeddings
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
 open import foundation.universe-levels
 ```
 
 </details>
 
 ## Idea
 
-A natural transformation between functors on categories is a natural
-transformation between the functors on the underlying precategories.
+A **natural transformation** between
+[functors on categories](category-theory.functors-categories.md) is a
+[natural transformation](category-theory.natural-transformations-precategories.md)
+between the [functors](category-theory.functors-precategories.md) on the
+underlying [precategories](category-theory.precategories.md).
 
 ## Definition
 
@@ -63,4 +70,162 @@ module _
       ( precategory-Category D)
       ( F)
       ( G)
+
+  coherence-square-natural-transformation-Category :
+    (γ : natural-transformation-Category) →
+    is-natural-transformation-Category
+      ( components-natural-transformation-Category γ)
+  coherence-square-natural-transformation-Category =
+    coherence-square-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+```
+
+## Composition and identity of natural transformations
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Category l1 l2) (D : Category l3 l4)
+  where
+
+  id-natural-transformation-Category :
+    (F : functor-Category C D) → natural-transformation-Category C D F F
+  id-natural-transformation-Category =
+    id-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+
+  comp-natural-transformation-Category :
+    (F G H : functor-Category C D) →
+    natural-transformation-Category C D G H →
+    natural-transformation-Category C D F G →
+    natural-transformation-Category C D F H
+  comp-natural-transformation-Category =
+    comp-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+```
+
+## Properties
+
+### That a family of morphisms is a natural transformation is a proposition
+
+This follows from the fact that the hom-types are
+[sets](foundation-core.sets.md).
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Category l1 l2)
+  (D : Category l3 l4)
+  (F G : functor-Category C D)
+  where
+
+  is-prop-is-natural-transformation-Category :
+    ( γ :
+      (x : obj-Category C) →
+      type-hom-Category D
+        ( obj-functor-Category C D F x)
+        ( obj-functor-Category C D G x)) →
+    is-prop (is-natural-transformation-Category C D F G γ)
+  is-prop-is-natural-transformation-Category =
+    is-prop-is-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+
+  is-natural-transformation-Category-Prop :
+    ( γ :
+      (x : obj-Category C) →
+      type-hom-Category D
+        ( obj-functor-Category C D F x)
+        ( obj-functor-Category C D G x)) →
+    Prop (l1 ⊔ l2 ⊔ l4)
+  is-natural-transformation-Category-Prop =
+    is-natural-transformation-Precategory-Prop
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+
+  components-natural-transformation-Category-is-emb :
+    is-emb (components-natural-transformation-Category C D F G)
+  components-natural-transformation-Category-is-emb =
+    components-natural-transformation-Precategory-is-emb
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+
+  natural-transformation-Category-Set :
+    Set (l1 ⊔ l2 ⊔ l4)
+  natural-transformation-Category-Set =
+    natural-transformation-Precategory-Set
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+```
+
+### Category laws for natural transformations
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Category l1 l2) (D : Category l3 l4)
+  where
+
+  extensionality-natural-transformation-Category :
+    (F G : functor-Category C D)
+    (α β : natural-transformation-Category C D F G) →
+    ( components-natural-transformation-Category C D F G α ＝
+      components-natural-transformation-Category C D F G β) →
+    α ＝ β
+  extensionality-natural-transformation-Category F G =
+    extensionality-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+      ( G)
+
+  right-unit-law-comp-natural-transformation-Category :
+    {F G : functor-Category C D}
+    (α : natural-transformation-Category C D F G) →
+    comp-natural-transformation-Category C D F F G α
+      ( id-natural-transformation-Category C D F) ＝ α
+  right-unit-law-comp-natural-transformation-Category {F} {G} =
+    right-unit-law-comp-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      { F}
+      { G}
+
+  left-unit-law-comp-natural-transformation-Category :
+    {F G : functor-Category C D}
+    (α : natural-transformation-Category C D F G) →
+    comp-natural-transformation-Category C D F G G
+      ( id-natural-transformation-Category C D G) α ＝ α
+  left-unit-law-comp-natural-transformation-Category {F} {G} =
+    left-unit-law-comp-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      { F}
+      { G}
+
+  associative-comp-natural-transformation-Category :
+    {F G H I : functor-Category C D}
+    (α : natural-transformation-Category C D F G)
+    (β : natural-transformation-Category C D G H)
+    (γ : natural-transformation-Category C D H I) →
+    comp-natural-transformation-Category C D F G I
+      ( comp-natural-transformation-Category C D G H I γ β) α ＝
+    comp-natural-transformation-Category C D F H I γ
+      ( comp-natural-transformation-Category C D F G H β α)
+  associative-comp-natural-transformation-Category {F} {G} {H} {I} =
+    associative-comp-natural-transformation-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      { F} {G} {H} {I}
 ```