From 4eacd3a9de3e36a58143fd754eccdb9b4403ce48 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sun, 17 Nov 2024 11:15:06 -0500 Subject: [PATCH] chore: Moving files about globular types to a new namespace (#1223) This PR should be merged before #1196. I have only moved files and adjusted imports and markdown links accordingly, in an attempt to preserve the credits to the content creators. --- DESIGN-PRINCIPLES.md | 2 +- .../wild-category-of-types.lagda.md | 12 ++++----- src/globular-types.lagda.md | 26 +++++++++++++++++++ .../dependent-globular-types.lagda.md | 8 +++--- ...ependent-reflexive-globular-types.lagda.md | 15 +++++------ .../equality-globular-types.lagda.md | 12 ++++----- .../globular-equivalences.lagda.md} | 10 +++---- .../globular-maps.lagda.md} | 8 +++--- .../globular-types.lagda.md | 10 +++---- .../large-globular-maps.lagda.md} | 10 +++---- .../large-globular-types.lagda.md | 6 ++--- .../large-reflexive-globular-types.lagda.md | 8 +++--- .../large-symmetric-globular-types.lagda.md | 8 +++--- .../large-transitive-globular-types.lagda.md | 8 +++--- .../reflexive-globular-types.lagda.md | 6 ++--- .../symmetric-globular-types.lagda.md | 6 ++--- .../transitive-globular-types.lagda.md | 6 ++--- src/structured-types.lagda.md | 14 ---------- .../wild-category-of-pointed-types.lagda.md | 13 +++++----- ...one-diagrams-synthetic-categories.lagda.md | 2 +- .../cospans-synthetic-categories.lagda.md | 2 +- ...equivalences-synthetic-categories.lagda.md | 2 +- ...ble-functors-synthetic-categories.lagda.md | 2 +- .../pullbacks-synthetic-categories.lagda.md | 2 +- .../retractions-synthetic-categories.lagda.md | 2 +- .../sections-synthetic-categories.lagda.md | 8 +++--- .../synthetic-categories.lagda.md | 4 +-- ...t-large-wild-higher-precategories.lagda.md | 4 +-- ...oherent-wild-higher-precategories.lagda.md | 4 +-- ...t-large-wild-higher-precategories.lagda.md | 2 +- ...oherent-wild-higher-precategories.lagda.md | 2 +- ...t-large-wild-higher-precategories.lagda.md | 8 +++--- ...oherent-wild-higher-precategories.lagda.md | 4 +-- ...t-large-wild-higher-precategories.lagda.md | 14 +++++----- ...oherent-wild-higher-precategories.lagda.md | 20 +++++++------- 35 files changed, 141 insertions(+), 129 deletions(-) create mode 100644 src/globular-types.lagda.md rename src/{structured-types => globular-types}/dependent-globular-types.lagda.md (85%) rename src/{structured-types => globular-types}/dependent-reflexive-globular-types.lagda.md (95%) rename src/{structured-types => globular-types}/equality-globular-types.lagda.md (92%) rename src/{structured-types/equivalences-globular-types.lagda.md => globular-types/globular-equivalences.lagda.md} (94%) rename src/{structured-types/maps-globular-types.lagda.md => globular-types/globular-maps.lagda.md} (93%) rename src/{structured-types => globular-types}/globular-types.lagda.md (95%) rename src/{structured-types/maps-large-globular-types.lagda.md => globular-types/large-globular-maps.lagda.md} (92%) rename src/{structured-types => globular-types}/large-globular-types.lagda.md (98%) rename src/{structured-types => globular-types}/large-reflexive-globular-types.lagda.md (91%) rename src/{structured-types => globular-types}/large-symmetric-globular-types.lagda.md (90%) rename src/{structured-types => globular-types}/large-transitive-globular-types.lagda.md (93%) rename src/{structured-types => globular-types}/reflexive-globular-types.lagda.md (97%) rename src/{structured-types => globular-types}/symmetric-globular-types.lagda.md (94%) rename src/{structured-types => globular-types}/transitive-globular-types.lagda.md (96%) diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index ada849d7b3..d66229a164 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -29,7 +29,7 @@ makes use of several postulates. 9. **Pushouts** are postulated in [`synthetic-homotopy-theory.pushouts`](synthetic-homotopy-theory.pushouts.md) 10. **Extensionality of globular types** is postulated in - [`structured-types.equality-globular-types`](structured-types.equality-globular-types.md). + [`globular-types.equality-globular-types`](globular-types.equality-globular-types.md). 11. Various **Agda built-in types** are postulated in [`primitives`](primitives.md) and in [`reflection`](reflection.md). 12. The **flat modality** and accompanying modalities, with propositional diff --git a/src/foundation/wild-category-of-types.lagda.md b/src/foundation/wild-category-of-types.lagda.md index d712b916cc..c357241b15 100644 --- a/src/foundation/wild-category-of-types.lagda.md +++ b/src/foundation/wild-category-of-types.lagda.md @@ -23,12 +23,12 @@ open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types -open import structured-types.globular-types -open import structured-types.large-globular-types -open import structured-types.large-reflexive-globular-types -open import structured-types.large-transitive-globular-types -open import structured-types.reflexive-globular-types -open import structured-types.transitive-globular-types +open import globular-types.globular-types +open import globular-types.large-globular-types +open import globular-types.large-reflexive-globular-types +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 diff --git a/src/globular-types.lagda.md b/src/globular-types.lagda.md new file mode 100644 index 0000000000..cc27aa4418 --- /dev/null +++ b/src/globular-types.lagda.md @@ -0,0 +1,26 @@ +# Globular types + +```agda +{-# OPTIONS --guardedness #-} +``` + +## Modules in the globular types namespace + +```agda +module globular-types where + +open import globular-types.dependent-globular-types public +open import globular-types.dependent-reflexive-globular-types public +open import globular-types.equality-globular-types public +open import globular-types.globular-equivalences public +open import globular-types.globular-maps public +open import globular-types.globular-types public +open import globular-types.large-globular-maps public +open import globular-types.large-globular-types public +open import globular-types.large-reflexive-globular-types public +open import globular-types.large-symmetric-globular-types public +open import globular-types.large-transitive-globular-types public +open import globular-types.reflexive-globular-types public +open import globular-types.symmetric-globular-types public +open import globular-types.transitive-globular-types public +``` diff --git a/src/structured-types/dependent-globular-types.lagda.md b/src/globular-types/dependent-globular-types.lagda.md similarity index 85% rename from src/structured-types/dependent-globular-types.lagda.md rename to src/globular-types/dependent-globular-types.lagda.md index ca590cd22c..bb5b68cbac 100644 --- a/src/structured-types/dependent-globular-types.lagda.md +++ b/src/globular-types/dependent-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.dependent-globular-types where +module globular-types.dependent-globular-types where ```
Imports @@ -12,14 +12,14 @@ module structured-types.dependent-globular-types where open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
## Idea -Consider a [globular type](structured-types.globular-types.md) `G`. A +Consider a [globular type](globular-types.globular-types.md) `G`. A {{#concept "dependent globular type" Agda=Dependent-Globular-Type}} over `G` consists of a type family `H₀ : G₀ → 𝒰`, and for any two `0`-cells `x y : G₀` in `G` a binary family of dependent globular types @@ -67,4 +67,4 @@ module _ ## See also -- [Dependent reflexive globular types](structured-types.dependent-reflexive-globular-types.md) +- [Dependent reflexive globular types](globular-types.dependent-reflexive-globular-types.md) diff --git a/src/structured-types/dependent-reflexive-globular-types.lagda.md b/src/globular-types/dependent-reflexive-globular-types.lagda.md similarity index 95% rename from src/structured-types/dependent-reflexive-globular-types.lagda.md rename to src/globular-types/dependent-reflexive-globular-types.lagda.md index 3f7100064f..8971e9fe20 100644 --- a/src/structured-types/dependent-reflexive-globular-types.lagda.md +++ b/src/globular-types/dependent-reflexive-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.dependent-reflexive-globular-types where +module globular-types.dependent-reflexive-globular-types where ```
Imports @@ -12,21 +12,20 @@ module structured-types.dependent-reflexive-globular-types where open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.dependent-globular-types -open import structured-types.globular-types -open import structured-types.reflexive-globular-types +open import globular-types.dependent-globular-types +open import globular-types.globular-types +open import globular-types.reflexive-globular-types ```
## Idea -Consider a -[reflexive globular type](structured-types.reflexive-globular-types.md) `G` -equipped with a reflexivity element `ρ`. A +Consider a [reflexive globular type](globular-types.reflexive-globular-types.md) +`G` equipped with a reflexivity element `ρ`. A {{#concept "dependent reflexive globular type" Agda=Dependent-Reflexive-Globular-Type}} over `G` consists of a -[dependent globular type](structured-types.dependent-globular-types.md) `H` over +[dependent globular type](globular-types.dependent-globular-types.md) `H` over `G` equipped with a reflexivity element `ρ'` consisting of ```text diff --git a/src/structured-types/equality-globular-types.lagda.md b/src/globular-types/equality-globular-types.lagda.md similarity index 92% rename from src/structured-types/equality-globular-types.lagda.md rename to src/globular-types/equality-globular-types.lagda.md index cd425b2c56..a93f6bde6f 100644 --- a/src/structured-types/equality-globular-types.lagda.md +++ b/src/globular-types/equality-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.equality-globular-types where +module globular-types.equality-globular-types where ```
Imports @@ -25,7 +25,7 @@ open import foundation-core.equivalences open import foundation-core.retractions open import foundation-core.sections -open import structured-types.globular-types +open import globular-types.globular-types ```
@@ -33,10 +33,10 @@ open import structured-types.globular-types ## Idea We postulate that [equality](foundation-core.identity-types.md) of -[globular types](structured-types.globular-types.md) is characterized by -equality of the 0-cells together with, coinductively, a binary family of -equalities of the globular type of 1-cells over the equality of the 0-cells. -This phrasing is used so that the extensionality principle is independent of +[globular types](globular-types.globular-types.md) is characterized by equality +of the 0-cells together with, coinductively, a binary family of equalities of +the globular type of 1-cells over the equality of the 0-cells. This phrasing is +used so that the extensionality principle is independent of [univalence](foundation.univalence.md). ## Definitions diff --git a/src/structured-types/equivalences-globular-types.lagda.md b/src/globular-types/globular-equivalences.lagda.md similarity index 94% rename from src/structured-types/equivalences-globular-types.lagda.md rename to src/globular-types/globular-equivalences.lagda.md index a588dfa7c5..92be9520e6 100644 --- a/src/structured-types/equivalences-globular-types.lagda.md +++ b/src/globular-types/globular-equivalences.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.equivalences-globular-types where +module globular-types.globular-equivalences where ```
Imports @@ -15,7 +15,7 @@ open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
@@ -24,9 +24,9 @@ open import structured-types.globular-types An {{#concept "equivalence" Disambiguation="globular types" Agda=equiv-Globular-Type}} -`f` between [globular types](structured-types.globular-types.md) `A` and `B` is -an equivalence `F₀` of $0$-cells, and for every pair of $n$-cells `x` and `y`, -an equivalence of $(n+1)$-cells +`f` between [globular types](globular-types.globular-types.md) `A` and `B` is an +equivalence `F₀` of $0$-cells, and for every pair of $n$-cells `x` and `y`, an +equivalence of $(n+1)$-cells ```text Fₙ₊₁ : (𝑛+1)-Cell A x y ≃ (𝑛+1)-Cell B (Fₙ x) (Fₙ y). diff --git a/src/structured-types/maps-globular-types.lagda.md b/src/globular-types/globular-maps.lagda.md similarity index 93% rename from src/structured-types/maps-globular-types.lagda.md rename to src/globular-types/globular-maps.lagda.md index 897076319b..38fb82846e 100644 --- a/src/structured-types/maps-globular-types.lagda.md +++ b/src/globular-types/globular-maps.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.maps-globular-types where +module globular-types.globular-maps where ```
Imports @@ -14,7 +14,7 @@ open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
@@ -22,8 +22,8 @@ open import structured-types.globular-types ## Idea A {{#concept "map" Disambiguation="globular types" Agda=map-Globular-Type}} `f` -between [globular types](structured-types.globular-types.md) `A` and `B` is a -map `F₀` of $0$-cells, and for every pair of $n$-cells `x` and `y`, a map of +between [globular types](globular-types.globular-types.md) `A` and `B` is a map +`F₀` of $0$-cells, and for every pair of $n$-cells `x` and `y`, a map of $(n+1)$-cells ```text diff --git a/src/structured-types/globular-types.lagda.md b/src/globular-types/globular-types.lagda.md similarity index 95% rename from src/structured-types/globular-types.lagda.md rename to src/globular-types/globular-types.lagda.md index 64ffb4d0cb..3afa544c04 100644 --- a/src/structured-types/globular-types.lagda.md +++ b/src/globular-types/globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.globular-types where +module globular-types.globular-types where ```
Imports @@ -58,7 +58,7 @@ special property of globular types. **Comment.** The choice to add a second universe level in the definition of a globular structure may seem rather arbitrary, but makes the concept applicable in particular extra cases that are of use to us when working with -[large globular structures](structured-types.large-globular-types.md). +[large globular structures](globular-types.large-globular-types.md). ```agda record @@ -209,6 +209,6 @@ globular-structure-Id A = ## See also -- [Reflexive globular types](structured-types.reflexive-globular-types.md) -- [Symmetric globular types](structured-types.symmetric-globular-types.md) -- [Transitive globular types](structured-types.transitive-globular-types.md) +- [Reflexive globular types](globular-types.reflexive-globular-types.md) +- [Symmetric globular types](globular-types.symmetric-globular-types.md) +- [Transitive globular types](globular-types.transitive-globular-types.md) diff --git a/src/structured-types/maps-large-globular-types.lagda.md b/src/globular-types/large-globular-maps.lagda.md similarity index 92% rename from src/structured-types/maps-large-globular-types.lagda.md rename to src/globular-types/large-globular-maps.lagda.md index be0963436a..4331f40162 100644 --- a/src/structured-types/maps-large-globular-types.lagda.md +++ b/src/globular-types/large-globular-maps.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.maps-large-globular-types where +module globular-types.large-globular-maps where ```
Imports @@ -13,9 +13,9 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.large-globular-types -open import structured-types.maps-globular-types +open import globular-types.globular-maps +open import globular-types.globular-types +open import globular-types.large-globular-types ```
@@ -24,7 +24,7 @@ open import structured-types.maps-globular-types A {{#concept "map" Disambiguation="large globular types" Agda=map-Large-Globular-Type}} -`f` between [large globular types](structured-types.large-globular-types.md) `A` +`f` between [large globular types](globular-types.large-globular-types.md) `A` and `B` is a map `F₀` of $0$-cells, and for every pair of $n$-cells `x` and `y`, a map of $(n+1)$-cells diff --git a/src/structured-types/large-globular-types.lagda.md b/src/globular-types/large-globular-types.lagda.md similarity index 98% rename from src/structured-types/large-globular-types.lagda.md rename to src/globular-types/large-globular-types.lagda.md index 04675ce811..1ffa424ac5 100644 --- a/src/structured-types/large-globular-types.lagda.md +++ b/src/globular-types/large-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.large-globular-types where +module globular-types.large-globular-types where ```
Imports @@ -12,7 +12,7 @@ module structured-types.large-globular-types where open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
@@ -22,7 +22,7 @@ open import structured-types.globular-types A {{#concept "large globular type" Agda=Large-Globular-Type}} is a hierarchy of types indexed by universe levels, [equipped](foundation.structure.md) with a [large binary relation](foundation.large-binary-relations.md) valued in -[globular types](structured-types.globular-types.md). +[globular types](globular-types.globular-types.md). Thus, a large globular type consists of a base hierarchy of types indexed by universe levels `A` called the _$0$-cells_, and for every pair of $0$-cells, a diff --git a/src/structured-types/large-reflexive-globular-types.lagda.md b/src/globular-types/large-reflexive-globular-types.lagda.md similarity index 91% rename from src/structured-types/large-reflexive-globular-types.lagda.md rename to src/globular-types/large-reflexive-globular-types.lagda.md index d48595094e..404b25e14a 100644 --- a/src/structured-types/large-reflexive-globular-types.lagda.md +++ b/src/globular-types/large-reflexive-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.large-reflexive-globular-types where +module globular-types.large-reflexive-globular-types where ```
Imports @@ -12,15 +12,15 @@ module structured-types.large-reflexive-globular-types where open import foundation.large-binary-relations open import foundation.universe-levels -open import structured-types.large-globular-types -open import structured-types.reflexive-globular-types +open import globular-types.large-globular-types +open import globular-types.reflexive-globular-types ```
## Idea -A [large globular type](structured-types.large-globular-types.md) is +A [large globular type](globular-types.large-globular-types.md) is {{#concept "reflexive" Disambiguation="large globular type" Agda=is-reflexive-large-globular-structure}} if every $n$-cell `x` comes with a choice of $(n+1)$-cell from `x` to `x`. diff --git a/src/structured-types/large-symmetric-globular-types.lagda.md b/src/globular-types/large-symmetric-globular-types.lagda.md similarity index 90% rename from src/structured-types/large-symmetric-globular-types.lagda.md rename to src/globular-types/large-symmetric-globular-types.lagda.md index 73b86a8c71..4eb510c457 100644 --- a/src/structured-types/large-symmetric-globular-types.lagda.md +++ b/src/globular-types/large-symmetric-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.large-symmetric-globular-types where +module globular-types.large-symmetric-globular-types where ```
Imports @@ -12,15 +12,15 @@ module structured-types.large-symmetric-globular-types where open import foundation.large-binary-relations open import foundation.universe-levels -open import structured-types.large-globular-types -open import structured-types.symmetric-globular-types +open import globular-types.large-globular-types +open import globular-types.symmetric-globular-types ```
## Idea -We say a [large globular type](structured-types.large-globular-types.md) is +We say a [large globular type](globular-types.large-globular-types.md) is {{#concept "symmetric" Disambiguation="large globular type" Agda=is-symmetric-large-globular-structure}} if there is a symmetry action on its $n$-cells for positive $n$, mapping $n$-cells from `x` to `y` to $n$-cells from `y` to `x`. diff --git a/src/structured-types/large-transitive-globular-types.lagda.md b/src/globular-types/large-transitive-globular-types.lagda.md similarity index 93% rename from src/structured-types/large-transitive-globular-types.lagda.md rename to src/globular-types/large-transitive-globular-types.lagda.md index af1cd79af6..a043fb72f7 100644 --- a/src/structured-types/large-transitive-globular-types.lagda.md +++ b/src/globular-types/large-transitive-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.large-transitive-globular-types where +module globular-types.large-transitive-globular-types where ```
Imports @@ -11,8 +11,8 @@ module structured-types.large-transitive-globular-types where ```agda open import foundation.universe-levels -open import structured-types.large-globular-types -open import structured-types.transitive-globular-types +open import globular-types.large-globular-types +open import globular-types.transitive-globular-types ```
@@ -21,7 +21,7 @@ open import structured-types.transitive-globular-types A {{#concept "large transitive globular type" Agda=Large-Transitive-Globular-Type}} -is a [large globular type](structured-types.large-globular-types.md) `A` +is a [large globular type](globular-types.large-globular-types.md) `A` [equipped](foundation.structure.md) with a binary operator ```text diff --git a/src/structured-types/reflexive-globular-types.lagda.md b/src/globular-types/reflexive-globular-types.lagda.md similarity index 97% rename from src/structured-types/reflexive-globular-types.lagda.md rename to src/globular-types/reflexive-globular-types.lagda.md index 69c8ba538a..9753bd99bc 100644 --- a/src/structured-types/reflexive-globular-types.lagda.md +++ b/src/globular-types/reflexive-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.reflexive-globular-types where +module globular-types.reflexive-globular-types where ```
Imports @@ -14,14 +14,14 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
## Idea -A [globular type](structured-types.globular-types.md) is +A [globular type](globular-types.globular-types.md) is {{#concept "reflexive" Disambiguation="globular type" Agda=is-reflexive-globular-structure}} if every $n$-cell `x` comes with a choice of $(n+1)$-cell from `x` to `x`. diff --git a/src/structured-types/symmetric-globular-types.lagda.md b/src/globular-types/symmetric-globular-types.lagda.md similarity index 94% rename from src/structured-types/symmetric-globular-types.lagda.md rename to src/globular-types/symmetric-globular-types.lagda.md index b84c03ea08..4b57dbf4cc 100644 --- a/src/structured-types/symmetric-globular-types.lagda.md +++ b/src/globular-types/symmetric-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.symmetric-globular-types where +module globular-types.symmetric-globular-types where ```
Imports @@ -14,14 +14,14 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
## Idea -We say a [globular type](structured-types.globular-types.md) is +We say a [globular type](globular-types.globular-types.md) is {{#concept "symmetric" Disambiguation="globular type" Agda=is-symmetric-globular-structure}} if there is a symmetry action on its $n$-cells for positive $n$, mapping $n$-cells from `x` to `y` to $n$-cells from `y` to `x`. diff --git a/src/structured-types/transitive-globular-types.lagda.md b/src/globular-types/transitive-globular-types.lagda.md similarity index 96% rename from src/structured-types/transitive-globular-types.lagda.md rename to src/globular-types/transitive-globular-types.lagda.md index 798d612054..bb6e080c8d 100644 --- a/src/structured-types/transitive-globular-types.lagda.md +++ b/src/globular-types/transitive-globular-types.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --guardedness #-} -module structured-types.transitive-globular-types where +module globular-types.transitive-globular-types where ```
Imports @@ -13,7 +13,7 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
@@ -21,7 +21,7 @@ open import structured-types.globular-types ## Idea A {{#concept "transitive globular type" Agda=Transitive-Globular-Type}} is a -[globular type](structured-types.globular-types.md) `A` +[globular type](globular-types.globular-types.md) `A` [equipped](foundation.structure.md) with a binary operator ```text diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index 967885e085..081ebda794 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -18,14 +18,10 @@ open import structured-types.conjugation-pointed-types public open import structured-types.constant-pointed-maps public open import structured-types.contractible-pointed-types public open import structured-types.cyclic-types public -open import structured-types.dependent-globular-types public open import structured-types.dependent-products-h-spaces public open import structured-types.dependent-products-pointed-types public open import structured-types.dependent-products-wild-monoids public -open import structured-types.dependent-reflexive-globular-types public open import structured-types.dependent-types-equipped-with-automorphisms public -open import structured-types.equality-globular-types public -open import structured-types.equivalences-globular-types public open import structured-types.equivalences-h-spaces public open import structured-types.equivalences-pointed-arrows public open import structured-types.equivalences-types-equipped-with-automorphisms public @@ -36,20 +32,13 @@ open import structured-types.finite-multiplication-magmas public open import structured-types.function-h-spaces public open import structured-types.function-magmas public open import structured-types.function-wild-monoids public -open import structured-types.globular-types public open import structured-types.h-spaces public open import structured-types.initial-pointed-type-equipped-with-automorphism public open import structured-types.involutive-type-of-h-space-structures public open import structured-types.involutive-types public open import structured-types.iterated-cartesian-products-types-equipped-with-endomorphisms public open import structured-types.iterated-pointed-cartesian-product-types public -open import structured-types.large-globular-types public -open import structured-types.large-reflexive-globular-types public -open import structured-types.large-symmetric-globular-types public -open import structured-types.large-transitive-globular-types public open import structured-types.magmas public -open import structured-types.maps-globular-types public -open import structured-types.maps-large-globular-types public open import structured-types.mere-equivalences-types-equipped-with-endomorphisms public open import structured-types.morphisms-h-spaces public open import structured-types.morphisms-magmas public @@ -79,13 +68,10 @@ open import structured-types.pointed-unit-type public open import structured-types.pointed-universal-property-contractible-types public open import structured-types.postcomposition-pointed-maps public open import structured-types.precomposition-pointed-maps public -open import structured-types.reflexive-globular-types public open import structured-types.sets-equipped-with-automorphisms public open import structured-types.small-pointed-types public open import structured-types.symmetric-elements-involutive-types public -open import structured-types.symmetric-globular-types public open import structured-types.symmetric-h-spaces public -open import structured-types.transitive-globular-types public open import structured-types.transposition-pointed-span-diagrams public open import structured-types.types-equipped-with-automorphisms public open import structured-types.types-equipped-with-endomorphisms public diff --git a/src/structured-types/wild-category-of-pointed-types.lagda.md b/src/structured-types/wild-category-of-pointed-types.lagda.md index 14d31f1fa0..e833b1f4a0 100644 --- a/src/structured-types/wild-category-of-pointed-types.lagda.md +++ b/src/structured-types/wild-category-of-pointed-types.lagda.md @@ -16,18 +16,19 @@ open import foundation.identity-types open import foundation.universe-levels open import foundation.whiskering-identifications-concatenation -open import structured-types.globular-types -open import structured-types.large-globular-types -open import structured-types.large-reflexive-globular-types -open import structured-types.large-transitive-globular-types +open import globular-types.globular-types +open import globular-types.large-globular-types +open import globular-types.large-reflexive-globular-types +open import globular-types.large-transitive-globular-types +open import globular-types.reflexive-globular-types +open import globular-types.transitive-globular-types + open import structured-types.pointed-2-homotopies open import structured-types.pointed-dependent-functions open import structured-types.pointed-families-of-types open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-types -open import structured-types.reflexive-globular-types -open import structured-types.transitive-globular-types open import structured-types.uniform-pointed-homotopies open import wild-category-theory.noncoherent-large-wild-higher-precategories diff --git a/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md b/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md index b94a468b43..793041a163 100644 --- a/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/cone-diagrams-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.cospans-synthetic-categories open import synthetic-category-theory.synthetic-categories diff --git a/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md b/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md index 8051db1b1d..d4385ae17e 100644 --- a/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/cospans-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.equivalences-synthetic-categories open import synthetic-category-theory.synthetic-categories diff --git a/src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md b/src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md index 7e6f9d6866..e616153e9f 100644 --- a/src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/equivalences-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.retractions-synthetic-categories open import synthetic-category-theory.sections-synthetic-categories diff --git a/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md b/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md index 59b67d0c4f..79a237ffc1 100644 --- a/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/invertible-functors-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.equivalences-synthetic-categories open import synthetic-category-theory.retractions-synthetic-categories diff --git a/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md b/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md index 9da94176ce..c57580a72d 100644 --- a/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/pullbacks-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.cone-diagrams-synthetic-categories open import synthetic-category-theory.cospans-synthetic-categories diff --git a/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md b/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md index cf22e0f544..9eefe32176 100644 --- a/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/retractions-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.synthetic-categories ``` diff --git a/src/synthetic-category-theory/sections-synthetic-categories.lagda.md b/src/synthetic-category-theory/sections-synthetic-categories.lagda.md index acd4f1c5db..e24866c194 100644 --- a/src/synthetic-category-theory/sections-synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/sections-synthetic-categories.lagda.md @@ -13,7 +13,7 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types open import synthetic-category-theory.synthetic-categories ``` @@ -22,10 +22,10 @@ open import synthetic-category-theory.synthetic-categories ## Idea -A section of a functor f: A → B is a functor g: B → A equipped with a natural -isomorphism f∘g ≅ id. +A section of a functor `f : A → B` is a functor `g : B → A` equipped with a +natural isomorphism `f ∘ g ≅ id`. -### The predicate of being a section of a functor f: A → B +### The predicate of being a section of a functor `f : A → B` ```agda module _ diff --git a/src/synthetic-category-theory/synthetic-categories.lagda.md b/src/synthetic-category-theory/synthetic-categories.lagda.md index 80066da1ba..5deaf488e8 100644 --- a/src/synthetic-category-theory/synthetic-categories.lagda.md +++ b/src/synthetic-category-theory/synthetic-categories.lagda.md @@ -12,7 +12,7 @@ module synthetic-category-theory.synthetic-categories where open import foundation.dependent-pair-types open import foundation.universe-levels -open import structured-types.globular-types +open import globular-types.globular-types ```
@@ -63,7 +63,7 @@ category theory. In synthetic category theory we may speak of categories, functors, isomorphisms between them, isomorphisms between those, and so forth. The sorts in the language of synthetic category theory are therefore organized in a -[globular type](structured-types.globular-types.md). +[globular type](globular-types.globular-types.md). ```agda module _ 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 6e923d8faa..905b7193d3 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 @@ -14,8 +14,8 @@ open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.maps-globular-types +open import globular-types.globular-maps +open import globular-types.globular-types open import wild-category-theory.colax-functors-noncoherent-wild-higher-precategories open import wild-category-theory.maps-noncoherent-large-wild-higher-precategories 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 0c5b5f044f..085730ee57 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 @@ -14,8 +14,8 @@ open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.maps-globular-types +open import globular-types.globular-maps +open import globular-types.globular-types open import wild-category-theory.maps-noncoherent-wild-higher-precategories open import wild-category-theory.noncoherent-wild-higher-precategories 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 5dcb2e82cc..78566fcef7 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 @@ -30,7 +30,7 @@ in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure. - a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote composition of morphisms and the identity morphism given by the transitive and reflexive structure on the underlying - [globular type](structured-types.globular-types.md), respectively + [globular type](globular-types.globular-types.md), respectively - a proof `is-iso-is-split-epi : is-iso is-split-epi`, which shows that the above $2$-morphism is itself an isomorphism - a morphism `r : y → x` 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 c4a7182618..e0d30bc8ae 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 @@ -29,7 +29,7 @@ in `𝒞` is a morphism `f : x → y` in `𝒞` [equipped](foundation.structure. - a $2$-morphism `is-split-epi : f ∘ s → id`, where `∘` and `id` denote composition of morphisms and the identity morphism given by the transitive and reflexive structure on the underlying - [globular type](structured-types.globular-types.md), respectively + [globular type](globular-types.globular-types.md), respectively - a proof `is-iso-is-split-epi : is-iso is-split-epi`, which shows that the above $2$-morphism is itself an isomorphism - a morphism `r : y → x` diff --git a/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md b/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md index 292ce8a8b0..76fed249a4 100644 --- a/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/maps-noncoherent-large-wild-higher-precategories.lagda.md @@ -14,10 +14,10 @@ open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.large-globular-types -open import structured-types.maps-globular-types -open import structured-types.maps-large-globular-types +open import globular-types.globular-maps +open import globular-types.globular-types +open import globular-types.large-globular-maps +open import globular-types.large-globular-types open import wild-category-theory.maps-noncoherent-wild-higher-precategories open import wild-category-theory.noncoherent-large-wild-higher-precategories diff --git a/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md b/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md index 051aa89d16..54cfcc8f8f 100644 --- a/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/maps-noncoherent-wild-higher-precategories.lagda.md @@ -14,8 +14,8 @@ open import foundation.function-types open import foundation.identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.maps-globular-types +open import globular-types.globular-maps +open import globular-types.globular-types open import wild-category-theory.noncoherent-wild-higher-precategories ``` 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 a35acc18ca..ce0ca67672 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 @@ -20,10 +20,10 @@ open import foundation.sets open import foundation.strictly-involutive-identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.large-globular-types -open import structured-types.large-reflexive-globular-types -open import structured-types.large-transitive-globular-types +open import globular-types.globular-types +open import globular-types.large-globular-types +open import globular-types.large-reflexive-globular-types +open import globular-types.large-transitive-globular-types open import wild-category-theory.noncoherent-wild-higher-precategories ``` @@ -43,7 +43,7 @@ A _large noncoherent wild higher precategory_ `𝒞` is a structure that attempt 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](structured-types.large-globular-types.md) with families of +[large globular type](globular-types.large-globular-types.md) with families of $n$-morphisms labeled as "identities" ```text @@ -59,8 +59,8 @@ and a composition operation at every dimension Entirely concretely, we define a {{#concept "noncoherent large wild higher precategory" Agda=Noncoherent-Large-Wild-Higher-Precategory}} -to be a [reflexive](structured-types.reflexive-globular-types.md) and -[transitive](structured-types.transitive-globular-types.md) large globular type. +to be a [reflexive](globular-types.reflexive-globular-types.md) and +[transitive](globular-types.transitive-globular-types.md) large globular type. We call the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells the _$n$-morphisms_. The reflexivities are called the _identity morphisms_, and the transitivity operations are branded as _composition of 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 0d32197fc4..e26040410c 100644 --- a/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md +++ b/src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md @@ -21,9 +21,9 @@ open import foundation.sets open import foundation.strictly-involutive-identity-types open import foundation.universe-levels -open import structured-types.globular-types -open import structured-types.reflexive-globular-types -open import structured-types.transitive-globular-types +open import globular-types.globular-types +open import globular-types.reflexive-globular-types +open import globular-types.transitive-globular-types ``` @@ -40,8 +40,8 @@ A _noncoherent wild higher 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](structured-types.globular-types.md) with families of -$n$-morphisms labeled as "identities" +[globular type](globular-types.globular-types.md) with families of $n$-morphisms +labeled as "identities" ```text id-hom : (x : 𝑛-Cell 𝒞) → (𝑛+1)-Cell 𝒞 x x @@ -56,11 +56,11 @@ and a composition operation at every dimension Entirely concretely, we define a {{#concept "noncoherent wild higher precategory" Agda=Noncoherent-Wild-Higher-Precategory}} -to be a [reflexive](structured-types.reflexive-globular-types.md) and -[transitive](structured-types.transitive-globular-types.md) globular type. We -call the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells -the _$n$-morphisms_. The reflexivities are called the _identity morphisms_, and -the transitivity operations are branded as _composition of morphisms_. +to be a [reflexive](globular-types.reflexive-globular-types.md) and +[transitive](globular-types.transitive-globular-types.md) globular type. We call +the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells the +_$n$-morphisms_. The reflexivities are called the _identity morphisms_, and the +transitivity operations are branded as _composition of morphisms_. ## Definitions