From dae7788d8df508ffc06e5c7d3f557df1bf028ded Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 10 Jul 2024 15:24:38 +0200 Subject: [PATCH] fix typos wild categories --- src/universal-algebra.lagda.md | 2 +- ...s-noncoherent-large-wild-higher-precategories.lagda.md | 6 ++---- ...unctors-noncoherent-wild-higher-precategories.lagda.md | 6 ++---- ...n-noncoherent-large-wild-higher-precategories.lagda.md | 4 ++-- ...isms-in-noncoherent-wild-higher-precategories.lagda.md | 4 ++-- .../noncoherent-large-wild-higher-precategories.lagda.md | 2 +- .../noncoherent-wild-higher-precategories.lagda.md | 8 ++++---- 7 files changed, 14 insertions(+), 18 deletions(-) diff --git a/src/universal-algebra.lagda.md b/src/universal-algebra.lagda.md index 76e1822e54..f3f214e968 100644 --- a/src/universal-algebra.lagda.md +++ b/src/universal-algebra.lagda.md @@ -1,4 +1,4 @@ -# Universal Algebra +# Universal algebra ## Files in the universal algebra folder diff --git a/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md index 0342a37f56..6e923d8faa 100644 --- a/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/colax-functors-noncoherent-large-wild-higher-precategories.lagda.md @@ -42,10 +42,8 @@ is an $(n+1)$-morphism Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f) ``` -in `ℬ`, - -and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, there -is an $(n+2)$-morphism +in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, +there is an $(n+2)$-morphism ```text Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f) diff --git a/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md index 3cf672b514..0c5b5f044f 100644 --- a/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md @@ -39,10 +39,8 @@ is an $(n+1)$-morphism Fₙ₊₁ (id-hom 𝒜 f) ⇒ id-hom ℬ (Fₙ f) ``` -in `ℬ`, - -and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, there -is an $(n+2)$-morphism +in `ℬ`, and for every pair of composable $(n+1)$-morphisms `g` after `f` in `𝒜`, +there is an $(n+2)$-morphism ```text Fₙ₊₁ (g ∘ f) ⇒ (Fₙ₊₁ g) ∘ (Fₙ₊₁ f) diff --git a/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md index 0129547cd8..5dcb2e82cc 100644 --- a/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/isomorphisms-in-noncoherent-large-wild-higher-precategories.lagda.md @@ -22,9 +22,9 @@ open import wild-category-theory.noncoherent-large-wild-higher-precategories Consider a [noncoherent large wild higher precategory](wild-category-theory.noncoherent-large-wild-higher-precategories.md) -𝒞. An +`𝒞`. An {{#concept "isomorphism" Disambiguation="in noncoherent large wild higher precategories" Agda=is-iso-Noncoherent-Large-Wild-Higher-Precategory}} -in 𝒞 is a morphism `f : x → y` in 𝒞 [equipped](foundation.structure.md) with +in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with - a morphism `s : y → x` - a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote diff --git a/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md index 932e38ed12..c4a7182618 100644 --- a/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/isomorphisms-in-noncoherent-wild-higher-precategories.lagda.md @@ -21,9 +21,9 @@ open import wild-category-theory.noncoherent-wild-higher-precategories Consider a [noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md) -𝒞. An +`𝒞`. An {{#concept "isomorphism" Disambiguation="in noncoherent wild higher precategories" Agda=is-iso-Noncoherent-Wild-Higher-Precategory}} -in 𝒞 is a morphism `f : x → y` in 𝒞 [equipped](foundation.structure.md) with +in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure.md) with - a morphism `s : y → x` - a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote diff --git a/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md index e451d335ee..a35acc18ca 100644 --- a/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/noncoherent-large-wild-higher-precategories.lagda.md @@ -32,7 +32,7 @@ open import wild-category-theory.noncoherent-wild-higher-precategories ## Idea -It is a important open problem known as the _coherence problem_ to define a +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 diff --git a/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md index bfc5d023e3..0d32197fc4 100644 --- a/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md @@ -30,16 +30,16 @@ open import structured-types.transitive-globular-types ## Idea -It is a important open problem known as the _coherence problem_ to define a +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 wild higher precategory_. A _noncoherent wild higher precategory_ `𝒞` is a structure that attempts at -capturing the structure of an higher precategory to the $0$'th order. It -consists of in some sense all of the operations and none of the coherence of an -higher precategory. Thus, it is defined as a +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](structured-types.globular-types.md) with families of $n$-morphisms labeled as "identities"