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

@@ -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

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

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
+```

src/structured-types/dependent-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
 
 ## 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)

src/structured-types/dependent-reflexive-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
 
 ## 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

src/structured-types/equality-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -25,18 +25,18 @@ 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
 ```
 
 </details>
 
 ## 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

src/structured-types/equivalences-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
@@ -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).

src/structured-types/maps-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -14,16 +14,16 @@ 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
 ```
 
 </details>
 
 ## 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

src/structured-types/globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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)

src/structured-types/maps-large-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
@@ -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
 

src/structured-types/large-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
@@ -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

src/structured-types/large-reflexive-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
 
 ## 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`.
 

src/structured-types/large-symmetric-globular-types.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -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
 ```
 
 </details>
 
 ## 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`.

src/structured-types/large-transitive-globular-types.lagda.md → src/globular-types/large-transitive-globular-types.lagda.md

@@ -3,16 +3,16 @@
 ```agda
 {-# OPTIONS --guardedness #-}
 
-module structured-types.large-transitive-globular-types where
+module globular-types.large-transitive-globular-types where
 ```
 
 <details><summary>Imports</summary>
 
 ```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
 ```
 
 </details>
@@ -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