From 105e1ad346d54330d47f0dc90219e7f4743b851b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 9 Oct 2024 19:21:57 +0200 Subject: [PATCH] Extensionality of globular types (#1190) Adds a postulate to characterize equality of globular types. --- DESIGN-PRINCIPLES.md | 6 +- src/structured-types.lagda.md | 2 + .../equality-globular-types.lagda.md | 183 ++++++++++++++++++ .../equivalences-globular-types.lagda.md | 165 ++++++++++++++++ 4 files changed, 354 insertions(+), 2 deletions(-) create mode 100644 src/structured-types/equality-globular-types.lagda.md create mode 100644 src/structured-types/equivalences-globular-types.lagda.md diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index 81a58850fa..a8639cfa87 100644 --- a/DESIGN-PRINCIPLES.md +++ b/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). diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index 3cdeac110c..967885e085 100644 --- a/src/structured-types.lagda.md +++ b/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 diff --git a/src/structured-types/equality-globular-types.lagda.md b/src/structured-types/equality-globular-types.lagda.md new file mode 100644 index 0000000000..cd425b2c56 --- /dev/null +++ b/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 +``` + +
Imports + +```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 +``` + +
+ +## 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) +``` diff --git a/src/structured-types/equivalences-globular-types.lagda.md b/src/structured-types/equivalences-globular-types.lagda.md new file mode 100644 index 0000000000..a588dfa7c5 --- /dev/null +++ b/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 +``` + +
Imports + +```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 +``` + +
+ +## 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) +```