Rename wild higher categories (#1233)

This PR renames "noncoherent wild higher categories" to "noncoherent ω-categories". The latter is both shorter and more descriptive. Additionally, this PR renames "isomorphisms in ω-categories" to "coinductive isomorphisms in ω-categories", as the concept that was defined is strictly weaker than the proper definition of an isomorphism in an ω-category, as discussed with @VojtechStep. Co-authored-by: VojtechStep [[email protected]](mailto:[email protected])
UniMath · Feb 4, 2025 · da15ec1 · da15ec1
1 parent 1e542d8
commit da15ec1
Show file tree

Hide file tree

Showing 24 changed files with 2,552 additions and 2,498 deletions.
diff --git a/references.bib b/references.bib
@@ -40,7 +40,7 @@ @misc{Anel24
 
 @article{AL19,
   title       = {Displayed Categories},
-  author      = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter},
+  author      = {Ahrens, Benedikt and LeFanu Lumsdaine, Peter},
   doi         = {10.23638/LMCS-15(1:20)2019},
   journal     = {{Logical Methods in Computer Science}},
   volume      = {15},
@@ -55,14 +55,14 @@ @article{AL19
 }
 
 @misc{Awodey22,
-       author = {{Awodey}, Steve},
-        title = "{On Hofmann-Streicher universes}",
-     keywords = {Mathematics - Category Theory, Mathematics - Logic},
-         year = 2022,
-        month = may,
-archivePrefix = {arXiv},
-       eprint = {2205.10917},
- primaryClass = {math.CT}
+  author        = {Awodey, Steve},
+  title         = {{On Hofmann-Streicher universes}},
+  keywords      = {Mathematics - Category Theory, Mathematics - Logic},
+  year          = 2022,
+  month         = may,
+  archiveprefix = {arXiv},
+  eprint        = {2205.10917},
+  primaryclass  = {math.CT}
 }
 
 @online{BCDE21,
@@ -167,6 +167,22 @@ @article{Cantor1890/91
   langid  = {german}
 }
 
+@article{Cheng07,
+  title    = {An ω-Category with All {{Duals}} Is an ω-Groupoid},
+  author   = {Cheng, Eugenia},
+  date     = {2007-08-01},
+  year     = {2007},
+  month    = {08},
+  journal  = {Applied Categorical Structures},
+  volume   = {15},
+  number   = {4},
+  pages    = {439--453},
+  issn     = {1572-9095},
+  doi      = {10.1007/s10485-007-9081-8},
+  abstract = {We make a definition of ω-precategory which should underlie any definition of weak ω-category. We make a precise definition of pseudo-invertible cells in this setting. We show that in an ω-precategory with all weak duals, every cell is pseudo-invertible. We deduce that in any “sensible” theory of ω-categories, an ω-category with all weak duals is an ω-groupoid. We discuss various examples and open questions involving higher-dimensional tangles and cobordisms.},
+  langid   = {english}
+}
+
 @unpublished{Cisinski24,
   title  = {Formalization of higher categories},
   author = {Denis-Charles Cisinski, Bastiaan Cnossen, Kim Nguyen and Tashi Walde},
@@ -566,21 +582,21 @@ @online{oeis
   date         = {1996},
   citeas       = {OEIS},
   url          = {https://oeis.org},
-  howpublished = {website},
+  howpublished = {website}
 }
 
 @phdthesis{Qui16,
-  title = {Lawvere–Tierney sheafification in Homotopy Type Theory},
-  author = {Quirin, Kevin},
-  url = {https://kevinquirin.github.io/thesis/main.pdf},
-  year = {2016},
-  month = dec,
-  number = {2016EMNA0298},
-  school = {École des Mines de Nantes},
+  title    = {Lawvere–Tierney sheafification in Homotopy Type Theory},
+  author   = {Quirin, Kevin},
+  url      = {https://kevinquirin.github.io/thesis/main.pdf},
+  year     = {2016},
+  month    = dec,
+  number   = {2016EMNA0298},
+  school   = {École des Mines de Nantes},
   abstract = {The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere–Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere–Tierney sheafification functor, which is the main theorem presented in this thesis.
-  To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities.
-  Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].},
-  langid = {english}
+              To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities.
+              Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].},
+  langid   = {english}
 }
 
 @book{Rie17,

diff --git a/src/foundation/globular-type-of-dependent-functions.lagda.md b/src/foundation/globular-type-of-dependent-functions.lagda.md
@@ -33,10 +33,10 @@ globular structure on dependent function types.
 The globular type of dependent functions of a type family `B` over `A` is
 [reflexive](globular-types.reflexive-globular-types.md) and
 [transitive](globular-types.transitive-globular-types.md), so it is a
-[noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md).
+[noncoherent ω-precategory](wild-category-theory.noncoherent-omega-precategories.md).
 
 The structures defined in this file are used to define the
-[noncoherent large wild higher precategory of types](foundation.wild-category-of-types.md).
+[wild category of types](foundation.wild-category-of-types.md).
 
 ## Definitions
 

diff --git a/src/foundation/globular-type-of-functions.lagda.md b/src/foundation/globular-type-of-functions.lagda.md
@@ -34,10 +34,10 @@ functions in terms of the
 The globular type of functions of a type family `B` over `A` is
 [reflexive](globular-types.reflexive-globular-types.md) and
 [transitive](globular-types.transitive-globular-types.md), so it is a
-[noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md).
+[noncoherent ω-precategory](wild-category-theory.noncoherent-omega-precategories.md).
 
 The structures defined in this file are used to define the
-[noncoherent large wild higher precategory of types](foundation.wild-category-of-types.md).
+[large category of types](foundation.wild-category-of-types.md).
 
 ## Definitions
 

diff --git a/src/foundation/wild-category-of-types.lagda.md b/src/foundation/wild-category-of-types.lagda.md
@@ -31,18 +31,16 @@ open import globular-types.large-transitive-globular-types
 open import globular-types.reflexive-globular-types
 open import globular-types.transitive-globular-types
 
-open import wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories
-open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories
-open import wild-category-theory.noncoherent-large-wild-higher-precategories
-open import wild-category-theory.noncoherent-wild-higher-precategories
+open import wild-category-theory.noncoherent-large-omega-precategories
+open import wild-category-theory.noncoherent-omega-precategories
 ```
 
 </details>
 
 ## Idea
 
 The
-{{#concept "wild category of types" Agda=Type-Noncoherent-Large-Wild-Higher-Precategory}}
+{{#concept "wild category of types" Agda=Type-Noncoherent-Large-ω-Precategory}}
 consists of types and [functions](foundation.dependent-function-types.md) and
 [homotopies](foundation-core.homotopies.md).
 
@@ -92,18 +90,18 @@ is-transitive-Large-Transitive-Globular-Type
   is-transitive-Type-Large-Globular-Type
 ```
 
-### The noncoherent large wild higher precategory of types
+### The noncoherent large ω-precategory of types
 
 ```agda
-Type-Noncoherent-Large-Wild-Higher-Precategory :
-  Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
-large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
-  Type-Noncoherent-Large-Wild-Higher-Precategory =
+Type-Noncoherent-Large-ω-Precategory :
+  Noncoherent-Large-ω-Precategory lsuc (_⊔_)
+large-globular-type-Noncoherent-Large-ω-Precategory
+  Type-Noncoherent-Large-ω-Precategory =
   Type-Large-Globular-Type
-id-structure-Noncoherent-Large-Wild-Higher-Precategory
-  Type-Noncoherent-Large-Wild-Higher-Precategory =
+id-structure-Noncoherent-Large-ω-Precategory
+  Type-Noncoherent-Large-ω-Precategory =
   is-reflexive-Type-Large-Globular-Type
-comp-structure-Noncoherent-Large-Wild-Higher-Precategory
-  Type-Noncoherent-Large-Wild-Higher-Precategory =
+comp-structure-Noncoherent-Large-ω-Precategory
+  Type-Noncoherent-Large-ω-Precategory =
   is-transitive-Type-Large-Globular-Type
 ```
diff --git a/src/globular-types/reflexive-globular-types.lagda.md b/src/globular-types/reflexive-globular-types.lagda.md
@@ -327,6 +327,6 @@ module _
 - [Colax reflexive globular maps](globular-types.colax-reflexive-globular-maps.md)
 - [Lax reflexive globular maps](globular-types.lax-reflexive-globular-maps.md)
 - [Reflexive globular maps](globular-types.reflexive-globular-maps.md)
-- [Noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md)
+- [Noncoherent ω-precategories](wild-category-theory.noncoherent-omega-precategories.md)
   are globular types that are both reflexive and
   [transitive](globular-types.transitive-globular-types.md).
diff --git a/src/globular-types/transitive-globular-types.lagda.md b/src/globular-types/transitive-globular-types.lagda.md
@@ -324,6 +324,6 @@ module _
 ## See also
 
 - [Composition structure on globular types](globular-types.composition-structure-globular-types.md)
-- [Noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md)
+- [Noncoherent ω-precategories](wild-category-theory.noncoherent-omega-precategories.md)
   are globular types that are both
   [reflexive](globular-types.reflexive-globular-types.md) and transitive.
diff --git a/src/structured-types/wild-category-of-pointed-types.lagda.md b/src/structured-types/wild-category-of-pointed-types.lagda.md
@@ -32,16 +32,16 @@ open import structured-types.pointed-maps
 open import structured-types.pointed-types
 open import structured-types.uniform-pointed-homotopies
 
-open import wild-category-theory.noncoherent-large-wild-higher-precategories
-open import wild-category-theory.noncoherent-wild-higher-precategories
+open import wild-category-theory.noncoherent-large-omega-precategories
+open import wild-category-theory.noncoherent-omega-precategories
 ```
 
 </details>
 
 ## Idea
 
 The
-{{#concept "wild category of pointed types" Agda=uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory Agda=pointed-type-Noncoherent-Large-Wild-Higher-Precategory}}
+{{#concept "wild category of pointed types" Agda=uniform-pointed-type-Noncoherent-Large-ω-Precategory Agda=pointed-type-Noncoherent-Large-ω-Precategory}}
 consists of [pointed types](structured-types.pointed-types.md),
 [pointed functions](structured-types.pointed-maps.md), and
 [pointed homotopies](structured-types.pointed-homotopies.md).
@@ -57,7 +57,7 @@ the higher cells are [identities](foundation-core.identity-types.md).
 
 ## Definitions
 
-### The noncoherent large wild higher precategory of pointed types, pointed maps, and uniform pointed homotopies
+### The noncoherent large ω-precategory of pointed types, pointed maps, and uniform pointed homotopies
 
 #### The large globular type of pointed types, pointed maps, and uniform pointed homotopies
 
@@ -160,23 +160,23 @@ is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type
   is-transitive-uniform-pointed-Π-Globular-Type _ _
 ```
 
-#### The noncoherent large wild higher precategory of pointed types, pointed maps, and uniform pointed homotopies
+#### The noncoherent large ω-precategory of pointed types, pointed maps, and uniform pointed homotopies
 
 ```agda
-uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory :
-  Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
-large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
-  uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory =
+uniform-pointed-type-Noncoherent-Large-ω-Precategory :
+  Noncoherent-Large-ω-Precategory lsuc (_⊔_)
+large-globular-type-Noncoherent-Large-ω-Precategory
+  uniform-pointed-type-Noncoherent-Large-ω-Precategory =
   uniform-pointed-type-Large-Globular-Type
-id-structure-Noncoherent-Large-Wild-Higher-Precategory
-  uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory =
+id-structure-Noncoherent-Large-ω-Precategory
+  uniform-pointed-type-Noncoherent-Large-ω-Precategory =
   id-structure-uniform-pointed-type-Large-Globular-Type
-comp-structure-Noncoherent-Large-Wild-Higher-Precategory
-  uniform-pointed-type-Noncoherent-Large-Wild-Higher-Precategory =
+comp-structure-Noncoherent-Large-ω-Precategory
+  uniform-pointed-type-Noncoherent-Large-ω-Precategory =
   comp-structure-uniform-pointed-type-Large-Globular-Type
 ```
 
-### The noncoherent large wild higher precategory of pointed types, pointed maps, and nonuniform homotopies
+### The noncoherent large ω-precategory of pointed types, pointed maps, and nonuniform homotopies
 
 #### The large globular type of pointed types, pointed maps, and nonuniform pointed homotopies
 
@@ -326,19 +326,19 @@ is-transitive-1-cell-globular-type-is-transitive-Large-Globular-Type
   is-transitive-pointed-map-Globular-Type _ _
 ```
 
-#### The noncoherent large wild higher precategory of pointed types, pointed maps, and nonuniform pointed homotopies
+#### The noncoherent large ω-precategory of pointed types, pointed maps, and nonuniform pointed homotopies
 
 ```agda
-pointed-type-Noncoherent-Large-Wild-Higher-Precategory :
-  Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
-large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
-  pointed-type-Noncoherent-Large-Wild-Higher-Precategory =
+pointed-type-Noncoherent-Large-ω-Precategory :
+  Noncoherent-Large-ω-Precategory lsuc (_⊔_)
+large-globular-type-Noncoherent-Large-ω-Precategory
+  pointed-type-Noncoherent-Large-ω-Precategory =
   pointed-type-Large-Globular-Type
-id-structure-Noncoherent-Large-Wild-Higher-Precategory
-  pointed-type-Noncoherent-Large-Wild-Higher-Precategory =
+id-structure-Noncoherent-Large-ω-Precategory
+  pointed-type-Noncoherent-Large-ω-Precategory =
   is-reflexive-pointed-type-Large-Globular-Type
-comp-structure-Noncoherent-Large-Wild-Higher-Precategory
-  pointed-type-Noncoherent-Large-Wild-Higher-Precategory =
+comp-structure-Noncoherent-Large-ω-Precategory
+  pointed-type-Noncoherent-Large-ω-Precategory =
   is-transitive-pointed-type-Large-Globular-Type
 ```
 

diff --git a/src/wild-category-theory.lagda.md b/src/wild-category-theory.lagda.md
@@ -13,12 +13,12 @@
 ```agda
 module wild-category-theory where
 
-open import wild-category-theory.colax-functors-noncoherent-large-wild-higher-precategories public
-open import wild-category-theory.colax-functors-noncoherent-wild-higher-precategories public
-open import wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories public
-open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories public
-open import wild-category-theory.maps-noncoherent-large-wild-higher-precategories public
-open import wild-category-theory.maps-noncoherent-wild-higher-precategories public
-open import wild-category-theory.noncoherent-large-wild-higher-precategories public
-open import wild-category-theory.noncoherent-wild-higher-precategories public
+open import wild-category-theory.coinductive-isomorphisms-in-noncoherent-large-omega-precategories public
+open import wild-category-theory.coinductive-isomorphisms-in-noncoherent-omega-precategories public
+open import wild-category-theory.colax-functors-noncoherent-large-omega-precategories public
+open import wild-category-theory.colax-functors-noncoherent-omega-precategories public
+open import wild-category-theory.maps-noncoherent-large-omega-precategories public
+open import wild-category-theory.maps-noncoherent-omega-precategories public
+open import wild-category-theory.noncoherent-large-omega-precategories public
+open import wild-category-theory.noncoherent-omega-precategories public
 ```