Extensionality of globular types (#1190)

Adds a postulate to characterize equality of globular types.

DESIGN-PRINCIPLES.md

@@ -28,9 +28,11 @@ makes use of several postulates.
    [`synthetic-homotopy-theory.circle`](synthetic-homotopy-theory.circle.md)
 9. **Pushouts** are postulated in
    [`synthetic-homotopy-theory.pushouts`](synthetic-homotopy-theory.pushouts.md)
-10. Various **Agda built-in types** are postulated in
+10. **Extensionality of globular types** is postulated in
+    [`structured-types.equality-globular-types`](structured-types.equality-globular-types.md).
+11. Various **Agda built-in types** are postulated in
     [`primitives`](primitives.md) and in [`reflection`](reflection.md).
-11. The **flat modality** and accompanying modalities, with propositional
+12. The **flat modality** and accompanying modalities, with propositional
     computation rules, are postulated in
     [`modal-type-theory`](modal-type-theory.md).
 

src/structured-types.lagda.md

@@ -24,6 +24,8 @@ 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

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

@@ -0,0 +1,183 @@
+# Equality of globular types
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module structured-types.equality-globular-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-types
+open import foundation.torsorial-type-families
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.coherently-invertible-maps
+open import foundation-core.equivalences
+open import foundation-core.retractions
+open import foundation-core.sections
+
+open import structured-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
+[univalence](foundation.univalence.md).
+
+## Definitions
+
+### Coinductive equality of globular types
+
+```agda
+record
+  Eq-Globular-Type
+  {l1 l2 : Level} (A : Globular-Type l1 l2) (B : Globular-Type l1 l2) :
+    UU (lsuc l1 ⊔ lsuc l2)
+  where
+  coinductive
+  field
+    eq-0-cell-Eq-Globular-Type :
+      0-cell-Globular-Type A ＝ 0-cell-Globular-Type B
+
+  map-0-cell-Eq-Globular-Type :
+      0-cell-Globular-Type A → 0-cell-Globular-Type B
+  map-0-cell-Eq-Globular-Type = map-eq eq-0-cell-Eq-Globular-Type
+
+  field
+    globular-type-1-cell-Eq-Globular-Type :
+      {x y : 0-cell-Globular-Type A} →
+      Eq-Globular-Type
+        ( 1-cell-globular-type-Globular-Type A x y)
+        ( 1-cell-globular-type-Globular-Type B
+          ( map-0-cell-Eq-Globular-Type x)
+          ( map-0-cell-Eq-Globular-Type y))
+
+open Eq-Globular-Type public
+
+refl-Eq-Globular-Type :
+  {l1 l2 : Level} (A : Globular-Type l1 l2) → Eq-Globular-Type A A
+refl-Eq-Globular-Type A =
+  λ where
+  .eq-0-cell-Eq-Globular-Type → refl
+  .globular-type-1-cell-Eq-Globular-Type {x} {y} →
+    refl-Eq-Globular-Type (1-cell-globular-type-Globular-Type A x y)
+
+Eq-eq-Globular-Type :
+  {l1 l2 : Level} {A B : Globular-Type l1 l2} → A ＝ B → Eq-Globular-Type A B
+Eq-eq-Globular-Type {A = A} refl = refl-Eq-Globular-Type A
+```
+
+### Equality of globular types as a dependent sum
+
+```agda
+module _
+  {l1 l2 : Level}
+  where
+
+  Eq-Globular-Type' : (A B : Globular-Type l1 l2) → UU (lsuc l1 ⊔ lsuc l2)
+  Eq-Globular-Type' A B =
+    Σ ( 0-cell-Globular-Type A ＝ 0-cell-Globular-Type B)
+      ( λ p →
+        (x y : 0-cell-Globular-Type A) →
+        1-cell-globular-type-Globular-Type A x y ＝
+        1-cell-globular-type-Globular-Type B (map-eq p x) (map-eq p y))
+
+  refl-Eq-Globular-Type' : (A : Globular-Type l1 l2) → Eq-Globular-Type' A A
+  refl-Eq-Globular-Type' A =
+    ( refl , refl-binary-htpy (1-cell-globular-type-Globular-Type A))
+
+  Eq-eq-Globular-Type' :
+    {A B : Globular-Type l1 l2} → A ＝ B → Eq-Globular-Type' A B
+  Eq-eq-Globular-Type' {A} refl = refl-Eq-Globular-Type' A
+```
+
+## Postulate
+
+We postulate that the map `Eq-eq-Globular-Type : A ＝ B → Eq-Globular-Type A B`
+is a [coherently invertible map](foundation-core.coherently-invertible-maps.md).
+
+```agda
+module _
+  {l1 l2 : Level} {A B : Globular-Type l1 l2}
+  where
+
+  postulate
+    eq-Eq-Globular-Type :
+      Eq-Globular-Type A B → A ＝ B
+
+  postulate
+    is-section-eq-Eq-Globular-Type :
+      is-section Eq-eq-Globular-Type eq-Eq-Globular-Type
+
+  postulate
+    is-retraction-eq-Eq-Globular-Type :
+      is-retraction Eq-eq-Globular-Type eq-Eq-Globular-Type
+
+  postulate
+    coh-eq-Eq-Globular-Type :
+      coherence-is-coherently-invertible
+        ( Eq-eq-Globular-Type)
+        ( eq-Eq-Globular-Type)
+        ( is-section-eq-Eq-Globular-Type)
+        ( is-retraction-eq-Eq-Globular-Type)
+```
+
+## Further definitions
+
+```agda
+module _
+  {l1 l2 : Level} {A B : Globular-Type l1 l2}
+  where
+
+  is-coherently-invertible-Eq-eq-Globular-Type :
+    is-coherently-invertible (Eq-eq-Globular-Type {A = A} {B})
+  is-coherently-invertible-Eq-eq-Globular-Type =
+    ( eq-Eq-Globular-Type ,
+      is-section-eq-Eq-Globular-Type ,
+      is-retraction-eq-Eq-Globular-Type ,
+      coh-eq-Eq-Globular-Type)
+
+  is-equiv-Eq-eq-Globular-Type : is-equiv (Eq-eq-Globular-Type {A = A} {B})
+  is-equiv-Eq-eq-Globular-Type =
+    is-equiv-is-invertible
+      eq-Eq-Globular-Type
+      is-section-eq-Eq-Globular-Type
+      is-retraction-eq-Eq-Globular-Type
+
+  is-equiv-eq-Eq-Globular-Type :
+    is-equiv (eq-Eq-Globular-Type {A = A} {B})
+  is-equiv-eq-Eq-Globular-Type =
+    is-equiv-is-invertible
+      Eq-eq-Globular-Type
+      is-retraction-eq-Eq-Globular-Type
+      is-section-eq-Eq-Globular-Type
+
+  equiv-Eq-eq-Globular-Type : (A ＝ B) ≃ Eq-Globular-Type A B
+  equiv-Eq-eq-Globular-Type = Eq-eq-Globular-Type , is-equiv-Eq-eq-Globular-Type
+
+  equiv-eq-Eq-Globular-Type : Eq-Globular-Type A B ≃ (A ＝ B)
+  equiv-eq-Eq-Globular-Type = eq-Eq-Globular-Type , is-equiv-eq-Eq-Globular-Type
+
+is-torsorial-Eq-Globular-Type :
+  {l1 l2 : Level} {A : Globular-Type l1 l2} →
+  is-torsorial (Eq-Globular-Type A)
+is-torsorial-Eq-Globular-Type =
+  fundamental-theorem-id'
+    ( λ _ → Eq-eq-Globular-Type)
+    ( λ _ → is-equiv-Eq-eq-Globular-Type)
+```

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

@@ -0,0 +1,165 @@
+# Equivalences between globular types
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module structured-types.equivalences-globular-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import structured-types.globular-types
+```
+
+</details>
+
+## Idea
+
+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
+
+```text
+  Fₙ₊₁ : (𝑛+1)-Cell A x y ≃ (𝑛+1)-Cell B (Fₙ x) (Fₙ y).
+```
+
+## Definitions
+
+### Equivalences between globular types
+
+```agda
+record
+  equiv-Globular-Type
+  {l1 l2 l3 l4 : Level} (A : Globular-Type l1 l2) (B : Globular-Type l3 l4)
+  : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  where
+  coinductive
+  field
+    equiv-0-cell-equiv-Globular-Type :
+      0-cell-Globular-Type A ≃ 0-cell-Globular-Type B
+
+  map-0-cell-equiv-Globular-Type :
+      0-cell-Globular-Type A → 0-cell-Globular-Type B
+  map-0-cell-equiv-Globular-Type = map-equiv equiv-0-cell-equiv-Globular-Type
+
+  field
+    globular-type-1-cell-equiv-Globular-Type :
+      {x y : 0-cell-Globular-Type A} →
+      equiv-Globular-Type
+        ( 1-cell-globular-type-Globular-Type A x y)
+        ( 1-cell-globular-type-Globular-Type B
+          ( map-0-cell-equiv-Globular-Type x)
+          ( map-0-cell-equiv-Globular-Type y))
+
+open equiv-Globular-Type public
+
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
+  (F : equiv-Globular-Type A B)
+  where
+
+  equiv-1-cell-equiv-Globular-Type :
+    {x y : 0-cell-Globular-Type A} →
+    1-cell-Globular-Type A x y ≃
+    1-cell-Globular-Type B
+      ( map-0-cell-equiv-Globular-Type F x)
+      ( map-0-cell-equiv-Globular-Type F y)
+  equiv-1-cell-equiv-Globular-Type =
+    equiv-0-cell-equiv-Globular-Type
+      ( globular-type-1-cell-equiv-Globular-Type F)
+
+  map-1-cell-equiv-Globular-Type :
+    {x y : 0-cell-Globular-Type A} →
+    1-cell-Globular-Type A x y →
+    1-cell-Globular-Type B
+      ( map-0-cell-equiv-Globular-Type F x)
+      ( map-0-cell-equiv-Globular-Type F y)
+  map-1-cell-equiv-Globular-Type =
+    map-0-cell-equiv-Globular-Type (globular-type-1-cell-equiv-Globular-Type F)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
+  (F : equiv-Globular-Type A B)
+  where
+
+  equiv-2-cell-equiv-Globular-Type :
+    {x y : 0-cell-Globular-Type A}
+    {f g : 1-cell-Globular-Type A x y} →
+    2-cell-Globular-Type A f g ≃
+    2-cell-Globular-Type B
+      ( map-1-cell-equiv-Globular-Type F f)
+      ( map-1-cell-equiv-Globular-Type F g)
+  equiv-2-cell-equiv-Globular-Type =
+    equiv-1-cell-equiv-Globular-Type
+      ( globular-type-1-cell-equiv-Globular-Type F)
+
+  map-2-cell-equiv-Globular-Type :
+    {x y : 0-cell-Globular-Type A}
+    {f g : 1-cell-Globular-Type A x y} →
+    2-cell-Globular-Type A f g →
+    2-cell-Globular-Type B
+      ( map-1-cell-equiv-Globular-Type F f)
+      ( map-1-cell-equiv-Globular-Type F g)
+  map-2-cell-equiv-Globular-Type =
+    map-1-cell-equiv-Globular-Type (globular-type-1-cell-equiv-Globular-Type F)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
+  (F : equiv-Globular-Type A B)
+  where
+
+  equiv-3-cell-equiv-Globular-Type :
+    {x y : 0-cell-Globular-Type A}
+    {f g : 1-cell-Globular-Type A x y} →
+    {H K : 2-cell-Globular-Type A f g} →
+    3-cell-Globular-Type A H K ≃
+    3-cell-Globular-Type B
+      ( map-2-cell-equiv-Globular-Type F H)
+      ( map-2-cell-equiv-Globular-Type F K)
+  equiv-3-cell-equiv-Globular-Type =
+    equiv-2-cell-equiv-Globular-Type
+      ( globular-type-1-cell-equiv-Globular-Type F)
+```
+
+### The identity equiv on a globular type
+
+```agda
+id-equiv-Globular-Type :
+  {l1 l2 : Level} (A : Globular-Type l1 l2) → equiv-Globular-Type A A
+id-equiv-Globular-Type A =
+  λ where
+  .equiv-0-cell-equiv-Globular-Type → id-equiv
+  .globular-type-1-cell-equiv-Globular-Type {x} {y} →
+    id-equiv-Globular-Type (1-cell-globular-type-Globular-Type A x y)
+```
+
+### Composition of equivalences of globular types
+
+```agda
+comp-equiv-Globular-Type :
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : Globular-Type l1 l2}
+  {B : Globular-Type l3 l4}
+  {C : Globular-Type l5 l6} →
+  equiv-Globular-Type B C → equiv-Globular-Type A B → equiv-Globular-Type A C
+comp-equiv-Globular-Type g f =
+  λ where
+  .equiv-0-cell-equiv-Globular-Type →
+    equiv-0-cell-equiv-Globular-Type g ∘e equiv-0-cell-equiv-Globular-Type f
+  .globular-type-1-cell-equiv-Globular-Type →
+    comp-equiv-Globular-Type
+      ( globular-type-1-cell-equiv-Globular-Type g)
+      ( globular-type-1-cell-equiv-Globular-Type f)
+```