Merge branch 'master' into functoriality-pullback-hom

UniMath · Oct 27, 2024 · a4c46f4 · a4c46f4
2 parents 07e46dc + 6901252
commit a4c46f4
Show file tree

Hide file tree

Showing 47 changed files with 2,236 additions and 215 deletions.
diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md
@@ -303,7 +303,7 @@ below to ensure a smooth setup and workflow. Also, please make sure to follow
 our [coding style](CODINGSTYLE.md) and
 [design principles](DESIGN-PRINCIPLES.md).
 
-### <a name="pre-commit-hooks"></a>Pre-commit hooks and Python dependencies
+### Pre-commit hooks and Python dependencies {#pre-commit-hooks}
 
 The agda-unimath library includes [pre-commit](https://pre-commit.com/) hooks
 that enforce [basic formatting rules](CONTRIBUTING.md). These will inform you of
@@ -333,7 +333,7 @@ Keep in mind that `pre-commit` is also a part of the Continuous Integration
 (CI), so any PR that violates the enforced conventions will be automatically
 blocked from merging.
 
-### <a name="build-website"></a>Building and viewing the website locally
+### Building and viewing the website locally {#build-website}
 
 The build process for the website uses the
 [Rust language](https://www.rust-lang.org/)'s package manager `cargo`. To

diff --git a/references.bib b/references.bib
@@ -1,3 +1,15 @@
+@online{1000+theorems,
+  title  = {1000+ theorems},
+  author = {Freek Wiedijk},
+  url    = {https://1000-plus.github.io/}
+}
+
+@online{100theorems,
+  title  = {Formalizing 100 Theorems},
+  author = {Freek Wiedijk},
+  url    = {https://www.cs.ru.nl/~freek/100/}
+}
+
 @article{AKS15,
   title       = {Univalent Categories and the {{Rezk}} Completion},
   author      = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
@@ -16,6 +28,22 @@ @article{AKS15
   langid      = {english}
 }
 
+@article{AL19,
+  title       = {Displayed Categories},
+  author      = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter},
+  doi         = {10.23638/LMCS-15(1:20)2019},
+  journal     = {{Logical Methods in Computer Science}},
+  volume      = {15},
+  issue       = {1},
+  year        = {2019},
+  month       = {03},
+  keywords    = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1},
+  eprint      = {1705.04296},
+  eprinttype  = {arxiv},
+  eprintclass = {math},
+  langid      = {english}
+}
+
 @online{BCDE21,
   title  = {Free groups in HoTT/UF in Agda},
   author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín},
@@ -69,7 +97,7 @@ @book{BSCS05
   langid    = {hungarian}
 }
 
-@online{BvDR18,
+@inproceedings{BvDR18,
   title       = {Higher {{Groups}} in {{Homotopy Type Theory}}},
   author      = {Buchholtz, Ulrik and van Doorn, Floris and Rijke, Egbert},
   date        = {2018-02-12},
@@ -79,8 +107,15 @@ @online{BvDR18
   eprinttype  = {arxiv},
   eprintclass = {cs, math},
   abstract    = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
-  pubstate    = {preprint},
-  keywords    = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic}
+  isbn        = {9781450355834},
+  doi         = {10.1145/3209108.3209150},
+  pages       = {205--214},
+  numpages    = {10},
+  location    = {Oxford, United Kingdom},
+  booktitle   = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
+  address     = {New York, NY, USA},
+  publisher   = {Association for Computing Machinery},
+  series      = {LICS '18}
 }
 
 @article{BW23,
@@ -469,10 +504,12 @@ @misc{Mye21
   primaryclass  = {math.CT}
 }
 
-@online{OEIS,
-  title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}} ({{OEIS}})},
-  organization = {{{OEIS}} Foundation Inc.},
-  url          = {https://oeis.org/}
+@online{oeis,
+  title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}},
+  author       = {OEIS Foundation Inc.},
+  date         = {1996},
+  url          = {https://oeis.org},
+  howpublished = {website},
 }
 
 @book{Rie17,

diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
@@ -38,11 +38,13 @@ open import category-theory.coproducts-in-precategories public
 open import category-theory.cores-categories public
 open import category-theory.cores-precategories public
 open import category-theory.coslice-precategories public
+open import category-theory.dependent-composition-operations-over-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public
 open import category-theory.dependent-products-of-precategories public
 open import category-theory.discrete-categories public
+open import category-theory.displayed-precategories public
 open import category-theory.embedding-maps-precategories public
 open import category-theory.embeddings-precategories public
 open import category-theory.endomorphisms-in-categories public

diff --git a/src/category-theory/dependent-composition-operations-over-precategories.lagda.md b/src/category-theory/dependent-composition-operations-over-precategories.lagda.md
@@ -0,0 +1,269 @@
+# Dependent composition operations over precategories
+
+```agda
+module category-theory.dependent-composition-operations-over-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.composition-operations-on-binary-families-of-sets
+open import category-theory.nonunital-precategories
+open import category-theory.precategories
+open import category-theory.set-magmoids
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-identifications
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.iterated-dependent-product-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.transport-along-identifications
+open import foundation.truncated-types
+open import foundation.truncation-levels
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a [precategory](category-theory.precategories.md) `C`, a
+{{#concept "dependent composition structure" Disambiguation="over a precategory"}}
+`D` over `C` is a family of types `obj D` over `obj C` and a family of
+_hom-[sets](foundation-core.sets.md)_
+
+```text
+hom D : hom C x y → obj D x → obj D y → Set
+```
+
+for every pair `x y : obj C`, equipped with a
+{{#concept "dependent composition operation" Disambiguation="over a precategory" Agda=dependent-composition-operation-Precategory}}
+
+```text
+  comp D : hom D g y' z' → hom D f x' y' → hom D (g ∘ f) x' z'.
+```
+
+## Definitions
+
+### The type of dependent composition operations over a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  dependent-composition-operation-Precategory :
+    { l3 l4 : Level}
+    ( obj-D : obj-Precategory C → UU l3) →
+    ( hom-set-D :
+      {x y : obj-Precategory C}
+      (f : hom-Precategory C x y)
+      (x' : obj-D x) (y' : obj-D y) → Set l4) →
+      UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  dependent-composition-operation-Precategory obj-D hom-set-D =
+    {x y z : obj-Precategory C}
+    (g : hom-Precategory C y z) (f : hom-Precategory C x y) →
+    {x' : obj-D x} {y' : obj-D y} {z' : obj-D z} →
+    (g' : type-Set (hom-set-D g y' z')) (f' : type-Set (hom-set-D f x' y')) →
+    type-Set (hom-set-D (comp-hom-Precategory C g f) x' z')
+```
+
+### The predicate of being associative on dependent composition operations over a precategory
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2)
+  ( obj-D : obj-Precategory C → UU l3)
+  ( hom-set-D :
+    {x y : obj-Precategory C}
+    (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4)
+  ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D)
+  where
+
+  is-associative-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-associative-dependent-composition-operation-Precategory =
+    {x y z w : obj-Precategory C}
+    (h : hom-Precategory C z w)
+    (g : hom-Precategory C y z)
+    (f : hom-Precategory C x y)
+    {x' : obj-D x} {y' : obj-D y} {z' : obj-D z} {w' : obj-D w}
+    (h' : type-Set (hom-set-D h z' w'))
+    (g' : type-Set (hom-set-D g y' z'))
+    (f' : type-Set (hom-set-D f x' y')) →
+    dependent-identification
+      ( λ i → type-Set (hom-set-D i x' w'))
+      ( associative-comp-hom-Precategory C h g f)
+      ( comp-hom-D (comp-hom-Precategory C h g) f (comp-hom-D h g h' g') f')
+      ( comp-hom-D h (comp-hom-Precategory C g f) h' (comp-hom-D g f g' f'))
+
+  is-prop-is-associative-dependent-composition-operation-Precategory :
+    is-prop is-associative-dependent-composition-operation-Precategory
+  is-prop-is-associative-dependent-composition-operation-Precategory =
+    is-prop-iterated-implicit-Π 4
+      ( λ x y z w →
+        is-prop-iterated-Π 3
+          ( λ h g f →
+            is-prop-iterated-implicit-Π 4
+              ( λ x' y' z' w' →
+                is-prop-iterated-Π 3
+                  ( λ h' g' f' →
+                    is-set-type-Set
+                      ( hom-set-D
+                        ( comp-hom-Precategory C h (comp-hom-Precategory C g f))
+                        ( x')
+                        ( w'))
+                      ( tr
+                        ( λ i → type-Set (hom-set-D i x' w'))
+                        ( associative-comp-hom-Precategory C h g f)
+                        ( comp-hom-D
+                          ( comp-hom-Precategory C h g)
+                          ( f)
+                          ( comp-hom-D h g h' g')
+                          ( f')))
+                      ( comp-hom-D
+                        ( h)
+                        ( comp-hom-Precategory C g f)
+                        ( h')
+                        ( comp-hom-D g f g' f'))))))
+
+  is-associative-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-associative-prop-dependent-composition-operation-Precategory =
+    is-associative-dependent-composition-operation-Precategory
+  pr2 is-associative-prop-dependent-composition-operation-Precategory =
+    is-prop-is-associative-dependent-composition-operation-Precategory
+```
+
+### The predicate of being unital on dependent composition operations over a precategory
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2)
+  ( obj-D : obj-Precategory C → UU l3)
+  ( hom-set-D :
+    {x y : obj-Precategory C}
+    (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4)
+  ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D)
+  ( id-hom-D :
+    {x : obj-Precategory C} (x' : obj-D x) →
+    type-Set (hom-set-D (id-hom-Precategory C {x}) x' x'))
+  where
+
+  is-left-unit-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-left-unit-dependent-composition-operation-Precategory =
+    {x y : obj-Precategory C} (f : hom-Precategory C x y)
+    {x' : obj-D x} {y' : obj-D y} (f' : type-Set (hom-set-D f x' y')) →
+    dependent-identification
+      ( λ i → type-Set (hom-set-D i x' y'))
+      ( left-unit-law-comp-hom-Precategory C f)
+      ( comp-hom-D (id-hom-Precategory C) f (id-hom-D y') f')
+      ( f')
+
+  is-prop-is-left-unit-dependent-composition-operation-Precategory :
+    is-prop is-left-unit-dependent-composition-operation-Precategory
+  is-prop-is-left-unit-dependent-composition-operation-Precategory =
+    is-prop-iterated-implicit-Π 2
+      ( λ x y →
+        is-prop-Π
+          ( λ f →
+            is-prop-iterated-implicit-Π 2
+              ( λ x' y' →
+                is-prop-Π
+                  ( λ f' →
+                    is-set-type-Set
+                      ( hom-set-D f x' y')
+                      ( tr
+                        ( λ i → type-Set (hom-set-D i x' y'))
+                        ( left-unit-law-comp-hom-Precategory C f)
+                        ( comp-hom-D (id-hom-Precategory C) f (id-hom-D y') f'))
+                      ( f')))))
+
+  is-left-unit-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-left-unit-prop-dependent-composition-operation-Precategory =
+    is-left-unit-dependent-composition-operation-Precategory
+  pr2 is-left-unit-prop-dependent-composition-operation-Precategory =
+    is-prop-is-left-unit-dependent-composition-operation-Precategory
+
+  is-right-unit-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-right-unit-dependent-composition-operation-Precategory =
+    {x y : obj-Precategory C} (f : hom-Precategory C x y)
+    {x' : obj-D x} {y' : obj-D y} (f' : type-Set (hom-set-D f x' y')) →
+    dependent-identification
+      ( λ i → type-Set (hom-set-D i x' y'))
+      ( right-unit-law-comp-hom-Precategory C f)
+      ( comp-hom-D f (id-hom-Precategory C) f' (id-hom-D x'))
+      ( f')
+
+  is-prop-is-right-unit-dependent-composition-operation-Precategory :
+    is-prop is-right-unit-dependent-composition-operation-Precategory
+  is-prop-is-right-unit-dependent-composition-operation-Precategory =
+    is-prop-iterated-implicit-Π 2
+      ( λ x y →
+        is-prop-Π
+          ( λ f →
+            is-prop-iterated-implicit-Π 2
+              ( λ x' y' →
+                is-prop-Π
+                  ( λ f' →
+                    is-set-type-Set
+                      ( hom-set-D f x' y')
+                      ( tr
+                        ( λ i → type-Set (hom-set-D i x' y'))
+                        ( right-unit-law-comp-hom-Precategory C f)
+                        ( comp-hom-D f (id-hom-Precategory C) f' (id-hom-D x')))
+                      ( f')))))
+
+  is-right-unit-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-right-unit-prop-dependent-composition-operation-Precategory =
+    is-right-unit-dependent-composition-operation-Precategory
+  pr2 is-right-unit-prop-dependent-composition-operation-Precategory =
+    is-prop-is-right-unit-dependent-composition-operation-Precategory
+
+  is-unit-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-unit-dependent-composition-operation-Precategory =
+    ( is-left-unit-dependent-composition-operation-Precategory) ×
+    ( is-right-unit-dependent-composition-operation-Precategory)
+
+  is-prop-is-unit-dependent-composition-operation-Precategory :
+    is-prop is-unit-dependent-composition-operation-Precategory
+  is-prop-is-unit-dependent-composition-operation-Precategory =
+    is-prop-product
+      ( is-prop-is-left-unit-dependent-composition-operation-Precategory)
+      ( is-prop-is-right-unit-dependent-composition-operation-Precategory)
+
+  is-unit-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-unit-prop-dependent-composition-operation-Precategory =
+    is-unit-dependent-composition-operation-Precategory
+  pr2 is-unit-prop-dependent-composition-operation-Precategory =
+    is-prop-is-unit-dependent-composition-operation-Precategory
+
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2)
+  ( obj-D : obj-Precategory C → UU l3)
+  ( hom-set-D :
+    {x y : obj-Precategory C}
+    (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4)
+  ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D)
+  where
+
+  is-unital-dependent-composition-operation-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-unital-dependent-composition-operation-Precategory =
+    Σ ( {x : obj-Precategory C} (x' : obj-D x) →
+        type-Set (hom-set-D (id-hom-Precategory C {x}) x' x'))
+      ( is-unit-dependent-composition-operation-Precategory C
+          obj-D hom-set-D comp-hom-D)
+```
+
+## See also
+
+- [Displayed precategories](category-theory.displayed-precategories.md)