superglobular types

src/structured-types.lagda.md

@@ -10,6 +10,9 @@
 module structured-types where
 
 open import structured-types.base-change-dependent-globular-types public
+open import structured-types.base-change-dependent-reflexive-globular-types public
+open import structured-types.binary-dependent-globular-types public
+open import structured-types.binary-dependent-reflexive-globular-types public
 open import structured-types.binary-globular-maps public
 open import structured-types.cartesian-products-types-equipped-with-endomorphisms public
 open import structured-types.central-h-spaces public
@@ -94,23 +97,34 @@ open import structured-types.pointed-types public
 open import structured-types.pointed-types-equipped-with-automorphisms public
 open import structured-types.pointed-unit-type public
 open import structured-types.pointed-universal-property-contractible-types public
+open import structured-types.points-globular-types public
+open import structured-types.points-reflexive-globular-types public
+open import structured-types.pointwise-extensions-binary-families-globular-types public
+open import structured-types.pointwise-extensions-binary-families-reflexive-globular-types public
+open import structured-types.pointwise-extensions-families-globular-types public
+open import structured-types.pointwise-extensions-families-reflexive-globular-types public
 open import structured-types.postcomposition-pointed-maps public
 open import structured-types.precomposition-pointed-maps public
 open import structured-types.products-families-of-globular-types public
+open import structured-types.reflexive-globular-equivalences public
 open import structured-types.reflexive-globular-maps public
 open import structured-types.reflexive-globular-types public
 open import structured-types.sections-dependent-globular-types public
 open import structured-types.sets-equipped-with-automorphisms public
 open import structured-types.small-pointed-types public
+open import structured-types.superglobular-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.terminal-globular-types public
 open import structured-types.transitive-globular-maps 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
 open import structured-types.uniform-pointed-homotopies public
+open import structured-types.unit-globular-type public
+open import structured-types.unit-reflexive-globular-type public
 open import structured-types.universal-globular-type public
 open import structured-types.universal-property-pointed-equivalences public
 open import structured-types.universal-reflexive-globular-type public

src/structured-types/base-change-dependent-reflexive-globular-types.lagda.md

@@ -25,7 +25,14 @@ open import structured-types.reflexive-globular-types
 
 ## Idea
 
