From 6a295aa146733295ab1fb671d3a3279503625b61 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 7 Jan 2025 16:54:59 +0100 Subject: [PATCH] prose fixes --- ...oherent-large-omega-precategories.lagda.md | 49 +++++++++---------- .../noncoherent-omega-precategories.lagda.md | 22 ++++----- 2 files changed, 33 insertions(+), 38 deletions(-) diff --git a/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md b/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md index 067fc6f196..d40fa26fd8 100644 --- a/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md +++ b/src/wild-category-theory/noncoherent-large-omega-precategories.lagda.md @@ -35,28 +35,26 @@ open import wild-category-theory.noncoherent-omega-precategories ## Idea It is an important open problem known as the _coherence problem_ to define a -fully coherent notion of $∞$-category in univalent type theory. The subject of -_wild category theory_ attempts to recover some of the benefits of $∞$-category -theory without tackling this problem. We introduce, as one of our basic building -blocks in this subject, the notion of a _large noncoherent wild higher -precategory_. - -A _large noncoherent ω-precategory_ `𝒞` is a structure that attempts at -capturing the structure of a large higher precategory to the $0$'th order. It -consists of in some sense all of the operations and none of the coherence of a -large higher precategory. Thus, it is defined as a -[large globular type](globular-types.large-globular-types.md) with families of -$n$-morphisms labeled as "identities" +fully coherent notion of $∞$-category or higher variants in univalent type +theory. The subject of _wild category theory_ attempts to recover some of the +benefits of $∞$-category theory without tackling this problem. We introduce, as +one of our basic building blocks in this subject, the notion of a _noncoherent +large ω-precategory_. + +A _noncoherent large ω-precategory_ `𝒞` is a structure that attempts at +capturing the structure of a large ω-category to the $0$'th order. It consists +of in some sense all of the operations and none of the coherence. Thus, it is +defined as a [large globular type](globular-types.large-globular-types.md) with +families of $n$-morphisms labeled as "identities" ```text - id-hom : (x : 𝑛-Cell 𝒞) → (𝑛+1)-Cell 𝒞 x x + id-hom : (x : 𝒞ₙ) → 𝒞ₙ₊₁ x x ``` and a composition operation at every dimension ```text - comp-hom : - {x y z : 𝑛-Cell 𝒞} → (𝑛+1)-Cell 𝒞 y z → (𝑛+1)-Cell 𝒞 x y → (𝑛+1)-Cell 𝒞 x z. + comp-hom : {x y z : 𝒞ₙ} → 𝒞ₙ₊₁ y z → 𝒞ₙ₊₁ x y → 𝒞ₙ₊₁ x z. ``` Entirely concretely, we define a @@ -96,8 +94,8 @@ The type of objects of a noncoherent large ω-precategory: large-globular-type-Noncoherent-Large-ω-Precategory ``` -The globular type of morphisms between two objects in a noncoherent large wild -higher precategory: +The globular type of morphisms between two objects in a noncoherent large +ω-precategory: ```agda hom-globular-type-Noncoherent-Large-ω-Precategory : @@ -119,8 +117,8 @@ higher precategory: large-globular-type-Noncoherent-Large-ω-Precategory ``` -The globular structure on the type of objects of a noncoherent large wild higher -precategory: +The globular structure on the type of objects of a noncoherent large +ω-precategory: ```agda globular-structure-obj-Noncoherent-Large-ω-Precategory : @@ -196,8 +194,8 @@ The globular type of 3-morphisms in a noncoherent large ω-precategory: large-globular-type-Noncoherent-Large-ω-Precategory ``` -The globular structure on the type of 2-morphisms in a noncoherent large wild -higher precategory: +The globular structure on the type of 2-morphisms in a noncoherent large +ω-precategory: ```agda globular-structure-2-hom-Noncoherent-Large-ω-Precategory : @@ -213,8 +211,7 @@ higher precategory: large-globular-type-Noncoherent-Large-ω-Precategory ``` -The structure of identity morphisms in a noncoherent large wild higher -precategory: +The structure of identity morphisms in a noncoherent large ω-precategory: ```agda field @@ -336,8 +333,7 @@ large ω-precategory: ( comp-structure-hom-globular-type-Noncoherent-Large-ω-Precategory) ``` -The underlying reflexive globular type of a noncoherent large wild higher -precategory: +The underlying reflexive globular type of a noncoherent large ω-precategory: ```agda large-reflexive-globular-type-Noncoherent-Large-ω-Precategory : @@ -350,8 +346,7 @@ precategory: id-structure-Noncoherent-Large-ω-Precategory ``` -The underlying transitive globular type of a noncoherent large wild higher -precategory: +The underlying transitive globular type of a noncoherent large ω-precategory: ```agda large-transitive-globular-type-Noncoherent-Large-ω-Precategory : diff --git a/src/wild-category-theory/noncoherent-omega-precategories.lagda.md b/src/wild-category-theory/noncoherent-omega-precategories.lagda.md index 832c21fe57..648d1f464f 100644 --- a/src/wild-category-theory/noncoherent-omega-precategories.lagda.md +++ b/src/wild-category-theory/noncoherent-omega-precategories.lagda.md @@ -31,26 +31,26 @@ open import globular-types.transitive-globular-types ## Idea It is an important open problem known as the _coherence problem_ to define a -fully coherent notion of $∞$-category in univalent type theory. The subject of -_wild category theory_ attempts to recover some of the benefits of $∞$-category -theory without tackling this problem. We introduce, as one of our basic building -blocks in this subject, the notion of a _noncoherent ω-precategory_. +fully coherent notion of $∞$-category or higher variants in univalent type +theory. The subject of _wild category theory_ attempts to recover some of the +benefits of $∞$-category theory without tackling this problem. We introduce, as +one of our basic building blocks in this subject, the notion of a _noncoherent +ω-precategory_. A _noncoherent ω-precategory_ `𝒞` is a structure that attempts at capturing the -structure of a higher precategory to the $0$'th order. It consists of in some -sense all of the operations and none of the coherence of a higher precategory. -Thus, it is defined as a [globular type](globular-types.globular-types.md) with -families of $n$-morphisms labeled as "identities" +structure of an ω-category to the $0$'th order. It consists of in some sense all +of the operations and none of the coherence. Thus, it is defined as a +[globular type](globular-types.globular-types.md) with families of $n$-morphisms +labeled as "identities" ```text - id-hom : (x : 𝑛-Cell 𝒞) → (𝑛+1)-Cell 𝒞 x x + id-hom : (x : 𝒞ₙ) → 𝒞ₙ₊₁ x x ``` and a composition operation at every dimension ```text - comp-hom : - {x y z : 𝑛-Cell 𝒞} → (𝑛+1)-Cell 𝒞 y z → (𝑛+1)-Cell 𝒞 x y → (𝑛+1)-Cell 𝒞 x z. + comp-hom : {x y z : 𝒞ₙ} → 𝒞ₙ₊₁ y z → 𝒞ₙ₊₁ x y → 𝒞ₙ₊₁ x z. ``` Entirely concretely, we define a