-Consider a [reflexive globular map](structured-types.reflexive-globular-maps.md) `f : G → H` between [reflexive globular types](structured-types.reflexive-globular-types.md) `G` and `H`, and consider a [dependent reflexive globular type](structured-types.dependent-reflexive-globular-types.md) `K` over `H`. The {{#concept "base change" Disambiguation="dependent reflexive globular types" Agda=base-change-Dependent-Reflexive-Globular-Type}} `f*K` is the dependent reflexive globular type over `G` given by
+Consider a [reflexive globular map](structured-types.reflexive-globular-maps.md)
+`f : G → H` between
+[reflexive globular types](structured-types.reflexive-globular-types.md) `G` and
+`H`, and consider a
+[dependent reflexive globular type](structured-types.dependent-reflexive-globular-types.md)
+`K` over `H`. The
+{{#concept "base change" Disambiguation="dependent reflexive globular types" Agda=base-change-Dependent-Reflexive-Globular-Type}}
+`f*K` is the dependent reflexive globular type over `G` given by
 
 ```text
   (f*K)₀ x := K₀ (f₀ x)

src/structured-types/binary-dependent-globular-types.lagda.md

@@ -19,7 +19,9 @@ open import structured-types.points-globular-types
 
 ## Idea
 
-Consider two [globular types](structured-types.globular-types.md) `G` and `H`. A {{#concept "binary dependent globular type" Agda=Binary-Dependent-Globular-Type}} `K` over `G` and `H` consists of
+Consider two [globular types](structured-types.globular-types.md) `G` and `H`. A
+{{#concept "binary dependent globular type" Agda=Binary-Dependent-Globular-Type}}
+`K` over `G` and `H` consists of
 
 ```text
   K₀ : G₀ → H₀ → Type

src/structured-types/binary-dependent-reflexive-globular-types.lagda.md

@@ -21,15 +21,26 @@ open import structured-types.reflexive-globular-types
 
 ## Idea
 
-Consider two [reflexive globular types](structured-types.reflexive-globular-types.md) `G` and `H`. A {{#concept "binary dependent reflexive globular type" Agda=Binary-Dependent-Reflexive-Globular-Type}} `K` over `G` and `H` consists of a [binary dependent globular type](structured-types.binary-dependent-globular-types.md) `K` over `G` and `H` equipped with reflexivity structure `Kᵣ`.
-
-A binary dependent globular type `K` over reflexive globular types `G` and `H` is said to be {{#concept "reflexive" Disambiguation="binary dependent globular type"}} if it comes equipped with
+Consider two
+[reflexive globular types](structured-types.reflexive-globular-types.md) `G` and
+`H`. A
+{{#concept "binary dependent reflexive globular type" Agda=Binary-Dependent-Reflexive-Globular-Type}}
+`K` over `G` and `H` consists of a
+[binary dependent globular type](structured-types.binary-dependent-globular-types.md)
+`K` over `G` and `H` equipped with reflexivity structure `Kᵣ`.
+
+A binary dependent globular type `K` over reflexive globular types `G` and `H`
+is said to be
+{{#concept "reflexive" Disambiguation="binary dependent globular type"}} if it
+comes equipped with
 
 ```text
   Kᵣ : {x : G₀} {y : H₀} (u : K₀ x y) → K₁ (Gᵣ x) (Gᵣ y) u u,
 ```
 
-such that the binary dependent globular type `K' s t u v` over `G' x x'` and `H' y y'` comes equipped with reflexivity structure for every `s : G₁ x x'` and `t : H₁ y y'`.
+such that the binary dependent globular type `K' s t u v` over `G' x x'` and
+`H' y y'` comes equipped with reflexivity structure for every `s : G₁ x x'` and
+`t : H₁ y y'`.
 
 ## Definitions
 
@@ -174,7 +185,7 @@ record
     refl-1-cell-binary-dependent-reflexive-globular-type-Binary-Dependent-Reflexive-Globular-Type
       ( s)
       ( t)
-     
+
 open Binary-Dependent-Reflexive-Globular-Type public
 ```
 

src/structured-types/points-globular-types.lagda.md

@@ -21,7 +21,12 @@ open import structured-types.unit-globular-type
 
 ## Idea
 
-A {{#concept "point" Disambiguation="globular type" Agda=point-Globular-Type}} of a [globular type](structured-types.globular-types.md) `G` consists of a 0-cell `x₀ : G₀` and a point in the globular type `G' x₀ x₀` of 1-cells from `x₀` to itself. Equivalently, a point is a [globular map](structured-types.globular-maps.md) from the [unit globular type](structured-types.unit-globular-types.md) `𝟏` to `G`.
+A {{#concept "point" Disambiguation="globular type" Agda=point-Globular-Type}}
+of a [globular type](structured-types.globular-types.md) `G` consists of a
+0-cell `x₀ : G₀` and a point in the globular type `G' x₀ x₀` of 1-cells from
+`x₀` to itself. Equivalently, a point is a
+[globular map](structured-types.globular-maps.md) from the
+[unit globular type](structured-types.unit-globular-type.md) `𝟏` to `G`.
 
 ## Definitions
 

src/structured-types/points-reflexive-globular-types.lagda.md

@@ -19,9 +19,20 @@ open import structured-types.reflexive-globular-types
 
 ## Idea
 
-Consider a [reflexive globular type](structured-types.reflexive-globular-types.md) `G`. A {{#concept "point" Disambiguation="reflexive globular type" Agda=point-Reflexive-Globular-Type}} of `G` is a 0-cell of `G`. Equivalently, a point of `G` is a [reflexive globular map](structured-types.reflexive-globular-maps.md) from the [unit reflexive globular type](structured-types.unit-reflexive-globular-type.md) into `G`.
+Consider a
+[reflexive globular type](structured-types.reflexive-globular-types.md) `G`. A
+{{#concept "point" Disambiguation="reflexive globular type" Agda=point-Reflexive-Globular-Type}}
+of `G` is a 0-cell of `G`. Equivalently, a point of `G` is a
+[reflexive globular map](structured-types.reflexive-globular-maps.md) from the
+[unit reflexive globular type](structured-types.unit-reflexive-globular-type.md)
+into `G`.
 
-The definition of points of reflexive globular types is much simpler than the definition of [points](structured-types.points-globular-types.md) of ordinary [globular types](structured-types.globular-types.md). This is due to the condition that reflexive globular maps preserve reflexivity, and therefore the type of higher cells relating the underlying 0-cell to itself is [contractible](foundation-core.contractible-types.md).
+The definition of points of reflexive globular types is much simpler than the
+definition of [points](structured-types.points-globular-types.md) of ordinary
+[globular types](structured-types.globular-types.md). This is due to the
+condition that reflexive globular maps preserve reflexivity, and therefore the
+type of higher cells relating the underlying 0-cell to itself is
+[contractible](foundation-core.contractible-types.md).
 
 ## Definitions
 

src/structured-types/pointwise-extensions-binary-families-globular-types.lagda.md

@@ -20,15 +20,24 @@ open import structured-types.globular-types
 open import structured-types.points-globular-types
 ```
 
+</details>
+
 ## Idea
 
-Consider two [globular types](structured-types.globular-types.md) `G` and `H`, and a binary family
+Consider two [globular types](structured-types.globular-types.md) `G` and `H`,
+and a binary family
 
 ```text
   K : G₀ → H₀ → Globular-Type
 ```
 
-of globular types, indexed over the 0-cells of `G` and `H`. Furthermore, consider a [binary dependent globular type](structured-types.binary-dependent-globular-types.md) `L` over `G` and `H`. We say that `L` is a {{#concept "pointwise extension" Disambiguation="binary family of globular types" Agda=is-pointwise-extension-Binary-Dependent-Globular-Type}} of `K` if it comes equipped with a family of [globular equivalences](structured-types.globular-equivalences.md)
+of globular types, indexed over the 0-cells of `G` and `H`. Furthermore,
+consider a
+[binary dependent globular type](structured-types.binary-dependent-globular-types.md)
+`L` over `G` and `H`. We say that `L` is a
+{{#concept "pointwise extension" Disambiguation="binary family of globular types" Agda=is-pointwise-extension-binary-family-globular-types}}
+of `K` if it comes equipped with a family of
+[globular equivalences](structured-types.globular-equivalences.md)
 
 ```text
   (x : point G) (y : point H) → ev-point L x y ≃ K x₀ y₀.

src/structured-types/pointwise-extensions-binary-families-reflexive-globular-types.lagda.md

@@ -24,13 +24,21 @@ open import structured-types.reflexive-globular-types
 
 ## Idea
 
-Consider two [reflexive globular types](structured-types.reflexive-globular-types.md) `G` and `H`, and a binary family
+Consider two
+[reflexive globular types](structured-types.reflexive-globular-types.md) `G` and
+`H`, and a binary family
 
 ```text
   K : G₀ → H₀ → Reflexive-Globular-Type
 ```
 
-of reflexive globular types, indexed over the 0-cells of `G` and `H`. Furthermore, consider a [binary dependent reflexive globular type](structured-types.binary-dependent-reflexive-globular-types.md) `L` over `G` and `H`. We say that `L` is a {{#concept "pointwise extension" Disambiguation="binary family of reflexive globular types" Agda=is-pointwise-extension-Binary-Dependent-Reflexive-Globular-Type}} of `K` if it comes equipped with a family of [reflexive globular equivalences](structured-types.reflexive-globular-equivalences.md)
+of reflexive globular types, indexed over the 0-cells of `G` and `H`.
+Furthermore, consider a
+[binary dependent reflexive globular type](structured-types.binary-dependent-reflexive-globular-types.md)
+`L` over `G` and `H`. We say that `L` is a
+{{#concept "pointwise extension" Disambiguation="binary family of reflexive globular types" Agda=is-pointwise-extension-binary-family-reflexive-globular-types}}
+of `K` if it comes equipped with a family of
+[reflexive globular equivalences](structured-types.reflexive-globular-equivalences.md)
 
 ```text
   (x : point G) (y : point H) → ev-point L x y ≃ K x₀ y₀.
@@ -77,4 +85,3 @@ module _
     Σ ( Binary-Dependent-Reflexive-Globular-Type l7 l8 G H)
       ( is-pointwise-extension-binary-family-reflexive-globular-types K)
 ```
-

src/structured-types/pointwise-extensions-families-globular-types.lagda.md

@@ -22,7 +22,14 @@ open import structured-types.points-globular-types
 
 ## Idea
 
-Consider a family of [globular types](structured-types.globular-types.md) `H : G₀ → Globular-Type` indexed by the 0-cells of a globular type `G` and consider a [dependent globular type](structured-types.dependent-globular-types.md) `K` over `G`. We say that `K` is a {{#concept "pointwise extension" Disambiguation="family of globular types" Agda=is-pointwise-extension-family-of-globular-types-Dependent-Globular-Type}} of `H` if it comes equipped with a family of [globular equivalences](structured-types.globular-equivalences.md)
+Consider a family of [globular types](structured-types.globular-types.md)
+`H : G₀ → Globular-Type` indexed by the 0-cells of a globular type `G` and
+consider a
+[dependent globular type](structured-types.dependent-globular-types.md) `K` over
+`G`. We say that `K` is a
+{{#concept "pointwise extension" Disambiguation="family of globular types" Agda=is-pointwise-extension-family-of-globular-types-Dependent-Globular-Type}}
+of `H` if it comes equipped with a family of
+[globular equivalences](structured-types.globular-equivalences.md)
 
 ```text
   ev-point K x ≃ H x₀

src/structured-types/pointwise-extensions-families-reflexive-globular-types.lagda.md

@@ -16,24 +16,33 @@ open import foundation.universe-levels
 
 open import structured-types.dependent-globular-types
 open import structured-types.dependent-reflexive-globular-types
-open import structured-types.reflexive-globular-equivalences
 open import structured-types.globular-types
 open import structured-types.points-globular-types
 open import structured-types.points-reflexive-globular-types
+open import structured-types.reflexive-globular-equivalences
 open import structured-types.reflexive-globular-types
 ```
 
 </details>
 
 ## Idea
 
-Consider a family of [reflexive globular types](structured-types.reflexive-globular-types.md) `H : G₀ → Reflexive-Globular-Type` indexed by the 0-cells of a reflexive globular type `G` and consider a [dependent reflexive globular type](structured-types.dependent-reflexive-globular-types.md) `K` over `G`. We say that `K` is a {{#concept "pointwise extension" Disambiguation="family of reflexive globular types"}} of `H` if it comes equipped with a family of [reflexive globular equivalences](structured-types.reflexive-globular-equivalences.md)
+Consider a family of
+[reflexive globular types](structured-types.reflexive-globular-types.md)
+`H : G₀ → Reflexive-Globular-Type` indexed by the 0-cells of a reflexive
+globular type `G` and consider a
+[dependent reflexive globular type](structured-types.dependent-reflexive-globular-types.md)
+`K` over `G`. We say that `K` is a
+{{#concept "pointwise extension" Disambiguation="family of reflexive globular types"}}
+of `H` if it comes equipped with a family of
+[reflexive globular equivalences](structured-types.reflexive-globular-equivalences.md)
 
 ```text
   ev-point K x ≃ H x₀
 ```
 
-indexed by the [points](structured-types.points-reflexive-globular-types.md) of `G`.
+indexed by the [points](structured-types.points-reflexive-globular-types.md) of
+`G`.
 
 ## Definitions
 

src/structured-types/superglobular-types.lagda.md

@@ -20,23 +20,34 @@ open import structured-types.reflexive-globular-equivalences
 open import structured-types.reflexive-globular-types
 ```
 
-**Disclaimer.** The contents of this file are experimental, and likely to be changed or reconsidered.
+</details>
+
+**Disclaimer.** The contents of this file are experimental, and likely to be
+changed or reconsidered.
 
 ## Idea
 
-An {{#concept "superglobular type" Agda=Extensive-Globular-Type}} is a [reflexive globular type](structured-types.reflexive-globular-types.md) `G` such that the binary family of globular types
+An {{#concept "superglobular type" Agda=Superglobular-Type}} is a
+[reflexive globular type](structured-types.reflexive-globular-types.md) `G` such
+that the binary family of globular types
 
 ```text
   G' : G₀ → G₀ → Globular-Type
 ```
 
-of 1-cells and higher cells [extends pointwise](structured-types.pointwise-extensions-binary-families-globular-types.md) to a [binary dependent globular type](structured-types.binary-dependent-globular-types.md). More specifically, a superglobular type consists of a reflexive globular type `G` equipped with a binary dependent globular type
+of 1-cells and higher cells
+[extends pointwise](structured-types.pointwise-extensions-binary-families-globular-types.md)
+to a
+[binary dependent globular type](structured-types.binary-dependent-globular-types.md).
+More specifically, a superglobular type consists of a reflexive globular type
+`G` equipped with a binary dependent globular type
 
 ```text
   H : Binary-Dependent-Globular-Type l2 l2 G G
 ```
 
-and a family of [globular equivalences](structured-types.globular-equivalences.md)
+and a family of
+[globular equivalences](structured-types.globular-equivalences.md)
 
 ```text
   (x y : G₀) → ev-point H x y ≃ G' x y.
@@ -64,7 +75,9 @@ The low-dimensional data of a superglobular type is therefore as follows:
        H₂ (Gᵣ x) (Gᵣ y) u v ≃ G₃ (e₁ u) (e₁ v)
 ```
 
-Note that the type of pairs `(Gₙ₊₁ , eₙ)` in this structure is [contractible](foundation-core.contractible-types.md). An equivalent way of presenting the low-dimensional data of a superglobular type is therefore:
+Note that the type of pairs `(Gₙ₊₁ , eₙ)` in this structure is
+[contractible](foundation-core.contractible-types.md). An equivalent way of
+presenting the low-dimensional data of a superglobular type is therefore:
 
 ```text
   G₀ : Type
@@ -79,7 +92,6 @@ Note that the type of pairs `(Gₙ₊₁ , eₙ)` in this structure is [contract
        (p : H₂ s s') (q : H₂ t t') → H₁ s t → H₁ s' t' → Type
 ```
 
-
 ## Definitions
 
 ### The predicate of being a superglobular type
@@ -88,7 +100,7 @@ Note that the type of pairs `(Gₙ₊₁ , eₙ)` in this structure is [contract
 module _
   {l1 l2 : Level} (l3 l4 : Level) (G : Reflexive-Globular-Type l1 l2)
   where
-  
+
   is-superglobular-Reflexive-Globular-Type : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
   is-superglobular-Reflexive-Globular-Type =
     pointwise-extension-binary-family-reflexive-globular-types l3 l4 G G

src/structured-types/terminal-globular-types.lagda.md

@@ -20,9 +20,11 @@ open import structured-types.globular-types
 
 ## Idea
 
-A [globular type](structured-types.globular-types.md) `G` is said to be {{#concept "terminal" Disambiguation="globular type" Agda=is-terminal-Globular-Type}} if for any globular type `H` the type of [globular maps](structured-types.globular-maps.md) `H → G` is [contractible](foundation-core.contractible-types.md).
-
-The standard {{#concept "terminal globular type" Agda=terminal-Globular-Type}} is the [unit globular type](structured-types.unit-globular-type.md).
+A [globular type](structured-types.globular-types.md) `G` is said to be
+{{#concept "terminal" Disambiguation="globular type" Agda=is-terminal-Globular-Type}}
+if for any globular type `H` the type of
+[globular maps](structured-types.globular-maps.md) `H → G` is
+[contractible](foundation-core.contractible-types.md).
 
 ## Definitions
 

src/structured-types/unit-globular-type.lagda.md

@@ -19,7 +19,8 @@ open import structured-types.globular-types
 
 ## Idea
 
-The {{#concept "unit globular type" Agda=unit-Globular-Type}} is the [globular type](structured-types.globular-types.md) `𝟏` given by
+The {{#concept "unit globular type" Agda=unit-Globular-Type}} is the
+[globular type](structured-types.globular-types.md) `𝟏` given by
 
 ```text
   𝟏₀ := unit