From f9d879c0f9b2adb3abd2dd15770ba5b506cec00b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 24 Nov 2023 15:29:52 +0100 Subject: [PATCH] Modal type theory (#701) ### Additions - Module on modal type theory, including - Define the flat modality - Define the sharp modality - Start work on their adjunction - Some basic definitions about codiscrete types and the flat modal operator - Some additions on higher modalities - Introduce (strong) subuniverse induction as a relaxation of modal subuniverse induction - Show we can induct on the identity types with a higher modality without appealing to univalence using strong subuniverse induction - Start on functorial properties of higher modalities - Multivariable sections is a definition of sections of multivariable maps that make it possible to circumvent applying function extensionality in many cases. (If we at some point in the future want a module on simplicial homotopy type theory, then it would be fruitful to develop the module on modal type theory further :)) ### A regression It has become clear that the current formulation of higher modalities is not the most practical one, as it needs to assume everything is sufficiently contained within a single universe. In addition, the small relaxation to locally small types seems somewhat contentless and makes the formalizations more cumbersome. I have started a new line of formalization to fix these problems in #890. --- .pre-commit-config.yaml | 14 +- CONTRIBUTING.md | 4 + DESIGN-PRINCIPLES.md | 3 + Makefile | 2 +- .../integer-fractions.lagda.md | 80 +-- .../decidable-propositions.lagda.md | 3 +- src/foundation-core/embeddings.lagda.md | 20 +- .../equality-dependent-pair-types.lagda.md | 6 +- src/foundation-core/small-types.lagda.md | 59 +-- src/foundation-core/subtypes.lagda.md | 4 + src/foundation.lagda.md | 2 + src/foundation/binary-homotopies.lagda.md | 34 +- ...ting-triangles-of-identifications.lagda.md | 49 ++ src/foundation/decidable-equality.lagda.md | 3 + src/foundation/decidable-types.lagda.md | 13 +- .../double-negation-modality.lagda.md | 4 +- src/foundation/equivalences.lagda.md | 6 + src/foundation/images.lagda.md | 42 +- .../iterated-dependent-product-types.lagda.md | 5 +- .../law-of-excluded-middle.lagda.md | 4 +- src/foundation/locally-small-types.lagda.md | 38 +- .../multivariable-homotopies.lagda.md | 11 +- .../multivariable-sections.lagda.md | 92 ++++ src/foundation/telescopes.lagda.md | 29 ++ .../torsorial-type-families.lagda.md | 20 +- src/foundation/truncation-modalities.lagda.md | 2 +- src/foundation/univalence.lagda.md | 4 +- src/modal-type-theory.lagda.md | 22 + .../crisp-identity-types.lagda.md | 37 ++ .../crisp-law-of-excluded-middle.lagda.md | 50 ++ .../flat-dependent-function-types.lagda.md | 66 +++ .../flat-dependent-pair-types.lagda.md | 93 ++++ .../flat-discrete-types.lagda.md | 100 ++++ src/modal-type-theory/flat-modality.lagda.md | 175 +++++++ .../flat-sharp-adjunction.lagda.md | 294 +++++++++++ .../sharp-codiscrete-maps.lagda.md | 50 ++ .../sharp-codiscrete-types.lagda.md | 154 ++++++ src/modal-type-theory/sharp-modality.lagda.md | 220 ++++++++ src/orthogonal-factorization-systems.lagda.md | 3 + .../closed-modalities.lagda.md | 7 +- .../functoriality-higher-modalities.lagda.md | 195 +++++++ .../higher-modalities.lagda.md | 491 ++++++++++++------ .../identity-modality.lagda.md | 2 +- .../modal-induction.lagda.md | 320 ++++++++++++ .../modal-operators.lagda.md | 12 +- .../modal-subuniverse-induction.lagda.md | 480 +++++++++++++++++ .../open-modalities.lagda.md | 42 +- .../raise-modalities.lagda.md | 2 +- .../reflective-subuniverses.lagda.md | 145 ++++-- .../uniquely-eliminating-modalities.lagda.md | 30 +- .../zero-modality.lagda.md | 2 +- src/set-theory/cardinalities.lagda.md | 63 +-- .../cocones-under-spans.lagda.md | 23 +- .../joins-of-types.lagda.md | 215 ++++---- .../pushouts.lagda.md | 2 +- 55 files changed, 3330 insertions(+), 518 deletions(-) create mode 100644 src/foundation/commuting-triangles-of-identifications.lagda.md create mode 100644 src/foundation/multivariable-sections.lagda.md create mode 100644 src/modal-type-theory.lagda.md create mode 100644 src/modal-type-theory/crisp-identity-types.lagda.md create mode 100644 src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md create mode 100644 src/modal-type-theory/flat-dependent-function-types.lagda.md create mode 100644 src/modal-type-theory/flat-dependent-pair-types.lagda.md create mode 100644 src/modal-type-theory/flat-discrete-types.lagda.md create mode 100644 src/modal-type-theory/flat-modality.lagda.md create mode 100644 src/modal-type-theory/flat-sharp-adjunction.lagda.md create mode 100644 src/modal-type-theory/sharp-codiscrete-maps.lagda.md create mode 100644 src/modal-type-theory/sharp-codiscrete-types.lagda.md create mode 100644 src/modal-type-theory/sharp-modality.lagda.md create mode 100644 src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md create mode 100644 src/orthogonal-factorization-systems/modal-induction.lagda.md create mode 100644 src/orthogonal-factorization-systems/modal-subuniverse-induction.lagda.md diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 5ffd298282..41852f881f 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -7,7 +7,7 @@ repos: - id: trailing-whitespace - id: end-of-file-fixer - id: mixed-line-ending - - id: double-quote-string-fixer + # - id: double-quote-string-fixer - id: check-ast - id: check-yaml # - id: check-json # Doesn't accept json with comments @@ -96,12 +96,12 @@ repos: - id: check-case-conflict - id: check-merge-conflict - - repo: https://github.com/pre-commit/mirrors-autopep8 - rev: 'v2.0.2' - hooks: - - id: autopep8 - name: Python scripts formatting - args: ['-i', '--global-config', '/dev/null'] + # - repo: https://github.com/pre-commit/mirrors-autopep8 + # rev: 'v2.0.2' + # hooks: + # - id: autopep8 + # name: Python scripts formatting + # args: ['-i', '--global-config', '/dev/null'] - repo: https://github.com/pre-commit/mirrors-prettier rev: 'v3.0.0-alpha.6' diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 7f3345a3b3..58320d31a2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -25,8 +25,10 @@ Below is a summary of the tasks this tool performs: - **Mixed line ending**: Ensures consistent use of line endings ([LF vs CRLF](https://www.aleksandrhovhannisyan.com/blog/crlf-vs-lf-normalizing-line-endings-in-git/#crlf-vs-lf-what-are-line-endings-anyway)). + - **Python AST**: Checks whether Python scripts parse as valid Python. @@ -76,9 +78,11 @@ Below is a summary of the tasks this tool performs: library. This file is also regenerated by `make check` each time it's run. No manual maintenance is required for this file. + - **CSS, JS, YAML and Markdown (no codeblocks) formatting**: Performs basic formatting tasks such as enforcing the 80-character line limit, formatting diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index 99ef5f78c4..81a58850fa 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -30,6 +30,9 @@ makes use of several postulates. [`synthetic-homotopy-theory.pushouts`](synthetic-homotopy-theory.pushouts.md) 10. 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 + computation rules, are postulated in + [`modal-type-theory`](modal-type-theory.md). Note that there is some redundancy in the postulates we assume. For example, the [univalence axiom implies function extensionality](foundation.univalence-implies-function-extensionality.md), diff --git a/Makefile b/Makefile index 4be42902e7..418f4b9c3e 100644 --- a/Makefile +++ b/Makefile @@ -4,7 +4,7 @@ # files, and if these options are pervasive (i.e. they need to be enabled in all # modules that include the modules that have them enabled), then they need to be # added to the everything file as well. -everythingOpts := --guardedness +everythingOpts := --guardedness --cohesion --flat-split # use "$ export AGDAVERBOSE=-v20" if you want to see all AGDAVERBOSE ?= -v1 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print) diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md index dbfd368c78..f7c60ffceb 100644 --- a/src/elementary-number-theory/integer-fractions.lagda.md +++ b/src/elementary-number-theory/integer-fractions.lagda.md @@ -143,46 +143,46 @@ transitive-sim-fraction-ℤ x y z s r = ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ z) ( denominator-fraction-ℤ y)) ∙ - ( ( ap - ( (numerator-fraction-ℤ x) *ℤ_) - ( commutative-mul-ℤ - ( denominator-fraction-ℤ z) - ( denominator-fraction-ℤ y))) ∙ - ( ( inv - ( associative-mul-ℤ - ( numerator-fraction-ℤ x) - ( denominator-fraction-ℤ y) - ( denominator-fraction-ℤ z))) ∙ - ( ( ap ( _*ℤ (denominator-fraction-ℤ z)) r) ∙ - ( ( associative-mul-ℤ - ( numerator-fraction-ℤ y) - ( denominator-fraction-ℤ x) - ( denominator-fraction-ℤ z)) ∙ - ( ( ap - ( (numerator-fraction-ℤ y) *ℤ_) - ( commutative-mul-ℤ - ( denominator-fraction-ℤ x) - ( denominator-fraction-ℤ z))) ∙ - ( ( inv - ( associative-mul-ℤ - ( numerator-fraction-ℤ y) - ( denominator-fraction-ℤ z) - ( denominator-fraction-ℤ x))) ∙ - ( ( ap (_*ℤ (denominator-fraction-ℤ x)) s) ∙ - ( ( associative-mul-ℤ - ( numerator-fraction-ℤ z) - ( denominator-fraction-ℤ y) - ( denominator-fraction-ℤ x)) ∙ - ( ( ap - ( (numerator-fraction-ℤ z) *ℤ_) - ( commutative-mul-ℤ - ( denominator-fraction-ℤ y) - ( denominator-fraction-ℤ x))) ∙ - ( inv - ( associative-mul-ℤ - ( numerator-fraction-ℤ z) - ( denominator-fraction-ℤ x) - ( denominator-fraction-ℤ y))))))))))))) + ( ap + ( (numerator-fraction-ℤ x) *ℤ_) + ( commutative-mul-ℤ + ( denominator-fraction-ℤ z) + ( denominator-fraction-ℤ y))) ∙ + ( inv + ( associative-mul-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ y) + ( denominator-fraction-ℤ z))) ∙ + ( ap ( _*ℤ (denominator-fraction-ℤ z)) r) ∙ + ( associative-mul-ℤ + ( numerator-fraction-ℤ y) + ( denominator-fraction-ℤ x) + ( denominator-fraction-ℤ z)) ∙ + ( ap + ( (numerator-fraction-ℤ y) *ℤ_) + ( commutative-mul-ℤ + ( denominator-fraction-ℤ x) + ( denominator-fraction-ℤ z))) ∙ + ( inv + ( associative-mul-ℤ + ( numerator-fraction-ℤ y) + ( denominator-fraction-ℤ z) + ( denominator-fraction-ℤ x))) ∙ + ( ap (_*ℤ (denominator-fraction-ℤ x)) s) ∙ + ( associative-mul-ℤ + ( numerator-fraction-ℤ z) + ( denominator-fraction-ℤ y) + ( denominator-fraction-ℤ x)) ∙ + ( ap + ( (numerator-fraction-ℤ z) *ℤ_) + ( commutative-mul-ℤ + ( denominator-fraction-ℤ y) + ( denominator-fraction-ℤ x))) ∙ + ( inv + ( associative-mul-ℤ + ( numerator-fraction-ℤ z) + ( denominator-fraction-ℤ x) + ( denominator-fraction-ℤ y)))) equivalence-relation-sim-fraction-ℤ : equivalence-relation lzero fraction-ℤ pr1 equivalence-relation-sim-fraction-ℤ = sim-fraction-ℤ-Prop diff --git a/src/foundation-core/decidable-propositions.lagda.md b/src/foundation-core/decidable-propositions.lagda.md index af46769d4a..dce6065d8d 100644 --- a/src/foundation-core/decidable-propositions.lagda.md +++ b/src/foundation-core/decidable-propositions.lagda.md @@ -28,7 +28,8 @@ open import foundation-core.subtypes ## Idea -A decidable proposition is a proposition that has a decidable underlying type. +A **decidable proposition** is a [proposition](foundation-core.propositions.md) +that has a [decidable](foundation.decidable-types.md) underlying type. ## Definition diff --git a/src/foundation-core/embeddings.lagda.md b/src/foundation-core/embeddings.lagda.md index 5f6ea53404..3eac0587bb 100644 --- a/src/foundation-core/embeddings.lagda.md +++ b/src/foundation-core/embeddings.lagda.md @@ -40,6 +40,15 @@ module _ is-emb : (A → B) → UU (l1 ⊔ l2) is-emb f = (x y : A) → is-equiv (ap f {x} {y}) + equiv-ap-is-emb : + {f : A → B} (e : is-emb f) {x y : A} → (x ＝ y) ≃ (f x ＝ f y) + pr1 (equiv-ap-is-emb {f} e) = ap f + pr2 (equiv-ap-is-emb {f} e {x} {y}) = e x y + + inv-equiv-ap-is-emb : + {f : A → B} (e : is-emb f) {x y : A} → (f x ＝ f y) ≃ (x ＝ y) + inv-equiv-ap-is-emb e = inv-equiv (equiv-ap-is-emb e) + infix 5 _↪_ _↪_ : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) @@ -50,15 +59,18 @@ module _ where map-emb : A ↪ B → A → B - map-emb f = pr1 f + map-emb = pr1 is-emb-map-emb : (f : A ↪ B) → is-emb (map-emb f) - is-emb-map-emb f = pr2 f + is-emb-map-emb = pr2 equiv-ap-emb : (e : A ↪ B) {x y : A} → (x ＝ y) ≃ (map-emb e x ＝ map-emb e y) - pr1 (equiv-ap-emb e {x} {y}) = ap (map-emb e) - pr2 (equiv-ap-emb e {x} {y}) = is-emb-map-emb e x y + equiv-ap-emb e = equiv-ap-is-emb (is-emb-map-emb e) + + inv-equiv-ap-emb : + (e : A ↪ B) {x y : A} → (map-emb e x ＝ map-emb e y) ≃ (x ＝ y) + inv-equiv-ap-emb e = inv-equiv (equiv-ap-emb e) ``` ## Examples diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md index 327d02e327..27b0da8527 100644 --- a/src/foundation-core/equality-dependent-pair-types.lagda.md +++ b/src/foundation-core/equality-dependent-pair-types.lagda.md @@ -93,7 +93,8 @@ module _ ( is-retraction-pair-eq-Σ s t) equiv-eq-pair-Σ : (s t : Σ A B) → Eq-Σ s t ≃ (s ＝ t) - equiv-eq-pair-Σ s t = pair eq-pair-Σ' (is-equiv-eq-pair-Σ s t) + pr1 (equiv-eq-pair-Σ s t) = eq-pair-Σ' + pr2 (equiv-eq-pair-Σ s t) = is-equiv-eq-pair-Σ s t abstract is-equiv-pair-eq-Σ : (s t : Σ A B) → is-equiv (pair-eq-Σ {s} {t}) @@ -104,7 +105,8 @@ module _ ( is-section-pair-eq-Σ s t) equiv-pair-eq-Σ : (s t : Σ A B) → (s ＝ t) ≃ Eq-Σ s t - equiv-pair-eq-Σ s t = pair pair-eq-Σ (is-equiv-pair-eq-Σ s t) + pr1 (equiv-pair-eq-Σ s t) = pair-eq-Σ + pr2 (equiv-pair-eq-Σ s t) = is-equiv-pair-eq-Σ s t η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t η-pair t = refl diff --git a/src/foundation-core/small-types.lagda.md b/src/foundation-core/small-types.lagda.md index 2021cd0f34..7755e353fc 100644 --- a/src/foundation-core/small-types.lagda.md +++ b/src/foundation-core/small-types.lagda.md @@ -33,8 +33,8 @@ open import foundation-core.propositions ## Idea -A type is said to be small with respect to a universe `UU l` if it is equivalent -to a type in `UU l`. +A type is said to be **small** with respect to a universe `UU l` if it is +[equivalent](foundation-core.equivalences.md) to a type in `UU l`. ## Definitions @@ -45,48 +45,49 @@ is-small : (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1) is-small l A = Σ (UU l) (λ X → A ≃ X) -type-is-small : - {l l1 : Level} {A : UU l1} → is-small l A → UU l -type-is-small = pr1 +module _ + {l l1 : Level} {A : UU l1} (H : is-small l A) + where + + type-is-small : UU l + type-is-small = pr1 H -equiv-is-small : - {l l1 : Level} {A : UU l1} (H : is-small l A) → A ≃ type-is-small H -equiv-is-small = pr2 + equiv-is-small : A ≃ type-is-small + equiv-is-small = pr2 H -inv-equiv-is-small : - {l l1 : Level} {A : UU l1} (H : is-small l A) → type-is-small H ≃ A -inv-equiv-is-small H = inv-equiv (equiv-is-small H) + inv-equiv-is-small : type-is-small ≃ A + inv-equiv-is-small = inv-equiv equiv-is-small -map-equiv-is-small : - {l l1 : Level} {A : UU l1} (H : is-small l A) → A → type-is-small H -map-equiv-is-small H = map-equiv (equiv-is-small H) + map-equiv-is-small : A → type-is-small + map-equiv-is-small = map-equiv equiv-is-small -map-inv-equiv-is-small : - {l l1 : Level} {A : UU l1} (H : is-small l A) → type-is-small H → A -map-inv-equiv-is-small H = map-inv-equiv (equiv-is-small H) + map-inv-equiv-is-small : type-is-small → A + map-inv-equiv-is-small = map-inv-equiv equiv-is-small ``` -### The universe of `UU l1`-small types in a universe `UU l2` +### The subuniverse of `UU l1`-small types in `UU l2` ```agda Small-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Small-Type l1 l2 = Σ (UU l2) (is-small l1) module _ - {l1 l2 : Level} (X : Small-Type l1 l2) + {l1 l2 : Level} (A : Small-Type l1 l2) where type-Small-Type : UU l2 - type-Small-Type = pr1 X + type-Small-Type = pr1 A is-small-type-Small-Type : is-small l1 type-Small-Type - is-small-type-Small-Type = pr2 X + is-small-type-Small-Type = pr2 A small-type-Small-Type : UU l1 small-type-Small-Type = type-is-small is-small-type-Small-Type - equiv-is-small-type-Small-Type : type-Small-Type ≃ small-type-Small-Type - equiv-is-small-type-Small-Type = equiv-is-small is-small-type-Small-Type + equiv-is-small-type-Small-Type : + type-Small-Type ≃ small-type-Small-Type + equiv-is-small-type-Small-Type = + equiv-is-small is-small-type-Small-Type ``` ## Properties @@ -148,8 +149,8 @@ is-small-lsuc {l} X = is-small-lmax (lsuc l) X is-small-equiv : {l1 l2 l3 : Level} {A : UU l1} (B : UU l2) → A ≃ B → is-small l3 B → is-small l3 A -pr1 (is-small-equiv B e (pair X h)) = X -pr2 (is-small-equiv B e (pair X h)) = h ∘e e +pr1 (is-small-equiv B e (X , h)) = X +pr2 (is-small-equiv B e (X , h)) = h ∘e e is-small-equiv' : {l1 l2 l3 : Level} (A : UU l1) {B : UU l2} → @@ -194,9 +195,9 @@ pr2 (is-small-is-contr l H) = equiv-is-contr H is-contr-raise-unit is-small-Σ : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} → is-small l3 A → ((x : A) → is-small l4 (B x)) → is-small (l3 ⊔ l4) (Σ A B) -pr1 (is-small-Σ {B = B} (pair X e) H) = +pr1 (is-small-Σ {B = B} (X , e) H) = Σ X (λ x → pr1 (H (map-inv-equiv e x))) -pr2 (is-small-Σ {B = B} (pair X e) H) = +pr2 (is-small-Σ {B = B} (X , e) H) = equiv-Σ ( λ x → pr1 (H (map-inv-equiv e x))) ( e) @@ -237,9 +238,9 @@ is-small-Π : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} → is-small l3 A → ((x : A) → is-small l4 (B x)) → is-small (l3 ⊔ l4) ((x : A) → B x) -pr1 (is-small-Π {B = B} (pair X e) H) = +pr1 (is-small-Π {B = B} (X , e) H) = (x : X) → pr1 (H (map-inv-equiv e x)) -pr2 (is-small-Π {B = B} (pair X e) H) = +pr2 (is-small-Π {B = B} (X , e) H) = equiv-Π ( λ (x : X) → pr1 (H (map-inv-equiv e x))) ( e) diff --git a/src/foundation-core/subtypes.lagda.md b/src/foundation-core/subtypes.lagda.md index 7605fae635..485127c4e8 100644 --- a/src/foundation-core/subtypes.lagda.md +++ b/src/foundation-core/subtypes.lagda.md @@ -79,6 +79,10 @@ module _ (x : type-subtype) → is-in-subtype (inclusion-subtype x) is-in-subtype-inclusion-subtype = pr2 + eq-is-in-subtype : + {x : A} {p q : is-in-subtype x} → p ＝ q + eq-is-in-subtype {x} = eq-is-prop (is-prop-is-in-subtype x) + is-closed-under-eq-subtype : {x y : A} → is-in-subtype x → (x ＝ y) → is-in-subtype y is-closed-under-eq-subtype p refl = p diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 55475184ff..ccb76b692d 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -51,6 +51,7 @@ open import foundation.commuting-squares-of-homotopies public open import foundation.commuting-squares-of-identifications public open import foundation.commuting-squares-of-maps public open import foundation.commuting-triangles-of-homotopies public +open import foundation.commuting-triangles-of-identifications public open import foundation.commuting-triangles-of-maps public open import foundation.complements public open import foundation.complements-subtypes public @@ -208,6 +209,7 @@ open import foundation.multivariable-functoriality-set-quotients public open import foundation.multivariable-homotopies public open import foundation.multivariable-operations public open import foundation.multivariable-relations public +open import foundation.multivariable-sections public open import foundation.negated-equality public open import foundation.negation public open import foundation.noncontractible-types public diff --git a/src/foundation/binary-homotopies.lagda.md b/src/foundation/binary-homotopies.lagda.md index f29459a7b5..75c57b18b3 100644 --- a/src/foundation/binary-homotopies.lagda.md +++ b/src/foundation/binary-homotopies.lagda.md @@ -9,6 +9,7 @@ module foundation.binary-homotopies where ```agda open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types +open import foundation.function-extensionality open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.universe-levels @@ -25,9 +26,9 @@ open import foundation-core.torsorial-type-families ## Idea Consider two binary operations `f g : (x : A) (y : B x) → C x y`. The type of -binary homotopies between `f` and `g` is defined to be the type of pointwise -identifications of `f` and `g`. We show that this characterizes the identity -type of `(x : A) (y : B x) → C x y`. +**binary homotopies** between `f` and `g` is defined to be the type of pointwise +[identifications](foundation-core.identity-types.md) of `f` and `g`. We show +that this characterizes the identity type of `(x : A) (y : B x) → C x y`. ## Definition @@ -71,3 +72,30 @@ module _ (f g : (x : A) (y : B x) → C x y) → binary-htpy f g → f ＝ g eq-binary-htpy f g = map-inv-equiv (extensionality-binary-Π f g) ``` + +## Properties + +### Binary homotopy is equivalent to function homotopy + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + where + + binary-htpy-htpy : + (f g : (x : A) (y : B x) → C x y) → (f ~ g) → binary-htpy f g + binary-htpy-htpy f g = + ind-htpy f (λ g H → binary-htpy f g) (refl-binary-htpy f) + + equiv-binary-htpy-htpy : + (f g : (x : A) (y : B x) → C x y) → (f ~ g) ≃ binary-htpy f g + equiv-binary-htpy-htpy f g = extensionality-binary-Π f g ∘e equiv-eq-htpy + + htpy-binary-htpy : + (f g : (x : A) (y : B x) → C x y) → binary-htpy f g → f ~ g + htpy-binary-htpy f g = map-inv-equiv (equiv-binary-htpy-htpy f g) + + equiv-htpy-binary-htpy : + (f g : (x : A) (y : B x) → C x y) → binary-htpy f g ≃ (f ~ g) + equiv-htpy-binary-htpy f g = inv-equiv (equiv-binary-htpy-htpy f g) +``` diff --git a/src/foundation/commuting-triangles-of-identifications.lagda.md b/src/foundation/commuting-triangles-of-identifications.lagda.md new file mode 100644 index 0000000000..540eeebbce --- /dev/null +++ b/src/foundation/commuting-triangles-of-identifications.lagda.md @@ -0,0 +1,49 @@ +# Commuting triangles of identifications + +```agda +module foundation.commuting-triangles-of-identifications where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.universe-levels + +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +``` + +
+ +## Idea + +A triangle of [identifications](foundation-core.identity-types.md) + +```text + x ----- y + \ / + \ / + \ / + z +``` + +is said to **commute** if there is a higher identification between the `x ＝ z` +and the concatenated identification `x ＝ y ＝ z`. + +## Definition + +```agda +module _ + {l : Level} {A : UU l} {x y z : A} + where + + coherence-triangle-identifications : + (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l + coherence-triangle-identifications left right top = left ＝ (top ∙ right) + + coherence-triangle-identifications' : + (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l + coherence-triangle-identifications' left right top = (top ∙ right) ＝ left +``` diff --git a/src/foundation/decidable-equality.lagda.md b/src/foundation/decidable-equality.lagda.md index 4fff5f35d7..8f062245cb 100644 --- a/src/foundation/decidable-equality.lagda.md +++ b/src/foundation/decidable-equality.lagda.md @@ -147,6 +147,9 @@ abstract ### Hedberg's theorem +**Hedberg's theorem** asserts that types with decidable equality are +[sets](foundation-core.sets.md). + ```agda module _ {l : Level} {A : UU l} diff --git a/src/foundation/decidable-types.lagda.md b/src/foundation/decidable-types.lagda.md index eda27cab02..fe561f31d9 100644 --- a/src/foundation/decidable-types.lagda.md +++ b/src/foundation/decidable-types.lagda.md @@ -31,11 +31,14 @@ open import foundation-core.retractions ## Idea -A type is said to be decidable if we can either construct an element, or we can -prove that it is empty. In other words, we interpret decidability via the -Curry-Howard interpretation of logic into type theory. A related concept is that -a type is either inhabited or empty, where inhabitedness of a type is expressed -using the propositional truncation. +A type is said to be **decidable** if we can either construct an element, or we +can prove that it is [empty](foundation-core.empty-types.md). In other words, we +interpret decidability via the +[Curry-Howard interpretation](https://en.wikipedia.org/wiki/Curry–Howard_correspondence) +of logic into type theory. A related concept is that a type is either +[inhabited](foundation.inhabited-types.md) or empty, where inhabitedness of a +type is expressed using the +[propositional truncation](foundation.propositional-truncations.md). ## Definition diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md index 2bd03a7af5..9ba0f5f24e 100644 --- a/src/foundation/double-negation-modality.lagda.md +++ b/src/foundation/double-negation-modality.lagda.md @@ -28,6 +28,8 @@ The [double negation](foundation.double-negation.md) operation `¬¬` is a ## Definition +### The double negation modality + ```agda operator-double-negation-modality : (l : Level) → operator-modality l l @@ -46,7 +48,7 @@ unit-double-negation-modality = intro-double-negation is-uniquely-eliminating-modality-double-negation-modality : {l : Level} → is-uniquely-eliminating-modality (unit-double-negation-modality {l}) -is-uniquely-eliminating-modality-double-negation-modality {l} A P = +is-uniquely-eliminating-modality-double-negation-modality {l} {A} P = is-local-dependent-type-is-prop ( unit-double-negation-modality) ( operator-double-negation-modality l ∘ P) diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index 79aa2a9bfb..ca5378e4b1 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -549,6 +549,12 @@ module _ ( ap ( λ g → map-equiv (f ∘e (g ∘e (inv-equiv f))) x) ( inv (right-inverse-law-equiv e))))) + + distributive-map-inv-comp-equiv : + (e : X ≃ Y) (f : Y ≃ Z) → + map-inv-equiv (f ∘e e) ＝ map-inv-equiv e ∘ map-inv-equiv f + distributive-map-inv-comp-equiv e f = + ap map-equiv (distributive-inv-comp-equiv e f) ``` #### Iterated inverse laws for equivalence composition diff --git a/src/foundation/images.lagda.md b/src/foundation/images.lagda.md index 5217741cd1..9a7edc62e9 100644 --- a/src/foundation/images.lagda.md +++ b/src/foundation/images.lagda.md @@ -8,6 +8,7 @@ module foundation.images where ```agda open import foundation.dependent-pair-types +open import foundation.function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.propositional-truncations open import foundation.slice @@ -60,7 +61,7 @@ module _ map-unit-im : A → im pr1 (map-unit-im a) = f a - pr2 (map-unit-im a) = unit-trunc-Prop (pair a refl) + pr2 (map-unit-im a) = unit-trunc-Prop (a , refl) triangle-unit-im : coherence-triangle-maps f inclusion-im map-unit-im triangle-unit-im a = refl @@ -121,8 +122,7 @@ abstract is-emb-inclusion-im : {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → is-emb (inclusion-im f) - is-emb-inclusion-im f = - is-emb-inclusion-subtype (λ x → trunc-Prop (fiber f x)) + is-emb-inclusion-im f = is-emb-inclusion-subtype (trunc-Prop ∘ fiber f) emb-im : {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → im f ↪ X @@ -137,8 +137,7 @@ abstract is-injective-inclusion-im : {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → is-injective (inclusion-im f) - is-injective-inclusion-im f = - is-injective-is-emb (is-emb-inclusion-im f) + is-injective-inclusion-im f = is-injective-is-emb (is-emb-inclusion-im f) ``` ### The unit map of the image is surjective @@ -148,15 +147,13 @@ abstract is-surjective-map-unit-im : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-surjective (map-unit-im f) - is-surjective-map-unit-im f (pair y z) = + is-surjective-map-unit-im f (y , z) = apply-universal-property-trunc-Prop z - ( trunc-Prop (fiber (map-unit-im f) (pair y z))) + ( trunc-Prop (fiber (map-unit-im f) (y , z))) ( α) where - α : fiber f y → type-Prop (trunc-Prop (fiber (map-unit-im f) (pair y z))) - α (pair x p) = - unit-trunc-Prop - ( pair x (eq-type-subtype (λ z → trunc-Prop (fiber f z)) p)) + α : fiber f y → type-Prop (trunc-Prop (fiber (map-unit-im f) (y , z))) + α (x , p) = unit-trunc-Prop (x , eq-type-subtype (trunc-Prop ∘ fiber f) p) ``` ### The image of a map into a truncated type is truncated @@ -167,6 +164,12 @@ abstract {l1 l2 : Level} (k : 𝕋) {X : UU l1} {A : UU l2} (f : A → X) → is-trunc (succ-𝕋 k) X → is-trunc (succ-𝕋 k) (im f) is-trunc-im k f = is-trunc-emb k (emb-im f) + +im-Truncated-Type : + {l1 l2 : Level} (k : 𝕋) (X : Truncated-Type l1 (succ-𝕋 k)) {A : UU l2} + (f : A → type-Truncated-Type X) → Truncated-Type (l1 ⊔ l2) (succ-𝕋 k) +pr1 (im-Truncated-Type k X f) = im f +pr2 (im-Truncated-Type k X f) = is-trunc-im k f (is-trunc-type-Truncated-Type X) ``` ### The image of a map into a proposition is a proposition @@ -177,6 +180,11 @@ abstract {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → is-prop X → is-prop (im f) is-prop-im = is-trunc-im neg-two-𝕋 + +im-Prop : + {l1 l2 : Level} (X : Prop l1) {A : UU l2} + (f : A → type-Prop X) → Prop (l1 ⊔ l2) +im-Prop X f = im-Truncated-Type neg-two-𝕋 X f ``` ### The image of a map into a set is a set @@ -189,10 +197,9 @@ abstract is-set-im = is-trunc-im neg-one-𝕋 im-Set : - {l1 l2 : Level} {A : UU l2} (X : Set l1) (f : A → type-Set X) → - Set (l1 ⊔ l2) -pr1 (im-Set X f) = im f -pr2 (im-Set X f) = is-set-im f (is-set-type-Set X) + {l1 l2 : Level} (X : Set l1) {A : UU l2} + (f : A → type-Set X) → Set (l1 ⊔ l2) +im-Set X f = im-Truncated-Type (neg-one-𝕋) X f ``` ### The image of a map into a 1-type is a 1-type @@ -205,8 +212,7 @@ abstract is-1-type-im = is-trunc-im zero-𝕋 im-1-Type : - {l1 l2 : Level} {A : UU l2} (X : 1-Type l1) + {l1 l2 : Level} (X : 1-Type l1) {A : UU l2} (f : A → type-1-Type X) → 1-Type (l1 ⊔ l2) -pr1 (im-1-Type X f) = im f -pr2 (im-1-Type X f) = is-1-type-im f (is-1-type-type-1-Type X) +im-1-Type X f = im-Truncated-Type zero-𝕋 X f ``` diff --git a/src/foundation/iterated-dependent-product-types.lagda.md b/src/foundation/iterated-dependent-product-types.lagda.md index e8a3bb5631..0d4263d469 100644 --- a/src/foundation/iterated-dependent-product-types.lagda.md +++ b/src/foundation/iterated-dependent-product-types.lagda.md @@ -55,12 +55,13 @@ of universe level `l₀ ⊔ l₁ ⊔ l₂ ⊔ l₃`. iterated-Π : {l : Level} {n : ℕ} → telescope l n → UU l iterated-Π (base-telescope A) = A -iterated-Π (cons-telescope A) = (x : _) → iterated-Π (A x) +iterated-Π (cons-telescope {X = X} A) = (x : X) → iterated-Π (A x) iterated-implicit-Π : {l : Level} {n : ℕ} → telescope l n → UU l iterated-implicit-Π (base-telescope A) = A -iterated-implicit-Π (cons-telescope A) = {x : _} → iterated-implicit-Π (A x) +iterated-implicit-Π (cons-telescope {X = X} A) = + {x : X} → iterated-implicit-Π (A x) ``` ### Iterated sections of type families diff --git a/src/foundation/law-of-excluded-middle.lagda.md b/src/foundation/law-of-excluded-middle.lagda.md index 2b19911c5f..d28bb30393 100644 --- a/src/foundation/law-of-excluded-middle.lagda.md +++ b/src/foundation/law-of-excluded-middle.lagda.md @@ -22,7 +22,9 @@ open import univalent-combinatorics.2-element-types ## Idea -The law of excluded middle asserts that any proposition `P` is decidable. +The **law of excluded middle** asserts that any +[proposition](foundation-core.propositions.md) `P` is +[decidable](foundation.decidable-types.md). ## Definition diff --git a/src/foundation/locally-small-types.lagda.md b/src/foundation/locally-small-types.lagda.md index a4835728c8..bbebd0d8db 100644 --- a/src/foundation/locally-small-types.lagda.md +++ b/src/foundation/locally-small-types.lagda.md @@ -31,17 +31,40 @@ open import foundation-core.truncation-levels ## Idea -A type is said to be locally small if its identity types are small. +A type is said to be **locally small** with respect to a universe `UU l` if its +[identity types](foundation-core.identity-types.md) are +[small](foundation-core.small-types.md) with respect to that universe. ## Definition +### Locally small types + ```agda is-locally-small : (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1) is-locally-small l A = (x y : A) → is-small l (x ＝ y) + +module _ + {l l1 : Level} {A : UU l1} (H : is-locally-small l A) (x y : A) + where + + type-is-locally-small : UU l + type-is-locally-small = pr1 (H x y) + + equiv-is-locally-small : (x ＝ y) ≃ type-is-locally-small + equiv-is-locally-small = pr2 (H x y) + + inv-equiv-is-locally-small : type-is-locally-small ≃ (x ＝ y) + inv-equiv-is-locally-small = inv-equiv equiv-is-locally-small + + map-equiv-is-locally-small : (x ＝ y) → type-is-locally-small + map-equiv-is-locally-small = map-equiv equiv-is-locally-small + + map-inv-equiv-is-locally-small : type-is-locally-small → (x ＝ y) + map-inv-equiv-is-locally-small = map-inv-equiv equiv-is-locally-small ``` -### The type of locally small types +### The subuniverse of `UU l1`-locally small types in `UU l2` ```agda Locally-Small-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) @@ -57,6 +80,17 @@ module _ is-locally-small-type-Locally-Small-Type : is-locally-small l1 type-Locally-Small-Type is-locally-small-type-Locally-Small-Type = pr2 A + + small-identity-type-Locally-Small-Type : + (x y : type-Locally-Small-Type) → UU l1 + small-identity-type-Locally-Small-Type = + type-is-locally-small is-locally-small-type-Locally-Small-Type + + equiv-is-locally-small-type-Locally-Small-Type : + (x y : type-Locally-Small-Type) → + (x ＝ y) ≃ small-identity-type-Locally-Small-Type x y + equiv-is-locally-small-type-Locally-Small-Type = + equiv-is-locally-small is-locally-small-type-Locally-Small-Type ``` ## Properties diff --git a/src/foundation/multivariable-homotopies.lagda.md b/src/foundation/multivariable-homotopies.lagda.md index a5aaf2529f..1ca939ec6e 100644 --- a/src/foundation/multivariable-homotopies.lagda.md +++ b/src/foundation/multivariable-homotopies.lagda.md @@ -13,6 +13,7 @@ open import elementary-number-theory.natural-numbers open import foundation.equivalences open import foundation.function-extensionality +open import foundation.homotopies open import foundation.iterated-dependent-product-types open import foundation.universe-levels @@ -39,8 +40,8 @@ to [identifications](foundation-core.identity-types.md). multivariable-htpy : {l : Level} {n : ℕ} {{A : telescope l n}} (f g : iterated-Π A) → UU l multivariable-htpy {{base-telescope A}} f g = f ＝ g -multivariable-htpy {{cons-telescope A}} f g = - (x : _) → multivariable-htpy {{A x}} (f x) (g x) +multivariable-htpy {{cons-telescope {X = X} A}} f g = + (x : X) → multivariable-htpy {{A x}} (f x) (g x) ``` ### Multivariable homotopies between implicit functions @@ -83,6 +84,12 @@ equiv-iterated-funext : equiv-iterated-funext .0 {{base-telescope A}} = id-equiv equiv-iterated-funext ._ {{cons-telescope A}} = equiv-Π-equiv-family (λ x → equiv-iterated-funext _ {{A x}}) ∘e equiv-funext + +equiv-eq-multivariable-htpy : + {l : Level} (n : ℕ) {{A : telescope l n}} + {f g : iterated-Π A} → multivariable-htpy {{A}} f g ≃ (f ＝ g) +equiv-eq-multivariable-htpy n {{A}} {f} {g} = + inv-equiv (equiv-iterated-funext n {{A}} {f} {g}) ``` ### Iterated function extensionality for implicit functions diff --git a/src/foundation/multivariable-sections.lagda.md b/src/foundation/multivariable-sections.lagda.md new file mode 100644 index 0000000000..b8f4cc2855 --- /dev/null +++ b/src/foundation/multivariable-sections.lagda.md @@ -0,0 +1,92 @@ +# Multivariable sections + +```agda +module foundation.multivariable-sections where + +open import foundation.telescopes public +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.binary-homotopies +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.iterated-dependent-product-types +open import foundation.multivariable-homotopies +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.sections +open import foundation-core.whiskering-homotopies +``` + +
+ +## Idea + +A **multivariable section** is a map of multivariable maps that is a right +inverse. Thus, a map + +```text + s : ((x₁ : A₁) ... (xₙ : Aₙ) → A x) → (y₁ : B₁) ... (yₙ : Bₙ) → B y +``` + +is a section of a map of type + +```text + f : ((y₁ : B₁) ... (yₙ : Bₙ) → B y) → (x₁ : A₁) ... (xₙ : Aₙ) → A x +``` + +if the composition `f ∘ s` is +[multivariable homotopic](foundation.multivariable-homotopies.md) to the +identity at + +```text + (y₁ : B₁) ... (yₙ : Bₙ) → B y. +``` + +Note that sections of multivariable maps are equivalent to common +[sections](foundation-core.sections.md) by function extensionality, so this +definition only finds it utility in avoiding unnecessary applications of +[function extensionality](foundation.function-extensionality.md). For instance, +this is useful when defining induction principles on function types. + +## Definition + +```agda +module _ + {l1 l2 : Level} (n : ℕ) + {{A : telescope l1 n}} {{B : telescope l2 n}} + (f : iterated-Π A → iterated-Π B) + where + + multivariable-section : UU (l1 ⊔ l2) + multivariable-section = + Σ ( iterated-Π B → iterated-Π A) + ( λ s → + multivariable-htpy + { n = succ-ℕ n} + {{A = prepend-telescope (iterated-Π B) B}} + ( f ∘ s) + ( id)) + + map-multivariable-section : + multivariable-section → iterated-Π B → iterated-Π A + map-multivariable-section = pr1 + + is-multivariable-section-map-multivariable-section : + (s : multivariable-section) → + multivariable-htpy + { n = succ-ℕ n} + {{A = prepend-telescope (iterated-Π B) B}} + ( f ∘ map-multivariable-section s) + ( id) + is-multivariable-section-map-multivariable-section = pr2 +``` diff --git a/src/foundation/telescopes.lagda.md b/src/foundation/telescopes.lagda.md index 6f981e3dee..a6d3fecbce 100644 --- a/src/foundation/telescopes.lagda.md +++ b/src/foundation/telescopes.lagda.md @@ -63,6 +63,35 @@ data open telescope public ``` +A very slight reformulation of `cons-telescope` for convenience: + +```agda +prepend-telescope : + {l1 l2 : Level} {n : ℕ} → + (A : UU l1) → ({x : A} → telescope l2 n) → telescope (l1 ⊔ l2) (succ-ℕ n) +prepend-telescope A B = cons-telescope {X = A} (λ x → B {x}) +``` + +### Telescopes at a universe level + +One issue with the previous definition of telescopes is that it is impossible to +extract any type information from it. At the expense of giving up full universe +polymorphism, we can define a notion of **telescopes at a universe level** that +admits such projections. This definition is also compatible with the +`--level-universe` restriction. + +```agda +data telescope-Level (l : Level) : ℕ → UU (lsuc l) + where + base-telescope-Level : + UU l → telescope-Level l 0 + cons-telescope-Level : + {n : ℕ} {X : UU l} → + (X → telescope-Level l n) → telescope-Level l (succ-ℕ n) + +open telescope-Level public +``` + ### Transformations on telescopes Given an operation on universes, we can apply it at the base of the telescope. diff --git a/src/foundation/torsorial-type-families.lagda.md b/src/foundation/torsorial-type-families.lagda.md index 14492d9b3a..dc2079c439 100644 --- a/src/foundation/torsorial-type-families.lagda.md +++ b/src/foundation/torsorial-type-families.lagda.md @@ -68,7 +68,7 @@ module _ ## Properties -#### `fib Id B ≃ is-torsorial B` for any type family `B` over `A` +### `fiber Id B ≃ is-torsorial B` for any type family `B` over `A` In other words, a type family `B` over `A` is in the [image](foundation.images.md) of `Id : A → (A → 𝒰)` if and only if `B` is @@ -84,29 +84,29 @@ module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where - is-torsorial-fib-Id : + is-torsorial-fiber-Id : {a : A} → ((x : A) → (a ＝ x) ≃ B x) → is-torsorial B - is-torsorial-fib-Id H = + is-torsorial-fiber-Id H = fundamental-theorem-id' ( λ x → map-equiv (H x)) ( λ x → is-equiv-map-equiv (H x)) - fib-Id-is-torsorial : + fiber-Id-is-torsorial : is-torsorial B → Σ A (λ a → (x : A) → (a ＝ x) ≃ B x) - pr1 (fib-Id-is-torsorial ((a , b) , H)) = a - pr2 (fib-Id-is-torsorial ((a , b) , H)) = + pr1 (fiber-Id-is-torsorial ((a , b) , H)) = a + pr2 (fiber-Id-is-torsorial ((a , b) , H)) = map-inv-distributive-Π-Σ (f , fundamental-theorem-id ((a , b) , H) f) where f : (x : A) → (a ＝ x) → B x f x refl = b - compute-fib-Id : + compute-fiber-Id : (Σ A (λ a → (x : A) → (a ＝ x) ≃ B x)) ≃ is-torsorial B - compute-fib-Id = + compute-fiber-Id = equiv-iff ( Σ A (λ a → (x : A) → (a ＝ x) ≃ B x) , is-prop-total-family-of-equivalences-Id) ( is-contr-Prop (Σ A B)) - ( λ u → is-torsorial-fib-Id (pr2 u)) - ( fib-Id-is-torsorial) + ( λ u → is-torsorial-fiber-Id (pr2 u)) + ( fiber-Id-is-torsorial) ``` diff --git a/src/foundation/truncation-modalities.lagda.md b/src/foundation/truncation-modalities.lagda.md index a11c518ea6..4c38c783fb 100644 --- a/src/foundation/truncation-modalities.lagda.md +++ b/src/foundation/truncation-modalities.lagda.md @@ -44,6 +44,6 @@ unit-trunc-modality = unit-trunc is-uniquely-eliminating-modality-trunc-modality : {l : Level} {k : 𝕋} → is-uniquely-eliminating-modality (unit-trunc-modality {l} {k}) -is-uniquely-eliminating-modality-trunc-modality {k = k} A P = +is-uniquely-eliminating-modality-trunc-modality {k = k} P = dependent-universal-property-trunc (trunc k ∘ P) ``` diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md index d0f561ec71..14343bbb08 100644 --- a/src/foundation/univalence.lagda.md +++ b/src/foundation/univalence.lagda.md @@ -197,8 +197,8 @@ commutativity-inv-eq-equiv A B f = ( equiv-univalence) ( ( inv (commutativity-inv-equiv-eq A B (eq-equiv A B f))) ∙ ( ( ap - ( λ e → (inv-equiv (map-equiv e f))) - ( right-inverse-law-equiv equiv-univalence)) ∙ + ( λ e → (inv-equiv (map-equiv e f))) + ( right-inverse-law-equiv equiv-univalence)) ∙ ( ap ( λ e → map-equiv e (inv-equiv f)) ( inv (right-inverse-law-equiv equiv-univalence))))) diff --git a/src/modal-type-theory.lagda.md b/src/modal-type-theory.lagda.md new file mode 100644 index 0000000000..073d022d0e --- /dev/null +++ b/src/modal-type-theory.lagda.md @@ -0,0 +1,22 @@ +# Modal type theory + +```agda +{-# OPTIONS --cohesion --flat-split #-} +``` + +## Files in the modal type theory folder + +```agda +module modal-type-theory where + +open import modal-type-theory.crisp-identity-types public +open import modal-type-theory.crisp-law-of-excluded-middle public +open import modal-type-theory.flat-dependent-function-types public +open import modal-type-theory.flat-dependent-pair-types public +open import modal-type-theory.flat-discrete-types public +open import modal-type-theory.flat-modality public +open import modal-type-theory.flat-sharp-adjunction public +open import modal-type-theory.sharp-codiscrete-maps public +open import modal-type-theory.sharp-codiscrete-types public +open import modal-type-theory.sharp-modality public +``` diff --git a/src/modal-type-theory/crisp-identity-types.lagda.md b/src/modal-type-theory/crisp-identity-types.lagda.md new file mode 100644 index 0000000000..87b191d9dc --- /dev/null +++ b/src/modal-type-theory/crisp-identity-types.lagda.md @@ -0,0 +1,37 @@ +# Crisp identity types + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.crisp-identity-types where +``` + +
Imports + +```agda +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +We record here some basic facts about +[identity types](foundation-core.identity-types.md) in crisp contexts. + +## Properties + +```agda +ind-path-crisp : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {@♭ a : A} → + (C : (@♭ y : A) (p : a ＝ y) → UU l2) → + C a refl → + (@♭ y : A) (@♭ p : a ＝ y) → C y p +ind-path-crisp C b _ refl = b + +ap-crisp : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {B : UU l2} {@♭ x y : A} + (f : (@♭ x : A) → B) → @♭ (x ＝ y) → (f x) ＝ (f y) +ap-crisp f refl = refl +``` diff --git a/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md b/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md new file mode 100644 index 0000000000..6770f4d7f0 --- /dev/null +++ b/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md @@ -0,0 +1,50 @@ +# The crisp law of excluded middle + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.crisp-law-of-excluded-middle where +``` + +
Imports + +```agda +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.decidable-propositions +open import foundation-core.negation +open import foundation-core.propositions +``` + +
+ +## Idea + +The **crisp law of excluded middle** asserts that any crisp +[proposition](foundation-core.propositions.md) `P` is +[decidable](foundation.decidable-types.md). + +## Definition + +```agda +Crisp-LEM : (@♭ l : Level) → UU (lsuc l) +Crisp-LEM l = (@♭ P : Prop l) → is-decidable (type-Prop P) +``` + +## Properties + +### Given crisp LEM, we obtain a map from crisp propositions to decidable propositions + +```agda +decidable-prop-Crisp-Prop : + {@♭ l : Level} → Crisp-LEM l → @♭ Prop l → Decidable-Prop l +pr1 (decidable-prop-Crisp-Prop lem P) = type-Prop P +pr1 (pr2 (decidable-prop-Crisp-Prop lem P)) = is-prop-type-Prop P +pr2 (pr2 (decidable-prop-Crisp-Prop lem P)) = lem P +``` + +## See also + +- [The law of excluded middle](foundation.law-of-excluded-middle.md) diff --git a/src/modal-type-theory/flat-dependent-function-types.lagda.md b/src/modal-type-theory/flat-dependent-function-types.lagda.md new file mode 100644 index 0000000000..0ced757ebe --- /dev/null +++ b/src/modal-type-theory/flat-dependent-function-types.lagda.md @@ -0,0 +1,66 @@ +# Flat dependent function types + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.flat-dependent-function-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.retractions +open import foundation.sections +open import foundation.universe-levels + +open import modal-type-theory.flat-modality +``` + +
+ +## Idea + +We study interactions between the +[flat modality](modal-type-theory.flat-modality.md) and +[dependent function types](foundation.function-types.md). + +## Properties + +### Flat distributes over dependent function types + +```agda +module _ + {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2} + where + + map-crisp-distributive-flat-Π : ♭ ((x : A) → B x) → ((@♭ x : A) → ♭ (B x)) + map-crisp-distributive-flat-Π (cons-flat f) x = cons-flat (f x) + +module _ + {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} + where + + map-crisp-distributive-flat-function-types : ♭ (A → B) → (@♭ A → ♭ B) + map-crisp-distributive-flat-function-types = map-crisp-distributive-flat-Π + + map-distributive-flat-function-types : ♭ (A → B) → (♭ A → ♭ B) + map-distributive-flat-function-types f (cons-flat x) = + map-crisp-distributive-flat-function-types f x +``` + +## See also + +- [Flat discrete types](modal-type-theory.flat-discrete-types.md) for types that + are flat modal. + +## References + +- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type + theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584)) +- Dan Licata, _cohesion-agda_, GitHub repository + () diff --git a/src/modal-type-theory/flat-dependent-pair-types.lagda.md b/src/modal-type-theory/flat-dependent-pair-types.lagda.md new file mode 100644 index 0000000000..3e6cf4e8dc --- /dev/null +++ b/src/modal-type-theory/flat-dependent-pair-types.lagda.md @@ -0,0 +1,93 @@ +# Flat dependent pair types + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.flat-dependent-pair-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.retractions +open import foundation.sections +open import foundation.universe-levels + +open import modal-type-theory.flat-modality +``` + +
+ +## Idea + +We study interactions between the +[flat modality](modal-type-theory.flat-modality.md) and +[dependent pair types](foundation.dependent-pair-types.md). + +## Definitions + +```agda +Σ-♭ : {@♭ l1 l2 : Level} (@♭ A : UU l1) (@♭ B : A → UU l2) → UU (l1 ⊔ l2) +Σ-♭ A B = Σ (♭ A) (λ where (cons-flat x) → ♭ (B x)) +``` + +## Properties + +### Flat distributes over Σ-types + +```agda +module _ + {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2} + where + + map-distributive-flat-Σ : ♭ (Σ A B) → Σ-♭ A B + pr1 (map-distributive-flat-Σ (cons-flat (x , y))) = cons-flat x + pr2 (map-distributive-flat-Σ (cons-flat (x , y))) = cons-flat y + + map-inv-distributive-flat-Σ : Σ-♭ A B → ♭ (Σ A B) + map-inv-distributive-flat-Σ (cons-flat x , cons-flat y) = cons-flat (x , y) + + is-section-distributive-flat-Σ : + (map-inv-distributive-flat-Σ ∘ map-distributive-flat-Σ) ~ id + is-section-distributive-flat-Σ (cons-flat _) = refl + + is-retraction-distributive-flat-Σ : + (map-distributive-flat-Σ ∘ map-inv-distributive-flat-Σ) ~ id + is-retraction-distributive-flat-Σ (cons-flat _ , cons-flat _) = refl + + section-distributive-flat-Σ : section map-distributive-flat-Σ + pr1 section-distributive-flat-Σ = map-inv-distributive-flat-Σ + pr2 section-distributive-flat-Σ = is-retraction-distributive-flat-Σ + + retraction-distributive-flat-Σ : retraction map-distributive-flat-Σ + pr1 retraction-distributive-flat-Σ = map-inv-distributive-flat-Σ + pr2 retraction-distributive-flat-Σ = is-section-distributive-flat-Σ + + is-equiv-distributive-flat-Σ : is-equiv map-distributive-flat-Σ + pr1 is-equiv-distributive-flat-Σ = section-distributive-flat-Σ + pr2 is-equiv-distributive-flat-Σ = retraction-distributive-flat-Σ + + equiv-distributive-flat-Σ : ♭ (Σ A B) ≃ Σ-♭ A B + pr1 equiv-distributive-flat-Σ = map-distributive-flat-Σ + pr2 equiv-distributive-flat-Σ = is-equiv-distributive-flat-Σ + + inv-equiv-distributive-flat-Σ : Σ-♭ A B ≃ ♭ (Σ A B) + inv-equiv-distributive-flat-Σ = inv-equiv equiv-distributive-flat-Σ +``` + +## See also + +- [Flat discrete types](modal-type-theory.flat-discrete-types.md) for types that + are flat modal. + +## References + +- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type + theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584)) +- Dan Licata, _cohesion-agda_, GitHub repository + () diff --git a/src/modal-type-theory/flat-discrete-types.lagda.md b/src/modal-type-theory/flat-discrete-types.lagda.md new file mode 100644 index 0000000000..1a8de9a979 --- /dev/null +++ b/src/modal-type-theory/flat-discrete-types.lagda.md @@ -0,0 +1,100 @@ +# Flat discrete types + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.flat-discrete-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.propositions +open import foundation.unit-type +open import foundation.universe-levels + +open import modal-type-theory.flat-modality +``` + +
+ +## Idea + +A crisp type is said to be **(flat) discrete** if it is +[flat](modal-type-theory.flat-modality.md) modal, i.e. if the flat counit at +that type is an [equivalence](foundation-core.equivalences.md). + +## Definition + +```agda +is-flat-discrete : {@♭ l : Level} (@♭ A : UU l) → UU l +is-flat-discrete {l} A = is-equiv (counit-flat {l} {A}) +``` + +## Properties + +### Being flat is a property + +```agda +is-property-is-flat-discrete : + {@♭ l : Level} (@♭ A : UU l) → is-prop (is-flat-discrete A) +is-property-is-flat-discrete {l} A = is-property-is-equiv (counit-flat {l} {A}) + +is-flat-discrete-Prop : {@♭ l : Level} (@♭ A : UU l) → Prop l +is-flat-discrete-Prop {l} A = is-equiv-Prop (counit-flat {l} {A}) +``` + +### The empty type is flat + +```agda +map-is-flat-discrete-empty : empty → ♭ empty +map-is-flat-discrete-empty () + +is-section-map-is-flat-discrete-empty : + (counit-flat ∘ map-is-flat-discrete-empty) ~ id +is-section-map-is-flat-discrete-empty () + +is-retraction-map-is-flat-discrete-empty : + (map-is-flat-discrete-empty ∘ counit-flat) ~ id +is-retraction-map-is-flat-discrete-empty (cons-flat ()) + +is-flat-discrete-empty : is-flat-discrete empty +is-flat-discrete-empty = + is-equiv-is-invertible + ( map-is-flat-discrete-empty) + ( is-section-map-is-flat-discrete-empty) + ( is-retraction-map-is-flat-discrete-empty) +``` + +### The unit type is flat + +```agda +map-is-flat-discrete-unit : unit → ♭ unit +map-is-flat-discrete-unit star = cons-flat star + +is-section-map-is-flat-discrete-unit : + counit-flat ∘ map-is-flat-discrete-unit ~ id +is-section-map-is-flat-discrete-unit _ = refl + +is-retraction-map-is-flat-discrete-unit : + map-is-flat-discrete-unit ∘ counit-flat ~ id +is-retraction-map-is-flat-discrete-unit (cons-flat _) = refl + +is-flat-discrete-unit : is-flat-discrete unit +is-flat-discrete-unit = + is-equiv-is-invertible + ( map-is-flat-discrete-unit) + ( is-section-map-is-flat-discrete-unit) + ( is-retraction-map-is-flat-discrete-unit) +``` + +## See also + +- [Sharp codiscrete types](modal-type-theory.sharp-codiscrete-types.md) for the + dual notion. diff --git a/src/modal-type-theory/flat-modality.lagda.md b/src/modal-type-theory/flat-modality.lagda.md new file mode 100644 index 0000000000..56863c0e9c --- /dev/null +++ b/src/modal-type-theory/flat-modality.lagda.md @@ -0,0 +1,175 @@ +# The flat modality + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.flat-modality where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.retractions +open import foundation.sections +open import foundation.universe-levels +``` + +
+ +## Idea + +The **flat modality** is an axiomatized comonadic modality we adjoin to our type +theory by use of _crisp type theory_. + +## Definition + +### The flat operator on types + +```agda +data ♭ {@♭ l : Level} (@♭ A : UU l) : UU l where + cons-flat : @♭ A → ♭ A +``` + +### The flat counit + +```agda +counit-crisp : {@♭ l : Level} {@♭ A : UU l} → @♭ A → A +counit-crisp x = x + +counit-flat : {@♭ l : Level} {@♭ A : UU l} → ♭ A → A +counit-flat (cons-flat x) = counit-crisp x +``` + +### Flat dependent elimination + +```agda +ind-flat : + {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level} (C : ♭ A → UU l2) → + ((@♭ u : A) → C (cons-flat u)) → + (x : ♭ A) → C x +ind-flat C f (cons-flat x) = f x + +crisp-ind-flat : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : @♭ ♭ A → UU l2) → + ((@♭ u : A) → C (cons-flat u)) → (@♭ x : ♭ A) → C x +crisp-ind-flat C f (cons-flat x) = f x +``` + +### Flat elimination + +```agda +rec-flat : + {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level} (C : UU l2) → + ((@♭ u : A) → C) → (x : ♭ A) → C +rec-flat C = ind-flat (λ _ → C) + +crisp-rec-flat : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : UU l2) → + ((@♭ u : A) → C) → (@♭ x : ♭ A) → C +crisp-rec-flat C = crisp-ind-flat (λ _ → C) +``` + +### Flat action on maps + +```agda +module _ + {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} + where + + ap-flat : @♭ (A → B) → (♭ A → ♭ B) + ap-flat f (cons-flat x) = cons-flat (f x) + + ap-crisp-flat : @♭ (@♭ A → B) → (♭ A → ♭ B) + ap-crisp-flat f (cons-flat x) = cons-flat (f x) + + coap-flat : (♭ A → ♭ B) → (@♭ A → B) + coap-flat f x = counit-flat (f (cons-flat x)) + + is-crisp-retraction-coap-flat : + (@♭ f : @♭ A → B) → coap-flat (ap-crisp-flat f) ＝ f + is-crisp-retraction-coap-flat _ = refl +``` + +## Properties + +### Crisp assumptions are weaker + +```agda +crispen : + {@♭ l1 l2 : Level} {@♭ A : UU l1} {P : A → UU l2} → + ((x : A) → P x) → ((@♭ x : A) → P x) +crispen f x = f x +``` + +### The flat modality is idempotent + +```agda +module _ + {@♭ l : Level} {@♭ A : UU l} + where + + is-crisp-section-cons-flat : (@♭ x : A) → counit-flat (cons-flat x) ＝ x + is-crisp-section-cons-flat _ = refl + + is-crisp-retraction-cons-flat : (@♭ x : ♭ A) → cons-flat (counit-flat x) ＝ x + is-crisp-retraction-cons-flat (cons-flat _) = refl +``` + +```agda +module _ + {@♭ l : Level} {@♭ A : UU l} + where + + map-flat-counit-flat : ♭ (♭ A) → ♭ A + map-flat-counit-flat (cons-flat x) = x + + diagonal-flat : ♭ A → ♭ (♭ A) + diagonal-flat (cons-flat x) = cons-flat (cons-flat x) + + is-section-flat-counit-flat : + diagonal-flat ∘ map-flat-counit-flat ~ id + is-section-flat-counit-flat (cons-flat (cons-flat _)) = refl + + is-retraction-flat-counit-flat : + map-flat-counit-flat ∘ diagonal-flat ~ id + is-retraction-flat-counit-flat (cons-flat _) = refl + + section-flat-counit-flat : section map-flat-counit-flat + pr1 section-flat-counit-flat = diagonal-flat + pr2 section-flat-counit-flat = is-retraction-flat-counit-flat + + retraction-flat-counit-flat : retraction map-flat-counit-flat + pr1 retraction-flat-counit-flat = diagonal-flat + pr2 retraction-flat-counit-flat = is-section-flat-counit-flat + + is-equiv-flat-counit-flat : is-equiv map-flat-counit-flat + pr1 is-equiv-flat-counit-flat = section-flat-counit-flat + pr2 is-equiv-flat-counit-flat = retraction-flat-counit-flat + + equiv-flat-counit-flat : ♭ (♭ A) ≃ ♭ A + pr1 equiv-flat-counit-flat = map-flat-counit-flat + pr2 equiv-flat-counit-flat = is-equiv-flat-counit-flat + + inv-equiv-flat-counit-flat : ♭ A ≃ ♭ (♭ A) + inv-equiv-flat-counit-flat = inv-equiv equiv-flat-counit-flat +``` + +## See also + +- In [the flat-sharp adjunction](modal-type-theory.flat-sharp-adjunction.md) we + postulate that the flat modality is left adjoint to the + [sharp modality](modal-type-theory.sharp-modality.md). +- [Flat discrete types](modal-type-theory.flat-discrete-types.md) for types that + are flat modal. + +## References + +- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type + theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584)) +- Dan Licata, _cohesion-agda_, GitHub repository + () diff --git a/src/modal-type-theory/flat-sharp-adjunction.lagda.md b/src/modal-type-theory/flat-sharp-adjunction.lagda.md new file mode 100644 index 0000000000..e0a4795a23 --- /dev/null +++ b/src/modal-type-theory/flat-sharp-adjunction.lagda.md @@ -0,0 +1,294 @@ +# The flat-sharp adjunction + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.flat-sharp-adjunction where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.locally-small-types +open import foundation.multivariable-sections +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import modal-type-theory.crisp-identity-types +open import modal-type-theory.flat-modality +open import modal-type-theory.sharp-codiscrete-types +open import modal-type-theory.sharp-modality + +open import orthogonal-factorization-systems.locally-small-modal-operators +open import orthogonal-factorization-systems.modal-induction +open import orthogonal-factorization-systems.uniquely-eliminating-modalities +``` + +
+ +## Idea + +We postulate that the [flat modality](modal-type-theory.flat-modality.md) `♭` is +a crisp left adjoint to the +[sharp modality](modal-type-theory.sharp-modality.md) `♯`. + +In [The sharp modality](modal-type-theory.sharp-modality.md) we postulated that +`♯` is a [modal operator](orthogonal-factorization-systems.modal-operators.md) +that has a +[modal induction principle](orthogonal-factorization-systems.modal-induction.md). +In the file +[Sharp-Codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we +postulated that the [subuniverse](foundation.subuniverses.md) of sharp modal +types has appropriate closure properties. Please note that there is some +redundancy between the postulated axioms, and they may be subject to change in +the future. + +## Postulates + +### Crisp induction for `♯` + +Sharp-Codiscrete types are local at the flat counit. + +```agda +postulate + crisp-ind-sharp : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : A → UU l2) → + ((x : A) → is-sharp-codiscrete (C x)) → + ((@♭ x : A) → C x) → (x : A) → C x + + compute-crisp-ind-sharp : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : A → UU l2) + (is-sharp-codiscrete-C : (x : A) → is-sharp-codiscrete (C x)) + (f : (@♭ x : A) → C x) → + (@♭ x : A) → crisp-ind-sharp C is-sharp-codiscrete-C f x ＝ f x +``` + +### Crisp elimination of `♯` + +```agda +postulate + crisp-elim-sharp : + {@♭ l : Level} {@♭ A : UU l} → @♭ ♯ A → A + + compute-crisp-elim-sharp : + {@♭ l : Level} {@♭ A : UU l} (@♭ x : A) → + crisp-elim-sharp (unit-sharp x) ＝ x + + uniqueness-crisp-elim-sharp : + {@♭ l : Level} {@♭ A : UU l} (@♭ x : ♯ A) → + unit-sharp (crisp-elim-sharp x) ＝ x + + coherence-uniqueness-crisp-elim-sharp : + {@♭ l : Level} {@♭ A : UU l} (@♭ x : A) → + ( uniqueness-crisp-elim-sharp (unit-sharp x)) ＝ + ( ap unit-sharp (compute-crisp-elim-sharp x)) +``` + +## Definitions + +### Crisp recursion for `♯` + +```agda +crisp-rec-sharp : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : UU l2) → + (is-sharp-codiscrete C) → + ((@♭ x : A) → C) → A → C +crisp-rec-sharp C is-sharp-codiscrete-C = + crisp-ind-sharp (λ _ → C) (λ _ → is-sharp-codiscrete-C) + +compute-crisp-rec-sharp : + {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : UU l2) + (is-sharp-codiscrete-C : is-sharp-codiscrete C) + (f : (@♭ x : A) → C) → + (@♭ x : A) → crisp-rec-sharp C is-sharp-codiscrete-C f x ＝ f x +compute-crisp-rec-sharp C is-sharp-codiscrete-C = + compute-crisp-ind-sharp (λ _ → C) (λ _ → is-sharp-codiscrete-C) +``` + +## Properties + +```agda +crisp-tr-sharp : + {@♭ l : Level} {@♭ A : UU l} {B : UU l} → (p : A ＝ B) → + {@♭ x : ♯ A} → unit-sharp (tr (λ X → X) p (crisp-elim-sharp x)) ＝ tr ♯ p x +crisp-tr-sharp refl {x} = uniqueness-crisp-elim-sharp x +``` + +### Crisp induction on `♯` implies typal induction + +```agda +ind-crisp-ind-sharp : + {@♭ l1 : Level} {l2 : Level} {A : UU l1} (C : ♯ A → UU l2) → + ((x : ♯ A) → is-sharp-codiscrete (C x)) → + ((x : A) → C (unit-sharp x)) → + (x : ♯ A) → C x +ind-crisp-ind-sharp {A = A} C is-sharp-codiscrete-C f x' = + crisp-ind-sharp + ( λ X → (x : ♯ X) (p : X ＝ A) → C (tr ♯ p x)) + ( λ x → + is-sharp-codiscrete-Π + ( λ y → is-sharp-codiscrete-Π + ( λ p → is-sharp-codiscrete-C (tr ♯ p y)))) + ( λ A' → + crisp-ind-sharp + ( λ y → (p : A' ＝ A) → C (tr ♯ p y)) + ( λ y → is-sharp-codiscrete-Π (λ p → is-sharp-codiscrete-C (tr ♯ p y))) + ( λ x p → tr C (crisp-tr-sharp p) (f (tr id p (crisp-elim-sharp x))))) + ( A) + ( x') + ( refl) +``` + +The accompanying computation principle remains to be fully formalized. + +```text +compute-ind-crisp-ind-sharp : + {@♭ l1 : Level} {l2 : Level} {A : UU l1} (C : ♯ A → UU l2) → + (is-sharp-codiscrete-C : (x : ♯ A) → is-sharp-codiscrete (C x)) → + (f : (x : A) → C (unit-sharp x)) → (x : A) → + ind-crisp-ind-sharp C is-sharp-codiscrete-C f (unit-sharp x) ＝ f x +compute-ind-crisp-ind-sharp {A = A} C is-sharp-codiscrete-C f x = + crisp-ind-sharp + ( λ X → (x : X) (p : X ＝ A) → + ind-crisp-ind-sharp {! !} {! !} {! !} {! !}) + ( {! !}) + {! !} + ( A) + ( x) + ( refl) +``` + +### Flat after sharp + +```agda +module _ + {@♭ l : Level} {@♭ A : UU l} + where + + ap-flat-elim-sharp : ♭ (♯ A) → ♭ A + ap-flat-elim-sharp = ap-crisp-flat crisp-elim-sharp + + ap-flat-unit-sharp : ♭ A → ♭ (♯ A) + ap-flat-unit-sharp = ap-flat unit-sharp + + is-section-ap-flat-unit-sharp : ap-flat-elim-sharp ∘ ap-flat-unit-sharp ~ id + is-section-ap-flat-unit-sharp (cons-flat x) = + ap-crisp cons-flat (compute-crisp-elim-sharp x) + + is-retraction-ap-flat-unit-sharp : + ap-flat-unit-sharp ∘ ap-flat-elim-sharp ~ id + is-retraction-ap-flat-unit-sharp (cons-flat x) = + ap-crisp cons-flat (uniqueness-crisp-elim-sharp x) + + is-equiv-ap-flat-elim-sharp : is-equiv ap-flat-elim-sharp + pr1 (pr1 is-equiv-ap-flat-elim-sharp) = ap-flat-unit-sharp + pr2 (pr1 is-equiv-ap-flat-elim-sharp) = is-section-ap-flat-unit-sharp + pr1 (pr2 is-equiv-ap-flat-elim-sharp) = ap-flat-unit-sharp + pr2 (pr2 is-equiv-ap-flat-elim-sharp) = is-retraction-ap-flat-unit-sharp + + equiv-ap-flat-elim-sharp : ♭ (♯ A) ≃ ♭ A + pr1 equiv-ap-flat-elim-sharp = ap-flat-elim-sharp + pr2 equiv-ap-flat-elim-sharp = is-equiv-ap-flat-elim-sharp + + is-equiv-ap-flat-unit-sharp : is-equiv ap-flat-unit-sharp + pr1 (pr1 is-equiv-ap-flat-unit-sharp) = ap-flat-elim-sharp + pr2 (pr1 is-equiv-ap-flat-unit-sharp) = is-retraction-ap-flat-unit-sharp + pr1 (pr2 is-equiv-ap-flat-unit-sharp) = ap-flat-elim-sharp + pr2 (pr2 is-equiv-ap-flat-unit-sharp) = is-section-ap-flat-unit-sharp + + equiv-ap-flat-unit-sharp : ♭ A ≃ ♭ (♯ A) + pr1 equiv-ap-flat-unit-sharp = ap-flat-unit-sharp + pr2 equiv-ap-flat-unit-sharp = is-equiv-ap-flat-unit-sharp +``` + +### Sharp after flat + +```agda +module _ + {@♭ l : Level} {@♭ A : UU l} + where + + ap-sharp-counit-flat : ♯ (♭ A) → ♯ A + ap-sharp-counit-flat = rec-sharp (unit-sharp ∘ counit-flat) + + ap-sharp-cons-flat : ♯ A → ♯ (♭ A) + ap-sharp-cons-flat = + rec-sharp + ( crisp-rec-sharp + ( ♯ (♭ A)) + ( is-sharp-codiscrete-sharp (♭ A)) + ( λ x → unit-sharp (cons-flat x))) +``` + +It remains to show that these two are inverses to each other. + +```text + is-section-cons-flat : ap-sharp-counit-flat ∘ cons-flat ~ id + is-section-cons-flat = + ind-subuniverse-sharp + ( A) + ( λ x → ap-sharp-counit-flat (cons-flat x) ＝ x) + ( λ x → is-sharp-codiscrete-Id-sharp (ap-sharp-counit-flat (cons-flat x)) x) + ( λ x → + crisp-rec-sharp + ( ap-sharp-counit-flat (cons-flat (unit-sharp x)) ＝ unit-sharp x) + ( is-sharp-codiscrete-Id-sharp (ap-sharp-counit-flat (cons-flat (unit-sharp x))) (unit-sharp x)) + ( λ y → + compute-rec-subuniverse-sharp + {! !} (♯ A) {! is-sharp-codiscrete-sharp ? !} {! !} {! !}) + {! !}) +``` + +### Sharp is uniquely eliminating + +This remains to be formalized. + +```text +map-crisp-retraction-precomp-unit-sharp : + {l1 : Level} {l2 : Level} {X : UU l1} {P : ♯ X → UU l2} → + ((x : ♯ X) → ♯ (P x)) → (x : X) → ♯ (P (unit-sharp x)) +map-crisp-retraction-precomp-unit-sharp {P = P} f = {! !} + +crisp-elim-sharp' : + {@♭ l : Level} {@♭ A : UU l} → @♭ ♯ A → A +crisp-elim-sharp' {A = A} x = crisp-ind-sharp {! !} {! !} {! !} {! !} + +is-retraction-map-crisp-retraction-precomp-unit-sharp : + {@♭ l1 : Level} {l2 : Level} {@♭ X : UU l1} {P : ♯ X → UU l2} → + map-crisp-retraction-precomp-unit-sharp {X = X} {P} ∘ {! precomp-Π (unit-sharp) (♯ ∘ P) !} ~ id +is-retraction-map-crisp-retraction-precomp-unit-sharp = {! !} + +is-uniquely-eliminating-sharp : + {l : Level} → is-uniquely-eliminating-modality (unit-sharp {l}) +is-uniquely-eliminating-sharp X P .pr1 = + section-multivariable-section 2 (precomp-Π unit-sharp (♯ ∘ P)) (induction-principle-sharp X P) +is-uniquely-eliminating-sharp {l} X P .pr2 .pr1 x = +is-uniquely-eliminating-sharp X P .pr2 .pr2 f = + eq-htpy + ( λ x → + equational-reasoning + {! !} + ＝ {! !} by {! !} + ＝ {! !} by compute-crisp-ind-sharp (♯ ∘ P) {! is-sharp-codiscrete-sharp ∘ P !} crisp-elim-sharp {! f !} + ＝ {! !} by {! !}) +``` + +## See also + +- In [codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we + postulate that the sharp modality is a + [higher modality](orthogonal-factorization-systems.higher-modalities.md). + +## References + +- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type + theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584)) +- Dan Licata, _cohesion-agda_, GitHub repository + () diff --git a/src/modal-type-theory/sharp-codiscrete-maps.lagda.md b/src/modal-type-theory/sharp-codiscrete-maps.lagda.md new file mode 100644 index 0000000000..2dab4ff828 --- /dev/null +++ b/src/modal-type-theory/sharp-codiscrete-maps.lagda.md @@ -0,0 +1,50 @@ +# Sharp codiscrete maps + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.sharp-codiscrete-maps where +``` + +
Imports + +```agda +open import foundation.fibers-of-maps +open import foundation.propositions +open import foundation.universe-levels + +open import modal-type-theory.sharp-codiscrete-types +``` + +
+ +## Idea + +A map is said to be **(sharp) codiscrete** if its +[fibers](foundation-core.fibers-of-maps.md) are +[(sharp) codiscrete](modal-type-theory.sharp-codiscrete-types.md). + +## Definition + +```agda +is-sharp-codiscrete-map : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) +is-sharp-codiscrete-map f = is-sharp-codiscrete-family (fiber f) +``` + +## Properties + +### Being codiscrete is a property + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-sharp-codiscrete-map-Prop : Prop (l1 ⊔ l2) + is-sharp-codiscrete-map-Prop = is-sharp-codiscrete-family-Prop (fiber f) + + is-prop-is-sharp-codiscrete-map : is-prop (is-sharp-codiscrete-map f) + is-prop-is-sharp-codiscrete-map = + is-prop-type-Prop is-sharp-codiscrete-map-Prop +``` diff --git a/src/modal-type-theory/sharp-codiscrete-types.lagda.md b/src/modal-type-theory/sharp-codiscrete-types.lagda.md new file mode 100644 index 0000000000..010ddf83e5 --- /dev/null +++ b/src/modal-type-theory/sharp-codiscrete-types.lagda.md @@ -0,0 +1,154 @@ +# Sharp codiscrete types + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.sharp-codiscrete-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.transport-along-equivalences +open import foundation.universe-levels + +open import modal-type-theory.sharp-modality + +open import orthogonal-factorization-systems.higher-modalities +``` + +
+ +## Idea + +A type is said to be **(sharp) codiscrete** if it is +[sharp](modal-type-theory.sharp-modality.md) modal, i.e. if the sharp unit is an +[equivalence](foundation-core.equivalences.md) at that type. + +We postulate that codiscrete types are closed under + +- the formation of identity types +- the formation of dependent function types +- the formation of the subuniverse of codiscrete types. + +Please note that there is some redundancy between the axioms that are assumed +here and in the files on +[the flat-sharp adjunction](modal-type-theory.flat-sharp-adjunction.md), and the +file on the [sharp modality](modal-type-theory.sharp-modality.md), and they may +be subject to change in the future. + +## Definition + +```agda +is-sharp-codiscrete : {l : Level} (A : UU l) → UU l +is-sharp-codiscrete {l} A = is-equiv (unit-sharp {l} {A}) + +is-sharp-codiscrete-family : + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) → UU (l1 ⊔ l2) +is-sharp-codiscrete-family {A = A} B = (x : A) → is-sharp-codiscrete (B x) + +Sharp-Codiscrete : (l : Level) → UU (lsuc l) +Sharp-Codiscrete l = Σ (UU l) (is-sharp-codiscrete) +``` + +## Postulates + +### The identity types of `♯` are codiscrete + +```agda +postulate + is-sharp-codiscrete-Id-sharp : + {l1 : Level} {A : UU l1} (x y : ♯ A) → is-sharp-codiscrete (x ＝ y) + +is-sharp-codiscrete-Id : + {l1 : Level} {A : UU l1} (x y : A) → + is-sharp-codiscrete A → is-sharp-codiscrete (x ＝ y) +is-sharp-codiscrete-Id x y is-sharp-codiscrete-A = + map-tr-equiv + ( is-sharp-codiscrete) + ( inv-equiv-ap-is-emb (is-emb-is-equiv is-sharp-codiscrete-A)) + ( is-sharp-codiscrete-Id-sharp (unit-sharp x) (unit-sharp y)) +``` + +### A `Π`-type is codiscrete if its codomain is + +```agda +postulate + is-sharp-codiscrete-Π : + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → + ((x : A) → is-sharp-codiscrete (B x)) → + is-sharp-codiscrete ((x : A) → B x) +``` + +### The universe of codiscrete types is codiscrete + +```agda +postulate + is-sharp-codiscrete-Sharp-Codiscrete : + (l : Level) → is-sharp-codiscrete (Sharp-Codiscrete l) +``` + +## Properties + +### Being codiscrete is a property + +```agda +module _ + {l : Level} (A : UU l) + where + + is-sharp-codiscrete-Prop : Prop l + is-sharp-codiscrete-Prop = is-equiv-Prop (unit-sharp {l} {A}) + + is-property-is-sharp-codiscrete : is-prop (is-sharp-codiscrete A) + is-property-is-sharp-codiscrete = is-prop-type-Prop is-sharp-codiscrete-Prop + +module _ + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) + where + + is-sharp-codiscrete-family-Prop : Prop (l1 ⊔ l2) + is-sharp-codiscrete-family-Prop = Π-Prop A (is-sharp-codiscrete-Prop ∘ B) + + is-property-is-sharp-codiscrete-family : + is-prop (is-sharp-codiscrete-family B) + is-property-is-sharp-codiscrete-family = + is-prop-type-Prop is-sharp-codiscrete-family-Prop +``` + +### Codiscreteness is a higher modality + +```agda +module _ + (l : Level) + where + + is-higher-modality-sharp : + is-higher-modality (sharp-locally-small-operator-modality l) (unit-sharp) + pr1 is-higher-modality-sharp = induction-principle-sharp + pr2 is-higher-modality-sharp X = is-sharp-codiscrete-Id-sharp + + sharp-higher-modality : higher-modality l l + pr1 sharp-higher-modality = sharp-locally-small-operator-modality l + pr1 (pr2 sharp-higher-modality) = unit-sharp + pr2 (pr2 sharp-higher-modality) = is-higher-modality-sharp +``` + +### Types in the image of `♯` are codiscrete + +```agda +is-sharp-codiscrete-sharp : {l : Level} (X : UU l) → is-sharp-codiscrete (♯ X) +is-sharp-codiscrete-sharp {l} = + is-modal-operator-type-higher-modality (sharp-higher-modality l) +``` + +## See also + +- [Flat discrete types](modal-type-theory.flat-discrete-types.md) for the dual + notion. diff --git a/src/modal-type-theory/sharp-modality.lagda.md b/src/modal-type-theory/sharp-modality.lagda.md new file mode 100644 index 0000000000..52610974df --- /dev/null +++ b/src/modal-type-theory/sharp-modality.lagda.md @@ -0,0 +1,220 @@ +# The sharp modality + +```agda +{-# OPTIONS --cohesion --flat-split #-} + +module modal-type-theory.sharp-modality where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.locally-small-types +open import foundation.universe-levels + +open import orthogonal-factorization-systems.locally-small-modal-operators +open import orthogonal-factorization-systems.modal-induction +open import orthogonal-factorization-systems.modal-subuniverse-induction +``` + +
+ +## Idea + +The **sharp modality `♯`** is an axiomatized +[monadic modality](orthogonal-factorization-systems.higher-modalities.md) we +postulate as a right adjoint to the +[flat modality](modal-type-theory.flat-modality.md). + +In this file, we only postulate that `♯` is a +[modal operator](orthogonal-factorization-systems.modal-operators.md) that has a +[modal induction principle](orthogonal-factorization-systems.modal-induction.md). +In the file about +[codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we postulate +that the [subuniverse](foundation.subuniverses.md) of sharp modal types has +appropriate closure properties. In +[the flat-sharp adjunction](modal-type-theory.flat-sharp-adjunction.md), we +postulate that it has the appropriate relation to the flat modality, making it a +lex modality. Please note that there is some redundancy between the postulated +axioms, and they may be subject to change in the future. + +## Postulates + +```agda +postulate + ♯ : {l : Level} (A : UU l) → UU l + + @♭ unit-sharp : {l : Level} {A : UU l} → A → ♯ A + + ind-sharp : + {l1 l2 : Level} {A : UU l1} (C : ♯ A → UU l2) → + ((x : A) → ♯ (C (unit-sharp x))) → + ((x : ♯ A) → ♯ (C x)) + + compute-ind-sharp : + {l1 l2 : Level} {A : UU l1} (C : ♯ A → UU l2) + (f : (x : A) → ♯ (C (unit-sharp x))) → + (ind-sharp C f ∘ unit-sharp) ~ f +``` + +## Definitions + +### The sharp modal operator + +```agda +sharp-locally-small-operator-modality : + (l : Level) → locally-small-operator-modality l l l +pr1 (sharp-locally-small-operator-modality l) = ♯ {l} +pr2 (sharp-locally-small-operator-modality l) A = is-locally-small' {l} {♯ A} +``` + +### The sharp induction principle + +```agda +induction-principle-sharp : + {l : Level} → induction-principle-modality {l} unit-sharp +pr1 (induction-principle-sharp P) = ind-sharp P +pr2 (induction-principle-sharp P) = compute-ind-sharp P + +strong-induction-principle-subuniverse-sharp : + {l : Level} → strong-induction-principle-subuniverse-modality {l} unit-sharp +strong-induction-principle-subuniverse-sharp = + strong-induction-principle-subuniverse-induction-principle-modality + ( unit-sharp) + ( induction-principle-sharp) + +strong-ind-subuniverse-sharp : + {l : Level} → strong-ind-subuniverse-modality {l} unit-sharp +strong-ind-subuniverse-sharp = + strong-ind-strong-induction-principle-subuniverse-modality + ( unit-sharp) + ( strong-induction-principle-subuniverse-sharp) + +compute-strong-ind-subuniverse-sharp : + {l : Level} → + compute-strong-ind-subuniverse-modality {l} + unit-sharp + strong-ind-subuniverse-sharp +compute-strong-ind-subuniverse-sharp = + compute-strong-ind-strong-induction-principle-subuniverse-modality + ( unit-sharp) + ( strong-induction-principle-subuniverse-sharp) + +induction-principle-subuniverse-sharp : + {l : Level} → induction-principle-subuniverse-modality {l} unit-sharp +induction-principle-subuniverse-sharp = + induction-principle-subuniverse-induction-principle-modality + ( unit-sharp) + ( induction-principle-sharp) + +ind-subuniverse-sharp : + {l : Level} → ind-subuniverse-modality {l} unit-sharp +ind-subuniverse-sharp = + ind-induction-principle-subuniverse-modality + ( unit-sharp) + ( induction-principle-subuniverse-sharp) + +compute-ind-subuniverse-sharp : + {l : Level} → + compute-ind-subuniverse-modality {l} unit-sharp ind-subuniverse-sharp +compute-ind-subuniverse-sharp = + compute-ind-induction-principle-subuniverse-modality + ( unit-sharp) + ( induction-principle-subuniverse-sharp) +``` + +### Sharp recursion + +```agda +rec-sharp : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + (A → ♯ B) → (♯ A → ♯ B) +rec-sharp {B = B} = ind-sharp (λ _ → B) + +compute-rec-sharp : + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (f : A → ♯ B) → + (rec-sharp f ∘ unit-sharp) ~ f +compute-rec-sharp {B = B} = compute-ind-sharp (λ _ → B) + +recursion-principle-sharp : + {l : Level} → recursion-principle-modality {l} unit-sharp +pr1 (recursion-principle-sharp) = rec-sharp +pr2 (recursion-principle-sharp) = compute-rec-sharp + +strong-recursion-principle-subuniverse-sharp : + {l : Level} → strong-recursion-principle-subuniverse-modality {l} unit-sharp +strong-recursion-principle-subuniverse-sharp = + strong-recursion-principle-subuniverse-recursion-principle-modality + ( unit-sharp) + ( recursion-principle-sharp) + +strong-rec-subuniverse-sharp : + {l : Level} → strong-rec-subuniverse-modality {l} unit-sharp +strong-rec-subuniverse-sharp = + strong-rec-strong-recursion-principle-subuniverse-modality + ( unit-sharp) + ( strong-recursion-principle-subuniverse-sharp) + +compute-strong-rec-subuniverse-sharp : + {l : Level} → + compute-strong-rec-subuniverse-modality {l} + unit-sharp + strong-rec-subuniverse-sharp +compute-strong-rec-subuniverse-sharp = + compute-strong-rec-strong-recursion-principle-subuniverse-modality + ( unit-sharp) + ( strong-recursion-principle-subuniverse-sharp) + +recursion-principle-subuniverse-sharp : + {l : Level} → recursion-principle-subuniverse-modality {l} unit-sharp +recursion-principle-subuniverse-sharp = + recursion-principle-subuniverse-recursion-principle-modality + ( unit-sharp) + ( recursion-principle-sharp) + +rec-subuniverse-sharp : + {l : Level} → rec-subuniverse-modality {l} unit-sharp +rec-subuniverse-sharp = + rec-recursion-principle-subuniverse-modality + ( unit-sharp) + ( recursion-principle-subuniverse-sharp) + +compute-rec-subuniverse-sharp : + {l : Level} → + compute-rec-subuniverse-modality {l} unit-sharp rec-subuniverse-sharp +compute-rec-subuniverse-sharp = + compute-rec-recursion-principle-subuniverse-modality + ( unit-sharp) + ( recursion-principle-subuniverse-sharp) +``` + +### Action on maps + +```agda +ap-sharp : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → (♯ A → ♯ B) +ap-sharp f = rec-sharp (unit-sharp ∘ f) +``` + +## See also + +- In [codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we + postulate that the sharp modality is a + [higher modality](orthogonal-factorization-systems.higher-modalities.md). +- and in [the flat-sharp adjunction](modal-type-theory.flat-sharp-adjunction.md) + we moreover postulate that the sharp modality is right adjoint to the + [flat modality](modal-type-theory.flat-modality.md). + +## References + +- Michael Shulman, _Brouwer's fixed-point theorem in real-cohesive homotopy type + theory_, 2015 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584)) +- Dan Licata, _cohesion-agda_, GitHub repository + () +- Felix Cherubini, _DCHoTT-Agda_/Im.agda, file in GitHub repository + () diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 84faaac91a..18369743fd 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -19,6 +19,7 @@ open import orthogonal-factorization-systems.factorizations-of-maps public open import orthogonal-factorization-systems.factorizations-of-maps-function-classes public open import orthogonal-factorization-systems.factorizations-of-maps-global-function-classes public open import orthogonal-factorization-systems.function-classes public +open import orthogonal-factorization-systems.functoriality-higher-modalities public open import orthogonal-factorization-systems.functoriality-pullback-hom public open import orthogonal-factorization-systems.global-function-classes public open import orthogonal-factorization-systems.higher-modalities public @@ -33,7 +34,9 @@ open import orthogonal-factorization-systems.localizations-maps public open import orthogonal-factorization-systems.localizations-subuniverses public open import orthogonal-factorization-systems.locally-small-modal-operators public open import orthogonal-factorization-systems.mere-lifting-properties public +open import orthogonal-factorization-systems.modal-induction public open import orthogonal-factorization-systems.modal-operators public +open import orthogonal-factorization-systems.modal-subuniverse-induction public open import orthogonal-factorization-systems.null-types public open import orthogonal-factorization-systems.open-modalities public open import orthogonal-factorization-systems.orthogonal-factorization-systems public diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md index d39203d1c0..0b18cf063c 100644 --- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md @@ -43,7 +43,7 @@ operator-closed-modality l Q A = A * type-Prop Q unit-closed-modality : {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality l Q) -unit-closed-modality Q {A} = inl-join A (type-Prop Q) +unit-closed-modality Q = inl-join is-closed-modal : {l lQ : Level} (Q : Prop lQ) → UU l → Prop (l ⊔ lQ) @@ -76,7 +76,7 @@ module _ ( λ f → is-contr-equiv ( Σ (A → B) (_＝ f)) - ( equiv-Σ + ( equiv-Σ-equiv-base ( _＝ f) ( right-unit-law-Σ-is-contr ( λ f' → @@ -89,8 +89,7 @@ module _ ( is-modal-B q) ( f' a) ( center (is-modal-B q))))) ∘e - ( equiv-up-join A (type-Prop Q) B)) - ( λ _ → id-equiv)) + ( equiv-up-join B))) ( is-torsorial-path' f)) reflective-subuniverse-closed-modality : diff --git a/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md b/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md new file mode 100644 index 0000000000..a2e7148542 --- /dev/null +++ b/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md @@ -0,0 +1,195 @@ +# Functoriality of higher modalities + +```agda +module orthogonal-factorization-systems.functoriality-higher-modalities where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.path-algebra +open import foundation.small-types +open import foundation.transport-along-identifications +open import foundation.univalence +open import foundation.universe-levels + +open import orthogonal-factorization-systems.higher-modalities +open import orthogonal-factorization-systems.modal-induction +open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.modal-subuniverse-induction +``` + +
+ +## Idea + +Every [higher modality](orthogonal-factorization-systems.higher-modalities.md) +`○` is functorial. Given a map `f : A → B`, there is a +[unique](foundation-core.contractible-types.md) map `○f : ○A → ○B` that fits +into a [natural square](foundation-core.commuting-squares-of-maps.md) + +```text + f + X ------> Y + | | + | | + v v + ○ X ----> ○ Y. + ○ f +``` + +This construction preserves [composition](foundation-core.function-types.md), +[identifications](foundation-core.identity-types.md), +[homotopies](foundation-core.homotopies.md), and +[equivalences](foundation-core.equivalences.md). + +## Properties + +### Action on maps + +```agda +module _ + {l1 l2 : Level} (m : higher-modality l1 l2) + where + + ap-map-higher-modality : + {X Y : UU l1} → + (X → Y) → operator-higher-modality m X → operator-higher-modality m Y + ap-map-higher-modality = + ap-map-ind-modality (unit-higher-modality m) (ind-higher-modality m) +``` + +### Functoriality + +```agda +module _ + {l : Level} (m : higher-modality l l) + where + + functoriality-higher-modality : + {X Y Z : UU l} (g : Y → Z) (f : X → Y) → + ( ap-map-higher-modality m g ∘ ap-map-higher-modality m f) ~ + ( ap-map-higher-modality m (g ∘ f)) + functoriality-higher-modality {X} {Y} {Z} g f = + ind-subuniverse-Id-higher-modality m + ( ap-map-higher-modality m g ∘ ap-map-higher-modality m f) + ( ap-map-higher-modality m (g ∘ f)) + ( λ x → + ( ap + ( ap-map-higher-modality m g) + ( compute-rec-higher-modality m (unit-higher-modality m ∘ f) x)) ∙ + ( ( compute-rec-higher-modality m (unit-higher-modality m ∘ g) (f x)) ∙ + ( inv + ( compute-rec-higher-modality m + ( unit-higher-modality m ∘ (g ∘ f)) + ( x))))) +``` + +### Naturality of the unit of a higher modality + +For every map `f : X → Y` there is a naturality square + +```text + f + X ------> Y + | | + | | + v v + ○ X ----> ○ Y. + ○ f +``` + +```agda +module _ + {l1 l2 : Level} (m : higher-modality l1 l2) + where + + naturality-unit-higher-modality : + {X Y : UU l1} (f : X → Y) → + ( ap-map-higher-modality m f ∘ unit-higher-modality m) ~ + ( unit-higher-modality m ∘ f) + naturality-unit-higher-modality = + naturality-unit-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + ( compute-ind-higher-modality m) +``` + +```agda + naturality-unit-higher-modality' : + {X Y : UU l1} (f : X → Y) {x x' : X} → + unit-higher-modality m x ＝ unit-higher-modality m x' → + unit-higher-modality m (f x) ＝ unit-higher-modality m (f x') + naturality-unit-higher-modality' = + naturality-unit-ind-modality' + ( unit-higher-modality m) + ( ind-higher-modality m) + ( compute-ind-higher-modality m) + +module _ + {l : Level} (m : higher-modality l l) + where + + compute-naturality-unit-ind-modality : + {X Y Z : UU l} (g : Y → Z) (f : X → Y) (x : X) → + ( ( functoriality-higher-modality m g f (unit-higher-modality m x)) ∙ + ( naturality-unit-higher-modality m (g ∘ f) x)) ＝ + ( ( ap + ( ap-map-higher-modality m g) + ( naturality-unit-higher-modality m f x)) ∙ + ( naturality-unit-higher-modality m g (f x))) + compute-naturality-unit-ind-modality g f x = + ( ap + ( _∙ + compute-rec-higher-modality m (unit-higher-modality m ∘ (g ∘ f)) x) + ( compute-ind-subuniverse-Id-higher-modality m + ( ap-map-higher-modality m g ∘ ap-map-higher-modality m f) + ( ap-map-higher-modality m (g ∘ f)) + ( _) + ( x))) ∙ + ( assoc + ( ap + ( ap-map-higher-modality m g) + ( compute-rec-higher-modality m (unit-higher-modality m ∘ f) x)) + ( ( compute-rec-higher-modality m (unit-higher-modality m ∘ g) (f x)) ∙ + ( inv + ( compute-rec-higher-modality m (unit-higher-modality m ∘ g ∘ f) x))) + ( compute-rec-higher-modality m (unit-higher-modality m ∘ g ∘ f) x)) ∙ + ( ap + ( ap + ( ap-map-higher-modality m g) + ( compute-rec-higher-modality m (unit-higher-modality m ∘ f) x) ∙_) + ( is-section-right-concat-inv + ( compute-rec-higher-modality m (unit-higher-modality m ∘ g) (f x)) + ( compute-rec-higher-modality m (unit-higher-modality m ∘ g ∘ f) x))) +``` + +### Action on homotopies + +This definition of action on [homotopies](foundation-core.homotopies.md) is +meant to avoid using +[function extensionality](foundation.function-extensionality.md). This is left +for future work. + +```agda +module _ + {l : Level} (m : higher-modality l l) + where + + htpy-ap-higher-modality : + {X Y : UU l} {f g : X → Y} → + f ~ g → ap-map-higher-modality m f ~ ap-map-higher-modality m g + htpy-ap-higher-modality H x' = + ap (λ f → ap-map-higher-modality m f x') (eq-htpy H) +``` + +## References + +- Felix Cherubini, _DCHoTT-Agda_/Im.agda, file in GitHub repository + () diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index 26554e0958..727700fdb1 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -15,11 +15,16 @@ open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies open import foundation.identity-types +open import foundation.retractions open import foundation.small-types +open import foundation.transport-along-identifications +open import foundation.univalence open import foundation.universe-levels open import orthogonal-factorization-systems.locally-small-modal-operators +open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.modal-subuniverse-induction open import orthogonal-factorization-systems.uniquely-eliminating-modalities ``` @@ -47,38 +52,6 @@ this, higher modalities in their most general form only make sense for ## Definition -### The universal property of higher modalities - -```agda -module _ - {l1 l2 : Level} - {○ : operator-modality l1 l2} - (unit-○ : unit-modality ○) - where - - ind-modality : UU (lsuc l1 ⊔ l2) - ind-modality = - (X : UU l1) (P : ○ X → UU l1) → - ((x : X) → ○ (P (unit-○ x))) → - (x' : ○ X) → ○ (P x') - - rec-modality : UU (lsuc l1 ⊔ l2) - rec-modality = (X Y : UU l1) → (X → ○ Y) → ○ X → ○ Y - - compute-ind-modality : ind-modality → UU (lsuc l1 ⊔ l2) - compute-ind-modality ind-○ = - (X : UU l1) (P : ○ X → UU l1) → - (f : (x : X) → ○ (P (unit-○ x))) → - (x : X) → ind-○ X P f (unit-○ x) ＝ f x - - dependent-universal-property-modality : UU (lsuc l1 ⊔ l2) - dependent-universal-property-modality = - Σ ind-modality compute-ind-modality - - rec-modality-ind-modality : ind-modality → rec-modality - rec-modality-ind-modality ind X Y = ind X (λ _ → Y) -``` - ### Closure under identity type formers We say that the [locally small type](foundation-core.identity-types.md) of a @@ -94,8 +67,8 @@ module _ (unit-○ : unit-modality ○) where - is-modal-identity-types : UU (lsuc l1 ⊔ l2) - is-modal-identity-types = + is-modal-small-identity-types : UU (lsuc l1 ⊔ l2) + is-modal-small-identity-types = (X : UU l1) (x y : ○ X) → is-modal-type-is-small (unit-○) (x ＝ y) (is-locally-small-○ X x y) ``` @@ -105,27 +78,57 @@ module _ ```agda is-higher-modality : UU (lsuc l1 ⊔ l2) is-higher-modality = - dependent-universal-property-modality (unit-○) × is-modal-identity-types + induction-principle-modality (unit-○) × is-modal-small-identity-types ``` ### Components of a higher modality proof ```agda - ind-modality-is-higher-modality : is-higher-modality → ind-modality unit-○ - ind-modality-is-higher-modality = pr1 ∘ pr1 - - rec-modality-is-higher-modality : is-higher-modality → rec-modality unit-○ - rec-modality-is-higher-modality = - rec-modality-ind-modality unit-○ ∘ ind-modality-is-higher-modality - - compute-ind-modality-is-higher-modality : - (h : is-higher-modality) → - compute-ind-modality unit-○ (ind-modality-is-higher-modality h) - compute-ind-modality-is-higher-modality = pr2 ∘ pr1 +module _ + {l1 l2 : Level} + (locally-small-○ : locally-small-operator-modality l1 l2 l1) + (unit-○ : unit-modality (pr1 locally-small-○)) + (h : is-higher-modality locally-small-○ unit-○) + where - is-modal-identity-types-is-higher-modality : - is-higher-modality → is-modal-identity-types - is-modal-identity-types-is-higher-modality = pr2 + induction-principle-is-higher-modality : induction-principle-modality unit-○ + induction-principle-is-higher-modality = pr1 h + + ind-is-higher-modality : ind-modality unit-○ + ind-is-higher-modality = + ind-induction-principle-modality + ( unit-○) + ( induction-principle-is-higher-modality) + + compute-ind-is-higher-modality : + compute-ind-modality unit-○ ind-is-higher-modality + compute-ind-is-higher-modality = + compute-ind-induction-principle-modality + ( unit-○) + ( induction-principle-is-higher-modality) + + recursion-principle-is-higher-modality : recursion-principle-modality unit-○ + recursion-principle-is-higher-modality = + recursion-principle-induction-principle-modality + ( unit-○) + ( induction-principle-is-higher-modality) + + rec-is-higher-modality : rec-modality unit-○ + rec-is-higher-modality = + rec-recursion-principle-modality + ( unit-○) + ( recursion-principle-is-higher-modality) + + compute-rec-is-higher-modality : + compute-rec-modality unit-○ rec-is-higher-modality + compute-rec-is-higher-modality = + compute-rec-recursion-principle-modality + ( unit-○) + ( recursion-principle-is-higher-modality) + + is-modal-small-identity-types-is-higher-modality : + is-modal-small-identity-types locally-small-○ unit-○ + is-modal-small-identity-types-is-higher-modality = pr2 h ``` ### The structure of a higher modality @@ -139,7 +142,7 @@ higher-modality l1 l2 = ( is-higher-modality ○)) ``` -### Compoents of a higher modality +### Components of a higher modality ```agda module _ @@ -171,37 +174,58 @@ module _ ( unit-higher-modality) is-higher-modality-higher-modality = pr2 (pr2 h) - ind-modality-higher-modality : - ind-modality (unit-higher-modality) - ind-modality-higher-modality = - ind-modality-is-higher-modality + induction-principle-higher-modality : + induction-principle-modality (unit-higher-modality) + induction-principle-higher-modality = + induction-principle-is-higher-modality ( locally-small-operator-higher-modality) ( unit-higher-modality) ( is-higher-modality-higher-modality) - rec-modality-higher-modality : - rec-modality (unit-higher-modality) - rec-modality-higher-modality = - rec-modality-ind-modality + ind-higher-modality : + ind-modality (unit-higher-modality) + ind-higher-modality = + ind-induction-principle-modality ( unit-higher-modality) - ( ind-modality-higher-modality) + ( induction-principle-higher-modality) - compute-ind-modality-higher-modality : + compute-ind-higher-modality : compute-ind-modality ( unit-higher-modality) - ( ind-modality-higher-modality) - compute-ind-modality-higher-modality = - compute-ind-modality-is-higher-modality + ( ind-higher-modality) + compute-ind-higher-modality = + compute-ind-induction-principle-modality + ( unit-higher-modality) + ( induction-principle-higher-modality) + + recursion-principle-higher-modality : + recursion-principle-modality (unit-higher-modality) + recursion-principle-higher-modality = + recursion-principle-is-higher-modality ( locally-small-operator-higher-modality) ( unit-higher-modality) ( is-higher-modality-higher-modality) - is-modal-identity-types-higher-modality : - is-modal-identity-types + rec-higher-modality : + rec-modality (unit-higher-modality) + rec-higher-modality = + rec-recursion-principle-modality + ( unit-higher-modality) + ( recursion-principle-higher-modality) + + compute-rec-higher-modality : + compute-rec-modality (unit-higher-modality) (rec-higher-modality) + compute-rec-higher-modality = + compute-rec-recursion-principle-modality + ( unit-higher-modality) + ( recursion-principle-higher-modality) + + is-modal-small-identity-type-higher-modality : + is-modal-small-identity-types ( locally-small-operator-higher-modality) ( unit-higher-modality) - is-modal-identity-types-higher-modality = - ( is-modal-identity-types-is-higher-modality) + is-modal-small-identity-type-higher-modality = + ( is-modal-small-identity-types-is-higher-modality) ( locally-small-operator-higher-modality) ( unit-higher-modality) ( is-higher-modality-higher-modality) @@ -209,135 +233,292 @@ module _ ## Properties -### The modal operator's action on maps +### Subuniverse induction for higher modalities ```agda module _ - {l : Level} - {○ : operator-modality l l} (unit-○ : unit-modality ○) + {l1 l2 : Level} (m : higher-modality l1 l2) where - map-rec-modality : - (rec-○ : rec-modality unit-○) {X Y : UU l} → (X → Y) → ○ X → ○ Y - map-rec-modality rec-○ {X} {Y} f = rec-○ X Y (unit-○ ∘ f) + strong-ind-subuniverse-higher-modality : + strong-ind-subuniverse-modality (unit-higher-modality m) + strong-ind-subuniverse-higher-modality = + strong-ind-subuniverse-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + + compute-strong-ind-subuniverse-higher-modality : + compute-strong-ind-subuniverse-modality + ( unit-higher-modality m) + ( strong-ind-subuniverse-higher-modality) + compute-strong-ind-subuniverse-higher-modality = + compute-strong-ind-subuniverse-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + ( compute-ind-higher-modality m) + + ind-subuniverse-higher-modality : + ind-subuniverse-modality (unit-higher-modality m) + ind-subuniverse-higher-modality = + ind-subuniverse-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + + compute-ind-subuniverse-higher-modality : + compute-ind-subuniverse-modality + ( unit-higher-modality m) + ( ind-subuniverse-higher-modality) + compute-ind-subuniverse-higher-modality = + compute-ind-subuniverse-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + ( compute-ind-higher-modality m) + + strong-rec-subuniverse-higher-modality : + strong-rec-subuniverse-modality (unit-higher-modality m) + strong-rec-subuniverse-higher-modality = + strong-rec-subuniverse-rec-modality + ( unit-higher-modality m) + ( rec-higher-modality m) + + compute-strong-rec-subuniverse-higher-modality : + compute-strong-rec-subuniverse-modality + ( unit-higher-modality m) + ( strong-rec-subuniverse-higher-modality) + compute-strong-rec-subuniverse-higher-modality = + compute-strong-rec-subuniverse-rec-modality + ( unit-higher-modality m) + ( rec-higher-modality m) + ( compute-rec-higher-modality m) + + rec-subuniverse-higher-modality : + rec-subuniverse-modality (unit-higher-modality m) + rec-subuniverse-higher-modality = + rec-subuniverse-rec-modality + ( unit-higher-modality m) + ( rec-higher-modality m) + + compute-rec-subuniverse-higher-modality : + compute-rec-subuniverse-modality + ( unit-higher-modality m) + ( rec-subuniverse-higher-modality) + compute-rec-subuniverse-higher-modality = + compute-rec-subuniverse-rec-modality + ( unit-higher-modality m) + ( rec-higher-modality m) + ( compute-rec-higher-modality m) ``` -### Modal identity elimination +### When `l1 = l2`, the identity types are modal in the usual sense ```agda -module _ +map-inv-unit-small-Id-higher-modality : {l1 l2 : Level} - ((○ , is-locally-small-○) : locally-small-operator-modality l1 l2 l1) - (unit-○ : unit-modality ○) - (Id-○ : is-modal-identity-types (○ , is-locally-small-○) unit-○) + (m : higher-modality l1 l2) + {X : UU l1} {x' y' : operator-higher-modality m X} → + ( operator-higher-modality m + ( type-is-small (is-locally-small-operator-higher-modality m X x' y'))) → + x' ＝ y' +map-inv-unit-small-Id-higher-modality m {X} {x'} {y'} = + map-inv-unit-is-modal-type-is-small + ( unit-higher-modality m) + ( x' ＝ y') + ( is-locally-small-operator-higher-modality m X x' y') + ( is-modal-small-identity-type-higher-modality m X x' y') + +module _ + {l : Level} (m : higher-modality l l) where - elim-Id-higher-modality : - {X : UU l1} {x' y' : ○ X} → - ○ (type-is-small (is-locally-small-○ X x' y')) → x' ＝ y' - elim-Id-higher-modality {X} {x'} {y'} = - map-inv-unit-is-modal-type-is-small unit-○ - ( x' ＝ y') - ( is-locally-small-○ X x' y') - ( Id-○ X x' y') + map-inv-unit-Id-higher-modality : + {X : UU l} {x' y' : operator-higher-modality m X} → + operator-higher-modality m (x' ＝ y') → x' ＝ y' + map-inv-unit-Id-higher-modality {X} {x'} {y'} = + map-inv-unit-small-Id-higher-modality m ∘ + ( ap-map-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + ( map-equiv-is-small + ( is-locally-small-operator-higher-modality m X x' y'))) + + is-section-unit-Id-higher-modality : + {X : UU l} {x' y' : operator-higher-modality m X} → + (map-inv-unit-Id-higher-modality ∘ unit-higher-modality m {x' ＝ y'}) ~ id + is-section-unit-Id-higher-modality {X} {x'} {y'} p = + ( ap + ( map-inv-equiv + ( equiv-unit-is-modal-type-is-small + ( unit-higher-modality m) + ( x' ＝ y') + ( is-small-x'=y') + ( is-modal-small-x'=y'))) + ( compute-rec-higher-modality m + ( unit-higher-modality m ∘ map-equiv-is-small is-small-x'=y') + ( p))) ∙ + ( htpy-eq + ( distributive-map-inv-comp-equiv + ( equiv-is-small is-small-x'=y') + ( unit-higher-modality m , is-modal-small-x'=y')) + ( unit-higher-modality m (map-equiv-is-small is-small-x'=y' p))) ∙ + ( ap + ( map-inv-equiv-is-small is-small-x'=y') + ( is-retraction-map-inv-is-equiv is-modal-small-x'=y' + ( map-equiv-is-small is-small-x'=y' p))) ∙ + ( is-retraction-map-inv-equiv (equiv-is-small is-small-x'=y') p) + where + is-small-x'=y' = is-locally-small-operator-higher-modality m X x' y' + is-modal-small-x'=y' = + is-modal-small-identity-type-higher-modality m X x' y' + + retraction-unit-Id-higher-modality : + {X : UU l} {x' y' : operator-higher-modality m X} → + retraction (unit-higher-modality m {x' ＝ y'}) + pr1 retraction-unit-Id-higher-modality = map-inv-unit-Id-higher-modality + pr2 retraction-unit-Id-higher-modality = is-section-unit-Id-higher-modality ``` -### For homogenous higher modalities, The identity types of modal types are modal in the usual sense +We get this retraction without applying univalence, so, using strong subuniverse +induction we can generally avoid it. However, we appeal to univalence to get the +full equivalence. + +```agda + is-modal-Id-higher-modality : + {X : UU l} {x' y' : operator-higher-modality m X} → + is-modal (unit-higher-modality m) (x' ＝ y') + is-modal-Id-higher-modality {X} {x'} {y'} = + tr + ( is-modal (unit-higher-modality m)) + ( eq-equiv + ( type-is-small (is-locally-small-operator-higher-modality m X x' y')) + ( x' ＝ y') + ( inv-equiv-is-small + ( is-locally-small-operator-higher-modality m X x' y'))) + ( is-modal-small-identity-type-higher-modality m X x' y') +``` + +### Subuniverse induction on identity types ```agda module _ - {l : Level} - ( ((○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) : - higher-modality l l) + {l : Level} (m : higher-modality l l) where - map-inv-unit-id-higher-modality : - {X : UU l} {x' y' : ○ X} → ○ (x' ＝ y') → x' ＝ y' - map-inv-unit-id-higher-modality {X} {x'} {y'} = - map-inv-unit-is-modal-type-is-small unit-○ - ( x' ＝ y') - ( is-locally-small-○ X x' y') - ( Id-○ X x' y') ∘ - ( map-rec-modality unit-○ - ( rec-modality-ind-modality unit-○ ind-○) - ( map-equiv-is-small ( is-locally-small-○ X x' y'))) + ind-subuniverse-Id-higher-modality : + {X : UU l} {Y : operator-higher-modality m X → UU l} + (f g : + (x' : operator-higher-modality m X) → operator-higher-modality m (Y x')) → + (f ∘ unit-higher-modality m) ~ (g ∘ unit-higher-modality m) → + f ~ g + ind-subuniverse-Id-higher-modality {X} f g = + strong-ind-subuniverse-higher-modality m + ( λ x' → f x' ＝ g x') + ( λ _ → retraction-unit-Id-higher-modality m) + + compute-ind-subuniverse-Id-higher-modality : + {X : UU l} {Y : operator-higher-modality m X → UU l} + (f g : + (x' : operator-higher-modality m X) → operator-higher-modality m (Y x')) → + (H : (f ∘ unit-higher-modality m) ~ (g ∘ unit-higher-modality m)) → + (x : X) → + ( strong-ind-subuniverse-higher-modality m + ( λ x' → f x' ＝ g x') + ( λ _ → retraction-unit-Id-higher-modality m) + ( H) + ( unit-higher-modality m x)) ＝ + ( H x) + compute-ind-subuniverse-Id-higher-modality f g = + compute-strong-ind-subuniverse-higher-modality m + ( λ x → f x ＝ g x) + ( λ _ → retraction-unit-Id-higher-modality m) ``` -### `○ X` is modal +### Types in the image of the modal operator are modal ```agda module _ - {l : Level} - ( ((○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) : - higher-modality l l) - (X : UU l) + {l : Level} (m : higher-modality l l) (X : UU l) where - map-inv-unit-higher-modality : ○ (○ X) → ○ X - map-inv-unit-higher-modality = ind-○ (○ X) (λ _ → X) id + map-inv-unit-higher-modality : + operator-higher-modality m (operator-higher-modality m X) → + operator-higher-modality m X + map-inv-unit-higher-modality = rec-higher-modality m id is-retraction-map-inv-unit-higher-modality : - (map-inv-unit-higher-modality ∘ unit-○) ~ id - is-retraction-map-inv-unit-higher-modality = compute-ind-○ (○ X) (λ _ → X) id + map-inv-unit-higher-modality ∘ unit-higher-modality m ~ id + is-retraction-map-inv-unit-higher-modality = compute-rec-higher-modality m id is-section-map-inv-unit-higher-modality : - (unit-○ ∘ map-inv-unit-higher-modality) ~ id - is-section-map-inv-unit-higher-modality x'' = - map-inv-unit-id-higher-modality - ( (○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) - ( ind-○ (○ X) - ( λ x'' → unit-○ (map-inv-unit-higher-modality x'') ＝ x'') - ( unit-○ ∘ (ap unit-○ ∘ is-retraction-map-inv-unit-higher-modality)) - ( x'')) - - is-modal-operator-modality-type : is-modal unit-○ (○ X) - pr1 (pr1 is-modal-operator-modality-type) = map-inv-unit-higher-modality - pr2 (pr1 is-modal-operator-modality-type) = + unit-higher-modality m ∘ map-inv-unit-higher-modality ~ id + is-section-map-inv-unit-higher-modality = + ind-subuniverse-Id-higher-modality m _ _ + ( ap (unit-higher-modality m) ∘ + is-retraction-map-inv-unit-higher-modality) + + is-modal-operator-type-higher-modality : + is-modal (unit-higher-modality m) (operator-higher-modality m X) + pr1 (pr1 is-modal-operator-type-higher-modality) = + map-inv-unit-higher-modality + pr2 (pr1 is-modal-operator-type-higher-modality) = is-section-map-inv-unit-higher-modality - pr1 (pr2 is-modal-operator-modality-type) = map-inv-unit-higher-modality - pr2 (pr2 is-modal-operator-modality-type) = + pr1 (pr2 is-modal-operator-type-higher-modality) = + map-inv-unit-higher-modality + pr2 (pr2 is-modal-operator-type-higher-modality) = is-retraction-map-inv-unit-higher-modality ``` ### Higher modalities are uniquely eliminating modalities ```agda +is-section-ind-higher-modality : + {l1 l2 : Level} (m : higher-modality l1 l2) + {X : UU l1} {P : operator-higher-modality m X → UU l1} → + ( ( precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P)) ∘ + ( ind-higher-modality m P)) ~ + ( id) +is-section-ind-higher-modality m = + is-section-ind-modality + ( unit-higher-modality m) + ( ind-higher-modality m) + ( compute-ind-higher-modality m) + module _ - {l : Level} - ( ((○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) : - higher-modality l l) + {l : Level} (m : higher-modality l l) where - is-retraction-ind-modality : - {X : UU l} {P : ○ X → UU l} → (precomp-Π unit-○ (○ ∘ P) ∘ ind-○ X P) ~ id - is-retraction-ind-modality {X} {P} = eq-htpy ∘ compute-ind-○ X P - - is-section-ind-modality : - {X : UU l} {P : ○ X → UU l} → (ind-○ X P ∘ precomp-Π unit-○ (○ ∘ P)) ~ id - is-section-ind-modality {X} {P} s = + is-retraction-ind-higher-modality : + {X : UU l} (P : operator-higher-modality m X → UU l) → + ( ind-higher-modality m P ∘ + precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P)) ~ + ( id) + is-retraction-ind-higher-modality P s = eq-htpy - ( map-inv-unit-id-higher-modality - ( (○ , is-locally-small-○) , unit-○ , (ind-○ , compute-ind-○) , Id-○) ∘ - ( ind-○ X - ( λ x' → (ind-○ X P ∘ precomp-Π (unit-○) (○ ∘ P)) s x' ＝ s x') - ( unit-○ ∘ compute-ind-○ X P (s ∘ unit-○)))) - - is-equiv-ind-modality : (X : UU l) (P : ○ X → UU l) → is-equiv (ind-○ X P) - pr1 (pr1 (is-equiv-ind-modality X P)) = precomp-Π unit-○ (○ ∘ P) - pr2 (pr1 (is-equiv-ind-modality X P)) = is-section-ind-modality - pr1 (pr2 (is-equiv-ind-modality X P)) = precomp-Π unit-○ (○ ∘ P) - pr2 (pr2 (is-equiv-ind-modality X P)) = is-retraction-ind-modality - - equiv-ind-modality : - (X : UU l) (P : ○ X → UU l) → - ((x : X) → ○ (P (unit-○ x))) ≃ ((x' : ○ X) → ○ (P x')) - pr1 (equiv-ind-modality X P) = ind-○ X P - pr2 (equiv-ind-modality X P) = is-equiv-ind-modality X P - - is-uniquely-eliminating-modality-higher-modality : - is-uniquely-eliminating-modality unit-○ - is-uniquely-eliminating-modality-higher-modality X P = - is-equiv-map-inv-is-equiv (is-equiv-ind-modality X P) + ( ind-subuniverse-Id-higher-modality m _ _ + ( compute-ind-higher-modality m P (s ∘ unit-higher-modality m))) + + is-equiv-ind-higher-modality : + {X : UU l} (P : operator-higher-modality m X → UU l) → + is-equiv (ind-higher-modality m P) + pr1 (pr1 (is-equiv-ind-higher-modality P)) = + precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P) + pr2 (pr1 (is-equiv-ind-higher-modality P)) = + is-retraction-ind-higher-modality P + pr1 (pr2 (is-equiv-ind-higher-modality P)) = + precomp-Π (unit-higher-modality m) (operator-higher-modality m ∘ P) + pr2 (pr2 (is-equiv-ind-higher-modality P)) = + is-section-ind-higher-modality m + + equiv-ind-higher-modality : + {X : UU l} (P : operator-higher-modality m X → UU l) → + ((x : X) → operator-higher-modality m (P (unit-higher-modality m x))) ≃ + ((x' : operator-higher-modality m X) → operator-higher-modality m (P x')) + pr1 (equiv-ind-higher-modality P) = ind-higher-modality m P + pr2 (equiv-ind-higher-modality P) = is-equiv-ind-higher-modality P + + is-uniquely-eliminating-higher-modality : + is-uniquely-eliminating-modality (unit-higher-modality m) + is-uniquely-eliminating-higher-modality P = + is-equiv-map-inv-is-equiv (is-equiv-ind-higher-modality P) ``` ## See also diff --git a/src/orthogonal-factorization-systems/identity-modality.lagda.md b/src/orthogonal-factorization-systems/identity-modality.lagda.md index 0798532317..ddd8624de0 100644 --- a/src/orthogonal-factorization-systems/identity-modality.lagda.md +++ b/src/orthogonal-factorization-systems/identity-modality.lagda.md @@ -42,7 +42,7 @@ unit-id-modality = id ```agda is-uniquely-eliminating-modality-id-modality : {l : Level} → is-uniquely-eliminating-modality (unit-id-modality {l}) -is-uniquely-eliminating-modality-id-modality {l} _ P = +is-uniquely-eliminating-modality-id-modality {l} P = is-local-dependent-type-is-equiv ( unit-id-modality) ( is-equiv-id) diff --git a/src/orthogonal-factorization-systems/modal-induction.lagda.md b/src/orthogonal-factorization-systems/modal-induction.lagda.md new file mode 100644 index 0000000000..0fa26500b1 --- /dev/null +++ b/src/orthogonal-factorization-systems/modal-induction.lagda.md @@ -0,0 +1,320 @@ +# Modal induction + +```agda +module orthogonal-factorization-systems.modal-induction where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.multivariable-sections +open import foundation.retractions +open import foundation.sections +open import foundation.type-theoretic-principle-of-choice +open import foundation.unit-type +open import foundation.universe-levels + +open import orthogonal-factorization-systems.modal-operators +``` + +
+ +## Idea + +Given a [modal operator](orthogonal-factorization-systems.modal-operators.md) +`○` and a modal unit, a **modal induction principle** for the modality is a +[section of maps of maps](foundation.multivariable-sections.md): + +```text + multivariable-section 1 (precomp-Π unit-○ (○ ∘ P)) +``` + +where + +```text + precomp-Π unit-○ (○ ∘ P) : ((x' : ○ X) → ○ (P x')) → (x : X) → ○ (P (unit-○ x)) +``` + +for all families `P` over some `○ X`. + +Note that for such principles to coincide with +[modal subuniverse induction](orthogonal-factorization-systems.modal-subuniverse-induction.md), +the modality must be idempotent. + +## Definition + +### Modal induction + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + ind-modality : UU (lsuc l1 ⊔ l2) + ind-modality = + {X : UU l1} (P : ○ X → UU l1) → + ((x : X) → ○ (P (unit-○ x))) → + (x' : ○ X) → ○ (P x') + + compute-ind-modality : ind-modality → UU (lsuc l1 ⊔ l2) + compute-ind-modality ind-○ = + {X : UU l1} (P : ○ X → UU l1) → + (f : (x : X) → ○ (P (unit-○ x))) → + (x : X) → ind-○ P f (unit-○ x) ＝ f x + + induction-principle-modality : UU (lsuc l1 ⊔ l2) + induction-principle-modality = + {X : UU l1} (P : ○ X → UU l1) → + multivariable-section 1 (precomp-Π unit-○ (○ ∘ P)) + + ind-induction-principle-modality : induction-principle-modality → ind-modality + ind-induction-principle-modality I P = + map-multivariable-section 1 (precomp-Π unit-○ (○ ∘ P)) (I P) + + compute-ind-induction-principle-modality : + (I : induction-principle-modality) → + compute-ind-modality (ind-induction-principle-modality I) + compute-ind-induction-principle-modality I P = + is-multivariable-section-map-multivariable-section 1 + ( precomp-Π unit-○ (○ ∘ P)) + ( I P) +``` + +### Modal recursion + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + rec-modality : UU (lsuc l1 ⊔ l2) + rec-modality = {X Y : UU l1} → (X → ○ Y) → ○ X → ○ Y + + compute-rec-modality : rec-modality → UU (lsuc l1 ⊔ l2) + compute-rec-modality rec-○ = + {X Y : UU l1} → + (f : X → ○ Y) → + (x : X) → rec-○ f (unit-○ x) ＝ f x + + recursion-principle-modality : UU (lsuc l1 ⊔ l2) + recursion-principle-modality = + {X Y : UU l1} → multivariable-section 1 (precomp {A = X} unit-○ (○ Y)) + + rec-recursion-principle-modality : recursion-principle-modality → rec-modality + rec-recursion-principle-modality I {Y = Y} = + map-multivariable-section 1 (precomp unit-○ (○ Y)) I + + compute-rec-recursion-principle-modality : + (I : recursion-principle-modality) → + compute-rec-modality (rec-recursion-principle-modality I) + compute-rec-recursion-principle-modality I {Y = Y} = + is-multivariable-section-map-multivariable-section 1 + ( precomp unit-○ (○ Y)) I +``` + +## Properties + +### Modal recursion from induction + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + rec-ind-modality : ind-modality unit-○ → rec-modality unit-○ + rec-ind-modality ind {Y = Y} = ind (λ _ → Y) + + compute-rec-compute-ind-modality : + (ind-○ : ind-modality unit-○) → + compute-ind-modality unit-○ ind-○ → + compute-rec-modality unit-○ (rec-ind-modality ind-○) + compute-rec-compute-ind-modality ind-○ compute-ind-○ {Y = Y} = + compute-ind-○ (λ _ → Y) + + recursion-principle-induction-principle-modality : + induction-principle-modality unit-○ → recursion-principle-modality unit-○ + recursion-principle-induction-principle-modality I {Y = Y} = I (λ _ → Y) +``` + +### Modal induction gives an inverse to the unit + +```agda +is-section-ind-modality : + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + (ind-○ : ind-modality unit-○) + (compute-ind-○ : compute-ind-modality unit-○ ind-○) + {X : UU l1} {P : ○ X → UU l1} → (precomp-Π unit-○ (○ ∘ P) ∘ ind-○ P) ~ id +is-section-ind-modality unit-○ ind-○ compute-ind-○ {X} {P} = + eq-htpy ∘ compute-ind-○ P + +is-retraction-ind-id-modality : + {l : Level} + {○ : operator-modality l l} + (unit-○ : unit-modality ○) + (ind-○ : ind-modality unit-○) + (compute-ind-○ : compute-ind-modality unit-○ ind-○) + {X : UU l} → (ind-○ (λ _ → X) id ∘ unit-○) ~ id +is-retraction-ind-id-modality {○ = ○} unit-○ ind-○ compute-ind-○ {X} = + compute-ind-○ (λ _ → X) id + +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + (rec-○ : rec-modality unit-○) + (compute-rec-○ : compute-rec-modality unit-○ rec-○) + where + + is-retraction-rec-map-modality : + {X Y : UU l1} (f : ○ X → Y) (r : retraction f) → + (rec-○ (map-retraction f r) ∘ (unit-○ ∘ f)) ~ id + is-retraction-rec-map-modality {X} {Y} f r = + ( compute-rec-○ (map-retraction f r) ∘ f) ∙h + ( is-retraction-map-retraction f r) + + retraction-rec-map-modality : + {X Y : UU l1} (f : ○ X → Y) → + retraction f → retraction (unit-○ ∘ f) + pr1 (retraction-rec-map-modality {X} {Y} f r) = rec-○ (map-retraction f r) + pr2 (retraction-rec-map-modality f r) = is-retraction-rec-map-modality f r + + section-rec-map-modality : + {X Y : UU l1} (f : X → ○ Y) → + section f → section (rec-○ f) + pr1 (section-rec-map-modality f s) = unit-○ ∘ map-section f s + pr2 (section-rec-map-modality {X} {Y} f s) = + (compute-rec-○ f ∘ map-section f s) ∙h is-section-map-section f s +``` + +### A modal induction principle consists precisely of an induction rule and a computation rule + +```agda +equiv-section-unit-induction-principle-modality : + { l1 l2 : Level} + { ○ : operator-modality l1 l2} + ( unit-○ : unit-modality ○) → + ( induction-principle-modality unit-○) ≃ + Σ ( {X : UU l1} (P : ○ X → UU l1) → + ((x : X) → ○ (P (unit-○ x))) → (x' : ○ X) → ○ (P x')) + ( λ I → + {X : UU l1} (P : ○ X → UU l1) (f : (x : X) → ○ (P (unit-○ x))) → + I P f ∘ unit-○ ~ f) +equiv-section-unit-induction-principle-modality unit-○ = + distributive-implicit-Π-Σ ∘e + equiv-implicit-Π-equiv-family (λ _ → distributive-Π-Σ) + +equiv-section-unit-recursion-principle-modality : + { l1 l2 : Level} + { ○ : operator-modality l1 l2} + ( unit-○ : unit-modality ○) → + ( recursion-principle-modality unit-○) ≃ + Σ ( {X Y : UU l1} → (X → ○ Y) → ○ X → ○ Y) + ( λ I → {X Y : UU l1} (f : X → ○ Y) → I f ∘ unit-○ ~ f) +equiv-section-unit-recursion-principle-modality unit-○ = + distributive-implicit-Π-Σ ∘e + equiv-implicit-Π-equiv-family (λ _ → distributive-implicit-Π-Σ) +``` + +### The modal operator's action on maps + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + ap-map-rec-modality : + rec-modality unit-○ → {X Y : UU l1} → (X → Y) → ○ X → ○ Y + ap-map-rec-modality rec-○ f = rec-○ (unit-○ ∘ f) + + ap-map-ind-modality : + ind-modality unit-○ → {X Y : UU l1} → (X → Y) → ○ X → ○ Y + ap-map-ind-modality ind-○ = + ap-map-rec-modality (rec-ind-modality unit-○ ind-○) +``` + +### Naturality of the unit + +For every `f : X → Y` there is an associated +[naturality square](foundation-core.commuting-squares-of-maps.md) + +```text + f + X ------> Y + | | + | | + v v + ○ X ----> ○ Y. + ○ f +``` + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + (rec-○ : rec-modality unit-○) + (compute-rec-○ : compute-rec-modality unit-○ rec-○) + where + + naturality-unit-rec-modality : + {X Y : UU l1} (f : X → Y) → + (ap-map-rec-modality unit-○ rec-○ f ∘ unit-○) ~ (unit-○ ∘ f) + naturality-unit-rec-modality f = + compute-rec-○ (unit-○ ∘ f) + + naturality-unit-rec-modality' : + {X Y : UU l1} (f : X → Y) {x x' : X} → + unit-○ x ＝ unit-○ x' → unit-○ (f x) ＝ unit-○ (f x') + naturality-unit-rec-modality' f {x} {x'} p = + ( inv (naturality-unit-rec-modality f x)) ∙ + ( ( ap (ap-map-rec-modality unit-○ rec-○ f) p) ∙ + ( naturality-unit-rec-modality f x')) + +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + (ind-○ : ind-modality unit-○) + (compute-ind-○ : compute-ind-modality unit-○ ind-○) + where + + naturality-unit-ind-modality : + {X Y : UU l1} (f : X → Y) → + ap-map-ind-modality unit-○ ind-○ f ∘ unit-○ ~ unit-○ ∘ f + naturality-unit-ind-modality = + naturality-unit-rec-modality unit-○ + ( rec-ind-modality unit-○ ind-○) + ( compute-rec-compute-ind-modality unit-○ ind-○ compute-ind-○) + + naturality-unit-ind-modality' : + {X Y : UU l1} (f : X → Y) {x x' : X} → + unit-○ x ＝ unit-○ x' → unit-○ (f x) ＝ unit-○ (f x') + naturality-unit-ind-modality' = + naturality-unit-rec-modality' unit-○ + ( rec-ind-modality unit-○ ind-○) + ( compute-rec-compute-ind-modality unit-○ ind-○ compute-ind-○) +``` + +## See also + +- [Functoriality of higher modalities](orthogonal-factorization-systems.functoriality-higher-modalities.md) +- [Modal subuniverse induction](orthogonal-factorization-systems.modal-subuniverse-induction.md) diff --git a/src/orthogonal-factorization-systems/modal-operators.lagda.md b/src/orthogonal-factorization-systems/modal-operators.lagda.md index d178089800..6f6a038a5e 100644 --- a/src/orthogonal-factorization-systems/modal-operators.lagda.md +++ b/src/orthogonal-factorization-systems/modal-operators.lagda.md @@ -51,15 +51,17 @@ module _ is-modal : (X : UU l1) → UU (l1 ⊔ l2) is-modal X = is-equiv (unit-○ {X}) + is-modal-family : {l3 : Level} {X : UU l3} (P : X → UU l1) → UU (l1 ⊔ l2 ⊔ l3) + is-modal-family {X = X} P = (x : X) → is-modal (P x) + modal-type : UU (lsuc l1 ⊔ l2) modal-type = Σ (UU l1) (is-modal) - is-property-is-modal : (X : UU l1) → is-prop (is-modal X) - is-property-is-modal X = is-property-is-equiv (unit-○ {X}) - is-modal-Prop : (X : UU l1) → Prop (l1 ⊔ l2) - pr1 (is-modal-Prop X) = is-modal X - pr2 (is-modal-Prop X) = is-property-is-modal X + is-modal-Prop X = is-equiv-Prop (unit-○ {X}) + + is-property-is-modal : (X : UU l1) → is-prop (is-modal X) + is-property-is-modal X = is-prop-type-Prop (is-modal-Prop X) is-subuniverse-is-modal : is-subuniverse is-modal is-subuniverse-is-modal = is-property-is-modal diff --git a/src/orthogonal-factorization-systems/modal-subuniverse-induction.lagda.md b/src/orthogonal-factorization-systems/modal-subuniverse-induction.lagda.md new file mode 100644 index 0000000000..8ff23a0246 --- /dev/null +++ b/src/orthogonal-factorization-systems/modal-subuniverse-induction.lagda.md @@ -0,0 +1,480 @@ +# Modal subuniverse induction + +```agda +module orthogonal-factorization-systems.modal-subuniverse-induction where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.multivariable-sections +open import foundation.retractions +open import foundation.type-theoretic-principle-of-choice +open import foundation.universe-levels + +open import orthogonal-factorization-systems.modal-induction +open import orthogonal-factorization-systems.modal-operators +``` + +
+ +## Idea + +Given a [modal operator](orthogonal-factorization-systems.modal-operators.md) +`○` and a modal unit, we can form the [subuniverse](foundation.subuniverses.md) +of modal types as those types whose unit is an +[equivalence](foundation-core.equivalences.md). A **modal subuniverse induction +principle** for the modality is then a +[section of maps of maps](foundation.multivariable-sections.md): + +```text + multivariable-section (precomp-Π unit-○ P) +``` + +where + +```text + precomp-Π unit-○ P : ((x' : ○ X) → P x') → (x : X) → P (unit-○ x) +``` + +for all families of modal types `P` over some `○ X`. + +Note that for such principles to coincide with +[modal induction](orthogonal-factorization-systems.modal-induction.md), the +modality must be idempotent. + +## Definition + +### Subuniverse induction + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + induction-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) + induction-principle-subuniverse-modality = + {X : UU l1} (P : ○ X → UU l1) (is-modal-P : is-modal-family unit-○ P) → + multivariable-section 1 (precomp-Π unit-○ P) + + ind-subuniverse-modality : UU (lsuc l1 ⊔ l2) + ind-subuniverse-modality = + {X : UU l1} (P : ○ X → UU l1) → is-modal-family unit-○ P → + ((x : X) → P (unit-○ x)) → (x' : ○ X) → P x' + + compute-ind-subuniverse-modality : + ind-subuniverse-modality → UU (lsuc l1 ⊔ l2) + compute-ind-subuniverse-modality ind-○ = + {X : UU l1} (P : ○ X → UU l1) (is-modal-P : is-modal-family unit-○ P) → + (f : (x : X) → P (unit-○ x)) → ind-○ P is-modal-P f ∘ unit-○ ~ f + + ind-induction-principle-subuniverse-modality : + induction-principle-subuniverse-modality → ind-subuniverse-modality + ind-induction-principle-subuniverse-modality I P is-modal-P = + map-multivariable-section 1 (precomp-Π unit-○ P) (I P is-modal-P) + + compute-ind-induction-principle-subuniverse-modality : + (I : induction-principle-subuniverse-modality) → + compute-ind-subuniverse-modality + ( ind-induction-principle-subuniverse-modality I) + compute-ind-induction-principle-subuniverse-modality I P is-modal-P = + is-multivariable-section-map-multivariable-section 1 + ( precomp-Π unit-○ P) + ( I P is-modal-P) +``` + +### Subuniverse recursion + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + recursion-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) + recursion-principle-subuniverse-modality = + {X Y : UU l1} → is-modal unit-○ Y → + multivariable-section 1 (precomp {A = X} unit-○ Y) + + rec-subuniverse-modality : UU (lsuc l1 ⊔ l2) + rec-subuniverse-modality = + {X Y : UU l1} → is-modal unit-○ Y → (X → Y) → ○ X → Y + + compute-rec-subuniverse-modality : + rec-subuniverse-modality → UU (lsuc l1 ⊔ l2) + compute-rec-subuniverse-modality rec-○ = + {X Y : UU l1} (is-modal-Y : is-modal unit-○ Y) → + (f : X → Y) → rec-○ is-modal-Y f ∘ unit-○ ~ f + + rec-recursion-principle-subuniverse-modality : + recursion-principle-subuniverse-modality → rec-subuniverse-modality + rec-recursion-principle-subuniverse-modality I {Y = Y} is-modal-Y = + map-multivariable-section 1 (precomp unit-○ Y) (I is-modal-Y) + + compute-rec-recursion-principle-subuniverse-modality : + (I : recursion-principle-subuniverse-modality) → + compute-rec-subuniverse-modality + ( rec-recursion-principle-subuniverse-modality I) + compute-rec-recursion-principle-subuniverse-modality I {Y = Y} is-modal-Y = + is-multivariable-section-map-multivariable-section 1 + ( precomp unit-○ Y) + ( I is-modal-Y) +``` + +### Strong subuniverse induction + +We can weaken the assumption that the codomain is modal and only ask that the +unit has a [retraction](foundation-core.retractions.md). We call this principle +**strong subuniverse induction**. Note that such a retraction may not in general +be [unique](foundation-core.contractible-types.md), and the computational +behaviour of this induction principle depends on the choice of retraction. + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + strong-induction-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) + strong-induction-principle-subuniverse-modality = + {X : UU l1} (P : ○ X → UU l1) → + ((x' : ○ X) → retraction (unit-○ {P x'})) → + multivariable-section 1 (precomp-Π unit-○ P) + + strong-ind-subuniverse-modality : UU (lsuc l1 ⊔ l2) + strong-ind-subuniverse-modality = + {X : UU l1} (P : ○ X → UU l1) → + ((x' : ○ X) → retraction (unit-○ {P x'})) → + ((x : X) → P (unit-○ x)) → (x' : ○ X) → P x' + + compute-strong-ind-subuniverse-modality : + strong-ind-subuniverse-modality → UU (lsuc l1 ⊔ l2) + compute-strong-ind-subuniverse-modality ind-○ = + {X : UU l1} (P : ○ X → UU l1) → + (is-premodal-P : (x' : ○ X) → retraction (unit-○ {P x'})) → + (f : (x : X) → P (unit-○ x)) → ind-○ P is-premodal-P f ∘ unit-○ ~ f + + strong-ind-strong-induction-principle-subuniverse-modality : + strong-induction-principle-subuniverse-modality → + strong-ind-subuniverse-modality + strong-ind-strong-induction-principle-subuniverse-modality + I P is-premodal-P = + map-multivariable-section 1 (precomp-Π unit-○ P) (I P is-premodal-P) + + compute-strong-ind-strong-induction-principle-subuniverse-modality : + (I : strong-induction-principle-subuniverse-modality) → + compute-strong-ind-subuniverse-modality + ( strong-ind-strong-induction-principle-subuniverse-modality I) + compute-strong-ind-strong-induction-principle-subuniverse-modality + I P is-premodal-P = + is-multivariable-section-map-multivariable-section 1 + ( precomp-Π unit-○ P) + ( I P is-premodal-P) +``` + +### Strong subuniverse recursion + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + strong-recursion-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) + strong-recursion-principle-subuniverse-modality = + {X Y : UU l1} → retraction (unit-○ {Y}) → + multivariable-section 1 (precomp {A = X} unit-○ Y) + + strong-rec-subuniverse-modality : UU (lsuc l1 ⊔ l2) + strong-rec-subuniverse-modality = + {X Y : UU l1} → retraction (unit-○ {Y}) → + (X → Y) → ○ X → Y + + compute-strong-rec-subuniverse-modality : + strong-rec-subuniverse-modality → UU (lsuc l1 ⊔ l2) + compute-strong-rec-subuniverse-modality rec-○ = + {X Y : UU l1} (is-premodal-Y : retraction (unit-○ {Y})) → + (f : X → Y) → rec-○ is-premodal-Y f ∘ unit-○ ~ f + + strong-rec-strong-recursion-principle-subuniverse-modality : + strong-recursion-principle-subuniverse-modality → + strong-rec-subuniverse-modality + strong-rec-strong-recursion-principle-subuniverse-modality + I {Y = Y} is-premodal-Y = + map-multivariable-section 1 (precomp unit-○ Y) (I is-premodal-Y) + + compute-strong-rec-strong-recursion-principle-subuniverse-modality : + (I : strong-recursion-principle-subuniverse-modality) → + compute-strong-rec-subuniverse-modality + ( strong-rec-strong-recursion-principle-subuniverse-modality I) + compute-strong-rec-strong-recursion-principle-subuniverse-modality + I {Y = Y} is-premodal-Y = + is-multivariable-section-map-multivariable-section 1 + ( precomp unit-○ Y) + ( I is-premodal-Y) +``` + +## Properties + +### Subuniverse recursion from subuniverse induction + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + rec-subuniverse-ind-subuniverse-modality : + ind-subuniverse-modality unit-○ → rec-subuniverse-modality unit-○ + rec-subuniverse-ind-subuniverse-modality ind-○ {Y = Y} is-modal-Y = + ind-○ (λ _ → Y) (λ _ → is-modal-Y) + + compute-rec-subuniverse-compute-ind-subuniverse-modality : + (ind-○ : ind-subuniverse-modality unit-○) → + compute-ind-subuniverse-modality unit-○ ind-○ → + compute-rec-subuniverse-modality unit-○ + ( rec-subuniverse-ind-subuniverse-modality ind-○) + compute-rec-subuniverse-compute-ind-subuniverse-modality + ind-○ compute-ind-○ {Y = Y} is-modal-Y = + compute-ind-○ (λ _ → Y) (λ _ → is-modal-Y) + + recursion-principle-induction-principle-subuniverse-modality : + induction-principle-subuniverse-modality unit-○ → + recursion-principle-subuniverse-modality unit-○ + recursion-principle-induction-principle-subuniverse-modality + I {Y = Y} is-modal-Y = + I (λ _ → Y) (λ _ → is-modal-Y) +``` + +### Subuniverse induction from strong subuniverse induction + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + ind-subuniverse-strong-ind-subuniverse-modality : + strong-ind-subuniverse-modality unit-○ → ind-subuniverse-modality unit-○ + ind-subuniverse-strong-ind-subuniverse-modality ind-○ P is-modal-P = + ind-○ P (retraction-is-equiv ∘ is-modal-P) + + compute-ind-subuniverse-strong-ind-subuniverse-modality : + (ind-○ : strong-ind-subuniverse-modality unit-○) → + compute-strong-ind-subuniverse-modality unit-○ ind-○ → + compute-ind-subuniverse-modality unit-○ + ( ind-subuniverse-strong-ind-subuniverse-modality ind-○) + compute-ind-subuniverse-strong-ind-subuniverse-modality + ind-○ compute-ind-○ P is-modal-P = + compute-ind-○ P (retraction-is-equiv ∘ is-modal-P) + + induction-principle-strong-induction-principle-subuniverse-modality : + strong-induction-principle-subuniverse-modality unit-○ → + induction-principle-subuniverse-modality unit-○ + induction-principle-strong-induction-principle-subuniverse-modality + I P is-modal-P = I P (retraction-is-equiv ∘ is-modal-P) +``` + +### Subuniverse recursion from strong subuniverse recursion + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + rec-subuniverse-strong-rec-subuniverse-modality : + strong-rec-subuniverse-modality unit-○ → rec-subuniverse-modality unit-○ + rec-subuniverse-strong-rec-subuniverse-modality rec-○ is-modal-Y = + rec-○ (retraction-is-equiv is-modal-Y) + + compute-rec-subuniverse-strong-rec-subuniverse-modality : + (rec-○ : strong-rec-subuniverse-modality unit-○) + (compute-rec-○ : compute-strong-rec-subuniverse-modality unit-○ rec-○) → + compute-rec-subuniverse-modality unit-○ + ( rec-subuniverse-strong-rec-subuniverse-modality rec-○) + compute-rec-subuniverse-strong-rec-subuniverse-modality + rec-○ compute-rec-○ is-modal-Y = + compute-rec-○ (retraction-is-equiv is-modal-Y) + + recursion-principle-strong-recursion-principle-subuniverse-modality : + strong-recursion-principle-subuniverse-modality unit-○ → + recursion-principle-subuniverse-modality unit-○ + recursion-principle-strong-recursion-principle-subuniverse-modality + I is-modal-Y = + I (retraction-is-equiv is-modal-Y) +``` + +### Subuniverse induction from modal induction + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + strong-ind-subuniverse-ind-modality : + ind-modality unit-○ → strong-ind-subuniverse-modality unit-○ + strong-ind-subuniverse-ind-modality ind-○ P is-premodal-P f x' = + map-retraction unit-○ (is-premodal-P x') (ind-○ P (unit-○ ∘ f) x') + + compute-strong-ind-subuniverse-ind-modality : + (ind-○ : ind-modality unit-○) → + compute-ind-modality unit-○ ind-○ → + compute-strong-ind-subuniverse-modality unit-○ + ( strong-ind-subuniverse-ind-modality ind-○) + compute-strong-ind-subuniverse-ind-modality + ind-○ compute-ind-○ P is-premodal-P f x = + ( ap + ( map-retraction unit-○ (is-premodal-P (unit-○ x))) + ( compute-ind-○ P (unit-○ ∘ f) x)) ∙ + ( is-retraction-map-retraction unit-○ (is-premodal-P (unit-○ x)) (f x)) + + strong-induction-principle-subuniverse-induction-principle-modality : + induction-principle-modality unit-○ → + strong-induction-principle-subuniverse-modality unit-○ + pr1 + ( strong-induction-principle-subuniverse-induction-principle-modality + I P is-modal-P) = + strong-ind-subuniverse-ind-modality + ( ind-induction-principle-modality unit-○ I) P is-modal-P + pr2 + ( strong-induction-principle-subuniverse-induction-principle-modality + I P is-modal-P) = + compute-strong-ind-subuniverse-ind-modality + ( ind-induction-principle-modality unit-○ I) + ( compute-ind-induction-principle-modality unit-○ I) + ( P) + ( is-modal-P) + + ind-subuniverse-ind-modality : + ind-modality unit-○ → ind-subuniverse-modality unit-○ + ind-subuniverse-ind-modality ind-○ = + ind-subuniverse-strong-ind-subuniverse-modality unit-○ + ( strong-ind-subuniverse-ind-modality ind-○) + + compute-ind-subuniverse-ind-modality : + (ind-○ : ind-modality unit-○) → + compute-ind-modality unit-○ ind-○ → + compute-ind-subuniverse-modality unit-○ + ( ind-subuniverse-ind-modality ind-○) + compute-ind-subuniverse-ind-modality ind-○ compute-ind-○ = + compute-ind-subuniverse-strong-ind-subuniverse-modality unit-○ + ( strong-ind-subuniverse-ind-modality ind-○) + ( compute-strong-ind-subuniverse-ind-modality ind-○ compute-ind-○) + + induction-principle-subuniverse-induction-principle-modality : + induction-principle-modality unit-○ → + induction-principle-subuniverse-modality unit-○ + pr1 + ( induction-principle-subuniverse-induction-principle-modality + I P is-modal-P) = + ind-subuniverse-ind-modality + ( ind-induction-principle-modality unit-○ I) + ( P) + ( is-modal-P) + pr2 + ( induction-principle-subuniverse-induction-principle-modality + I P is-modal-P) = + compute-ind-subuniverse-ind-modality + ( ind-induction-principle-modality unit-○ I) + ( compute-ind-induction-principle-modality unit-○ I) + ( P) + ( is-modal-P) +``` + +### Subuniverse recursion from modal recursion + +```agda +module _ + {l1 l2 : Level} + {○ : operator-modality l1 l2} + (unit-○ : unit-modality ○) + where + + strong-rec-subuniverse-rec-modality : + rec-modality unit-○ → strong-rec-subuniverse-modality unit-○ + strong-rec-subuniverse-rec-modality rec-○ is-premodal-Y f x' = + map-retraction unit-○ (is-premodal-Y) (rec-○ (unit-○ ∘ f) x') + + compute-strong-rec-subuniverse-rec-modality : + (rec-○ : rec-modality unit-○) → + compute-rec-modality unit-○ rec-○ → + compute-strong-rec-subuniverse-modality unit-○ + ( strong-rec-subuniverse-rec-modality rec-○) + compute-strong-rec-subuniverse-rec-modality + rec-○ compute-rec-○ is-premodal-Y f x = + ( ap + ( map-retraction unit-○ (is-premodal-Y)) + ( compute-rec-○ (unit-○ ∘ f) x)) ∙ + ( is-retraction-map-retraction unit-○ (is-premodal-Y) (f x)) + + strong-recursion-principle-subuniverse-recursion-principle-modality : + recursion-principle-modality unit-○ → + strong-recursion-principle-subuniverse-modality unit-○ + pr1 + ( strong-recursion-principle-subuniverse-recursion-principle-modality + I is-premodal-Y) = + strong-rec-subuniverse-rec-modality + ( rec-recursion-principle-modality unit-○ I) + ( is-premodal-Y) + pr2 + ( strong-recursion-principle-subuniverse-recursion-principle-modality + I is-premodal-Y) = + compute-strong-rec-subuniverse-rec-modality + ( rec-recursion-principle-modality unit-○ I) + ( compute-rec-recursion-principle-modality unit-○ I) + ( is-premodal-Y) + + rec-subuniverse-rec-modality : + rec-modality unit-○ → rec-subuniverse-modality unit-○ + rec-subuniverse-rec-modality rec-○ = + rec-subuniverse-strong-rec-subuniverse-modality unit-○ + ( strong-rec-subuniverse-rec-modality rec-○) + + compute-rec-subuniverse-rec-modality : + (rec-○ : rec-modality unit-○) → + compute-rec-modality unit-○ rec-○ → + compute-rec-subuniverse-modality unit-○ (rec-subuniverse-rec-modality rec-○) + compute-rec-subuniverse-rec-modality rec-○ compute-rec-○ = + compute-rec-subuniverse-strong-rec-subuniverse-modality unit-○ + ( strong-rec-subuniverse-rec-modality rec-○) + ( compute-strong-rec-subuniverse-rec-modality rec-○ compute-rec-○) + + recursion-principle-subuniverse-recursion-principle-modality : + recursion-principle-modality unit-○ → + recursion-principle-subuniverse-modality unit-○ + pr1 + ( recursion-principle-subuniverse-recursion-principle-modality + I is-modal-Y) = + rec-subuniverse-rec-modality + ( rec-recursion-principle-modality unit-○ I) is-modal-Y + pr2 + ( recursion-principle-subuniverse-recursion-principle-modality + I is-modal-Y) = + compute-rec-subuniverse-rec-modality + ( rec-recursion-principle-modality unit-○ I) + ( compute-rec-recursion-principle-modality unit-○ I) + ( is-modal-Y) +``` + +## See also + +- [Modal induction](orthogonal-factorization-systems.modal-induction.md) +- [Reflective subuniverses](orthogonal-factorization-systems.reflective-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/open-modalities.lagda.md b/src/orthogonal-factorization-systems/open-modalities.lagda.md index 45a170fa4c..f20203e06c 100644 --- a/src/orthogonal-factorization-systems/open-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/open-modalities.lagda.md @@ -19,6 +19,7 @@ open import foundation.universe-levels open import orthogonal-factorization-systems.higher-modalities open import orthogonal-factorization-systems.locally-small-modal-operators +open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.uniquely-eliminating-modalities ``` @@ -60,30 +61,31 @@ module _ where ind-open-modality : ind-modality {l} (unit-open-modality Q) - ind-open-modality X P f z q = + ind-open-modality P f z q = tr P (eq-htpy λ q' → ap z (eq-is-prop (is-prop-type-Prop Q))) (f (z q) q) compute-ind-open-modality : compute-ind-modality {l} (unit-open-modality Q) (ind-open-modality) - compute-ind-open-modality X P f a = + compute-ind-open-modality P f a = eq-htpy - ( λ q → - ap - ( λ p → tr P p (f a q)) - ( ( ap - ( eq-htpy) - ( eq-htpy - ( λ _ → ap-const a (eq-is-prop (is-prop-type-Prop Q))))) ∙ - ( eq-htpy-refl-htpy (λ _ → a)))) - - dependent-universal-property-open-modality : - dependent-universal-property-modality {l} (unit-open-modality Q) - pr1 dependent-universal-property-open-modality = ind-open-modality - pr2 dependent-universal-property-open-modality = compute-ind-open-modality + ( λ q → + ap + ( λ p → tr P p (f a q)) + ( ( ap + ( eq-htpy) + ( eq-htpy + ( λ _ → ap-const a (eq-is-prop (is-prop-type-Prop Q))))) ∙ + ( eq-htpy-refl-htpy (λ _ → a)))) + + induction-principle-open-modality : + induction-principle-modality {l} (unit-open-modality Q) + pr1 (induction-principle-open-modality P) = ind-open-modality P + pr2 (induction-principle-open-modality P) = compute-ind-open-modality P ``` -For local smallness with respect to the appropriate universe level, we must take -the maximum of `l` and `lQ` as our domain. In practice, this allows `lQ` to be +For [local smallness](foundation.locally-small-types.md) with respect to the +appropriate [universe level](foundation.universe-levels.md), we must take the +maximum of `l` and `lQ` as our domain. In practice, this only allows `lQ` to be smaller than `l`. ```agda @@ -92,7 +94,7 @@ module _ where is-modal-identity-types-open-modality : - is-modal-identity-types + is-modal-small-identity-types ( locally-small-operator-open-modality (l ⊔ lQ) Q) ( unit-open-modality Q) is-modal-identity-types-open-modality X x y = @@ -116,7 +118,7 @@ module _ ( locally-small-operator-open-modality (l ⊔ lQ) Q) ( unit-open-modality Q) pr1 is-higher-modality-open-modality = - dependent-universal-property-open-modality Q + induction-principle-open-modality Q pr2 is-higher-modality-open-modality = is-modal-identity-types-open-modality @@ -133,5 +135,5 @@ is-uniquely-eliminating-modality-open-modality : (l : Level) {lQ : Level} (Q : Prop lQ) → is-uniquely-eliminating-modality {l ⊔ lQ} (unit-open-modality Q) is-uniquely-eliminating-modality-open-modality l Q = - is-uniquely-eliminating-modality-higher-modality (open-higher-modality l Q) + is-uniquely-eliminating-higher-modality (open-higher-modality l Q) ``` diff --git a/src/orthogonal-factorization-systems/raise-modalities.lagda.md b/src/orthogonal-factorization-systems/raise-modalities.lagda.md index eaf3235f1e..2b0597b2fa 100644 --- a/src/orthogonal-factorization-systems/raise-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/raise-modalities.lagda.md @@ -46,7 +46,7 @@ unit-raise-modality = map-raise is-uniquely-eliminating-modality-raise-modality : {l1 l2 : Level} → is-uniquely-eliminating-modality (unit-raise-modality {l1} {l2}) -is-uniquely-eliminating-modality-raise-modality {l1} {l2} _ P = +is-uniquely-eliminating-modality-raise-modality {l1} {l2} P = is-local-dependent-type-is-equiv ( unit-raise-modality) ( is-equiv-map-raise) diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md index d2f588bdd1..6b35ebe7ee 100644 --- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md @@ -7,15 +7,23 @@ module orthogonal-factorization-systems.reflective-subuniverses where
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.identity-types open import foundation.propositions +open import foundation.retractions open import foundation.subuniverses open import foundation.universe-levels open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.localizations-subuniverses +open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.modal-subuniverse-induction ```
@@ -36,39 +44,39 @@ precisely the types in the reflective subuniverse. ```agda is-reflective-subuniverse : - {l lP : Level} (P : UU l → Prop lP) → UU (lsuc l ⊔ lP) -is-reflective-subuniverse {l} P = - Σ ( operator-modality l l) + {l1 l2 : Level} (P : UU l1 → Prop l2) → UU (lsuc l1 ⊔ l2) +is-reflective-subuniverse {l1} P = + Σ ( operator-modality l1 l1) ( λ ○ → Σ ( unit-modality ○) ( λ unit-○ → - ( (X : UU l) → is-in-subuniverse P (○ X)) × - ( (X Y : UU l) → is-in-subuniverse P X → is-local (unit-○ {Y}) X))) + ( (X : UU l1) → is-in-subuniverse P (○ X)) × + ( (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-○ {Y}) X))) ``` ```agda module _ - {l lP : Level} (P : subuniverse l lP) + {l1 l2 : Level} (P : subuniverse l1 l2) (is-reflective-P : is-reflective-subuniverse P) where - operator-modality-is-reflective-subuniverse : operator-modality l l - operator-modality-is-reflective-subuniverse = pr1 is-reflective-P + operator-is-reflective-subuniverse : operator-modality l1 l1 + operator-is-reflective-subuniverse = pr1 is-reflective-P - unit-modality-is-reflective-subuniverse : - unit-modality (operator-modality-is-reflective-subuniverse) - unit-modality-is-reflective-subuniverse = pr1 (pr2 is-reflective-P) + unit-is-reflective-subuniverse : + unit-modality (operator-is-reflective-subuniverse) + unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-P) - is-in-subuniverse-image-operator-modality-is-reflective-subuniverse : - (X : UU l) → - is-in-subuniverse P (operator-modality-is-reflective-subuniverse X) - is-in-subuniverse-image-operator-modality-is-reflective-subuniverse = + is-in-subuniverse-operator-type-is-reflective-subuniverse : + (X : UU l1) → + is-in-subuniverse P (operator-is-reflective-subuniverse X) + is-in-subuniverse-operator-type-is-reflective-subuniverse = pr1 (pr2 (pr2 is-reflective-P)) is-local-is-in-subuniverse-is-reflective-subuniverse : - (X Y : UU l) → + (X Y : UU l1) → is-in-subuniverse P X → - is-local (unit-modality-is-reflective-subuniverse {Y}) X + is-local (unit-is-reflective-subuniverse {Y}) X is-local-is-in-subuniverse-is-reflective-subuniverse = pr2 (pr2 (pr2 is-reflective-P)) ``` @@ -76,25 +84,25 @@ module _ ### The type of reflective subuniverses ```agda -reflective-subuniverse : (l lP : Level) → UU (lsuc l ⊔ lsuc lP) -reflective-subuniverse l lP = - Σ (UU l → Prop lP) (is-reflective-subuniverse) +reflective-subuniverse : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +reflective-subuniverse l1 l2 = + Σ (UU l1 → Prop l2) (is-reflective-subuniverse) ``` ```agda module _ - {l lP : Level} (P : reflective-subuniverse l lP) + {l1 l2 : Level} (P : reflective-subuniverse l1 l2) where - subuniverse-reflective-subuniverse : subuniverse l lP + subuniverse-reflective-subuniverse : subuniverse l1 l2 subuniverse-reflective-subuniverse = pr1 P - is-in-reflective-subuniverse : UU l → UU lP + is-in-reflective-subuniverse : UU l1 → UU l2 is-in-reflective-subuniverse = is-in-subuniverse subuniverse-reflective-subuniverse inclusion-reflective-subuniverse : - type-subuniverse (subuniverse-reflective-subuniverse) → UU l + type-subuniverse (subuniverse-reflective-subuniverse) → UU l1 inclusion-reflective-subuniverse = inclusion-subuniverse subuniverse-reflective-subuniverse @@ -102,33 +110,33 @@ module _ is-reflective-subuniverse (subuniverse-reflective-subuniverse) is-reflective-subuniverse-reflective-subuniverse = pr2 P - operator-modality-reflective-subuniverse : operator-modality l l - operator-modality-reflective-subuniverse = - operator-modality-is-reflective-subuniverse + operator-reflective-subuniverse : operator-modality l1 l1 + operator-reflective-subuniverse = + operator-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) - unit-modality-reflective-subuniverse : - unit-modality (operator-modality-reflective-subuniverse) - unit-modality-reflective-subuniverse = - unit-modality-is-reflective-subuniverse + unit-reflective-subuniverse : + unit-modality (operator-reflective-subuniverse) + unit-reflective-subuniverse = + unit-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) - is-in-subuniverse-image-operator-modality-reflective-subuniverse : - ( X : UU l) → + is-in-subuniverse-operator-type-reflective-subuniverse : + ( X : UU l1) → is-in-subuniverse ( subuniverse-reflective-subuniverse) - ( operator-modality-reflective-subuniverse X) - is-in-subuniverse-image-operator-modality-reflective-subuniverse = - is-in-subuniverse-image-operator-modality-is-reflective-subuniverse + ( operator-reflective-subuniverse X) + is-in-subuniverse-operator-type-reflective-subuniverse = + is-in-subuniverse-operator-type-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) is-local-is-in-subuniverse-reflective-subuniverse : - ( X Y : UU l) → + ( X Y : UU l1) → is-in-subuniverse subuniverse-reflective-subuniverse X → - is-local (unit-modality-reflective-subuniverse {Y}) X + is-local (unit-reflective-subuniverse {Y}) X is-local-is-in-subuniverse-reflective-subuniverse = is-local-is-in-subuniverse-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) @@ -141,27 +149,27 @@ module _ ```agda module _ - {l lP : Level} (P : subuniverse l lP) + {l1 l2 : Level} (P : subuniverse l1 l2) (is-reflective-P : is-reflective-subuniverse P) where has-all-localizations-is-reflective-subuniverse : - (A : UU l) → subuniverse-localization P A + (A : UU l1) → subuniverse-localization P A pr1 (has-all-localizations-is-reflective-subuniverse A) = - operator-modality-is-reflective-subuniverse P is-reflective-P A + operator-is-reflective-subuniverse P is-reflective-P A pr1 (pr2 (has-all-localizations-is-reflective-subuniverse A)) = - is-in-subuniverse-image-operator-modality-is-reflective-subuniverse + is-in-subuniverse-operator-type-is-reflective-subuniverse P is-reflective-P A pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) = - unit-modality-is-reflective-subuniverse P is-reflective-P + unit-is-reflective-subuniverse P is-reflective-P pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) X is-in-subuniverse-X = is-local-is-in-subuniverse-is-reflective-subuniverse P is-reflective-P X A is-in-subuniverse-X module _ - {l lP : Level} (P : subuniverse l lP) - (L : (A : UU l) → subuniverse-localization P A) + {l1 l2 : Level} (P : subuniverse l1 l2) + (L : (A : UU l1) → subuniverse-localization P A) where is-reflective-has-all-localizations-subuniverse : @@ -178,6 +186,53 @@ module _ P (L B) A is-in-subuniverse-A ``` +## Recursion for reflective subuniverses + +```agda +module _ + {l1 l2 : Level} (P : subuniverse l1 l2) + (is-reflective-P : is-reflective-subuniverse P) + where + + rec-modality-is-reflective-subuniverse : + rec-modality (unit-is-reflective-subuniverse P is-reflective-P) + rec-modality-is-reflective-subuniverse {X} {Y} = + map-inv-is-equiv + ( is-local-is-in-subuniverse-is-reflective-subuniverse + ( P) + ( is-reflective-P) + ( operator-is-reflective-subuniverse P is-reflective-P Y) + ( X) + ( is-in-subuniverse-operator-type-is-reflective-subuniverse + ( P) + ( is-reflective-P) + ( Y))) + + map-is-reflective-subuniverse : + {X Y : UU l1} → (X → Y) → + operator-is-reflective-subuniverse P is-reflective-P X → + operator-is-reflective-subuniverse P is-reflective-P Y + map-is-reflective-subuniverse = + ap-map-rec-modality + ( unit-is-reflective-subuniverse P is-reflective-P) + ( rec-modality-is-reflective-subuniverse) + + strong-rec-subuniverse-is-reflective-subuniverse : + strong-rec-subuniverse-modality + ( unit-is-reflective-subuniverse P is-reflective-P) + strong-rec-subuniverse-is-reflective-subuniverse = + strong-rec-subuniverse-rec-modality + ( unit-is-reflective-subuniverse P is-reflective-P) + ( rec-modality-is-reflective-subuniverse) + + rec-subuniverse-is-reflective-subuniverse : + rec-subuniverse-modality (unit-is-reflective-subuniverse P is-reflective-P) + rec-subuniverse-is-reflective-subuniverse = + rec-subuniverse-rec-modality + ( unit-is-reflective-subuniverse P is-reflective-P) + ( rec-modality-is-reflective-subuniverse) +``` + ## See also - [Σ-closed reflective subuniverses](orthogonal-factorization-systems.sigma-closed-reflective-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md index 76f7bdfd1c..2da65f739a 100644 --- a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md @@ -32,7 +32,12 @@ A **uniquely eliminating modality** is a _higher mode of logic_ defined in terms of a monadic [modal operator](orthogonal-factorization-systems.modal-operators.md) `○` satisfying a certain [locality](orthogonal-factorization-systems.local-types.md) -condition. +condition. Namely, that dependent precomposition by the modal unit `unit-○` is +an equivalence for type families over types in the image of the operator: + +```text + - ∘ unit-○ : Π (x : ○ X) (○ (P x)) ≃ Π (x : X) (○ (P (unit-○ x))) +``` ## Definition @@ -41,7 +46,7 @@ is-uniquely-eliminating-modality : {l1 l2 : Level} {○ : operator-modality l1 l2} → unit-modality ○ → UU (lsuc l1 ⊔ l2) is-uniquely-eliminating-modality {l1} {l2} {○} unit-○ = - (X : UU l1) (P : ○ X → UU l1) → is-local-dependent-type (unit-○) (○ ∘ P) + {X : UU l1} (P : ○ X → UU l1) → is-local-dependent-type (unit-○) (○ ∘ P) uniquely-eliminating-modality : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) uniquely-eliminating-modality l1 l2 = @@ -60,16 +65,16 @@ module _ where ind-modality-is-uniquely-eliminating-modality : - (X : UU l1) (P : ○ X → UU l1) → + {X : UU l1} (P : ○ X → UU l1) → ((x : X) → ○ (P (unit-○ x))) → (x' : ○ X) → ○ (P x') - ind-modality-is-uniquely-eliminating-modality X P = - map-inv-is-equiv (is-uem-○ X P) + ind-modality-is-uniquely-eliminating-modality P = + map-inv-is-equiv (is-uem-○ P) compute-ind-modality-is-uniquely-eliminating-modality : - (X : UU l1) (P : ○ X → UU l1) (f : (x : X) → ○ (P (unit-○ x))) → - (pr1 (pr1 (is-uem-○ X P)) f ∘ unit-○) ~ f - compute-ind-modality-is-uniquely-eliminating-modality X P = - htpy-eq ∘ pr2 (pr1 (is-uem-○ X P)) + {X : UU l1} (P : ○ X → UU l1) (f : (x : X) → ○ (P (unit-○ x))) → + (pr1 (pr1 (is-uem-○ P)) f ∘ unit-○) ~ f + compute-ind-modality-is-uniquely-eliminating-modality P = + htpy-eq ∘ pr2 (pr1 (is-uem-○ P)) module _ {l1 l2 : Level} @@ -99,7 +104,7 @@ module _ is-prop-is-uniquely-eliminating-modality : is-prop (is-uniquely-eliminating-modality unit-○) is-prop-is-uniquely-eliminating-modality = - is-prop-Π + is-prop-Π' ( λ X → is-prop-Π ( λ P → is-property-is-local-dependent-type unit-○ (○ ∘ P))) @@ -122,14 +127,13 @@ module _ map-inv-unit-uniquely-eliminating-modality : ○ (○ X) → ○ X map-inv-unit-uniquely-eliminating-modality = - ind-modality-is-uniquely-eliminating-modality is-uem-○ (○ X) (λ _ → X) id + ind-modality-is-uniquely-eliminating-modality is-uem-○ (λ _ → X) id is-section-unit-uniquely-eliminating-modality : (map-inv-unit-uniquely-eliminating-modality ∘ unit-○) ~ id is-section-unit-uniquely-eliminating-modality = compute-ind-modality-is-uniquely-eliminating-modality ( is-uem-○) - ( ○ X) ( λ _ → X) ( id) @@ -139,7 +143,7 @@ module _ htpy-eq ( ap pr1 ( eq-is-contr' - ( is-contr-map-is-equiv (is-uem-○ (○ X) (λ _ → ○ X)) unit-○) + ( is-contr-map-is-equiv (is-uem-○ (λ _ → ○ X)) unit-○) ( unit-○ ∘ map-inv-unit-uniquely-eliminating-modality , eq-htpy ( ap unit-○ ∘ (is-section-unit-uniquely-eliminating-modality))) diff --git a/src/orthogonal-factorization-systems/zero-modality.lagda.md b/src/orthogonal-factorization-systems/zero-modality.lagda.md index 171e5c5dc4..855dba60bc 100644 --- a/src/orthogonal-factorization-systems/zero-modality.lagda.md +++ b/src/orthogonal-factorization-systems/zero-modality.lagda.md @@ -43,7 +43,7 @@ unit-zero-modality _ = raise-star is-uniquely-eliminating-modality-zero-modality : {l1 l2 : Level} → is-uniquely-eliminating-modality (unit-zero-modality {l1} {l2}) -is-uniquely-eliminating-modality-zero-modality {l2 = l2} A P = +is-uniquely-eliminating-modality-zero-modality {l2 = l2} P = is-local-is-contr ( unit-zero-modality) ( raise-unit l2) diff --git a/src/set-theory/cardinalities.lagda.md b/src/set-theory/cardinalities.lagda.md index 6d862dbe3b..a94d5efa5b 100644 --- a/src/set-theory/cardinalities.lagda.md +++ b/src/set-theory/cardinalities.lagda.md @@ -13,6 +13,7 @@ open import foundation.equivalences open import foundation.function-extensionality open import foundation.functoriality-propositional-truncation open import foundation.identity-types +open import foundation.large-binary-relations open import foundation.law-of-excluded-middle open import foundation.mere-embeddings open import foundation.mere-equivalences @@ -27,11 +28,15 @@ open import foundation.universe-levels ## Idea -The cardinality of a set is its isomorphism class. We take isomorphism classes -of sets by set truncating the universe of sets of any given universe level. Note -that this definition takes advantage of the univalence axiom: By the univalence -axiom isomorphic sets are equal, and will be mapped to the same element in the -set truncation of the universe of all sets. +The **cardinality** of a [set](foundation-core.sets.md) is its +[isomorphism](category-theory.isomorphisms-in-categories.md) class. We take +isomorphism classes of sets by [set truncating](foundation.set-truncations.md) +the universe of sets of any given +[universe level](foundation.universe-levels.md). Note that this definition takes +advantage of the [univalence axiom](foundation.univalence.md): By the univalence +axiom [isomorphic sets](foundation.isomorphisms-of-sets.md) are +[equal](foundation-core.identity-types.md), and will be mapped to the same +element in the set truncation of the universe of all sets. ## Definition @@ -60,9 +65,8 @@ leq-cardinality-Prop' {l1} {l2} X = compute-leq-cardinality-Prop' : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - Id - ( leq-cardinality-Prop' X (cardinality Y)) - ( mere-emb-Prop (type-Set X) (type-Set Y)) + ( leq-cardinality-Prop' X (cardinality Y)) ＝ + ( mere-emb-Prop (type-Set X) (type-Set Y)) compute-leq-cardinality-Prop' {l1} {l2} X = triangle-universal-property-trunc-Set ( Prop-Set (l1 ⊔ l2)) @@ -75,7 +79,8 @@ leq-cardinality-Prop {l1} {l2} = ( hom-set-Set (cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) ( leq-cardinality-Prop') -leq-cardinality : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) +leq-cardinality : + {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) leq-cardinality X Y = type-Prop (leq-cardinality-Prop X Y) is-prop-leq-cardinality : @@ -108,7 +113,7 @@ inv-unit-leq-cardinality : mere-emb (type-Set X) (type-Set Y) inv-unit-leq-cardinality X Y = pr1 (compute-leq-cardinality X Y) -refl-leq-cardinality : {l : Level} → is-reflexive (leq-cardinality {l}) +refl-leq-cardinality : is-reflexive-Large-Relation cardinal leq-cardinality refl-leq-cardinality {l} = apply-dependent-universal-property-trunc-Set' ( λ X → set-Prop (leq-cardinality-Prop X X)) @@ -124,38 +129,38 @@ transitive-leq-cardinality : leq-cardinality X Z transitive-leq-cardinality X Y Z = apply-dependent-universal-property-trunc-Set' - (λ u → + ( λ u → set-Prop - (function-Prop - (leq-cardinality u Y) - (function-Prop (leq-cardinality Y Z) - (leq-cardinality-Prop u Z)))) - (λ a → + ( function-Prop + ( leq-cardinality u Y) + ( function-Prop (leq-cardinality Y Z) + ( leq-cardinality-Prop u Z)))) + ( λ a → apply-dependent-universal-property-trunc-Set' - (λ v → + ( λ v → set-Prop (function-Prop (leq-cardinality (cardinality a) v) (function-Prop (leq-cardinality v Z) (leq-cardinality-Prop (cardinality a) Z)))) - (λ b → + ( λ b → apply-dependent-universal-property-trunc-Set' - (λ w → + ( λ w → set-Prop (function-Prop (leq-cardinality (cardinality a) (cardinality b)) (function-Prop (leq-cardinality (cardinality b) w) (leq-cardinality-Prop (cardinality a) w)))) - (λ c aImports ```agda +open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types @@ -14,6 +15,7 @@ open import foundation.disjunction open import foundation.empty-types open import foundation.equivalences open import foundation.function-types +open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.type-arithmetic-cartesian-product-types @@ -22,6 +24,7 @@ open import foundation.type-arithmetic-empty-type open import foundation.type-arithmetic-unit-type open import foundation.unit-type open import foundation.universe-levels +open import foundation.whiskering-homotopies open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.pushouts @@ -46,38 +49,50 @@ join A B = pushout (pr1 {A = A} {B = λ _ → B}) pr2 infixr 15 _*_ _*_ = join -cocone-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → - cocone (pr1 {A = A} {B = λ _ → B}) pr2 (A * B) -cocone-join A B = cocone-pushout pr1 pr2 - -up-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) - {l : Level} → universal-property-pushout l pr1 pr2 (cocone-join A B) -up-join A B = up-pushout pr1 pr2 - -equiv-up-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) - {l : Level} (X : UU l) → (A * B → X) ≃ cocone pr1 pr2 X -equiv-up-join A B = equiv-up-pushout pr1 pr2 - -inl-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → A → A * B -inl-join A B = pr1 (cocone-join A B) - -inr-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → B → A * B -inr-join A B = pr1 (pr2 (cocone-join A B)) - -glue-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) (t : A × B) → - Id (inl-join A B (pr1 t)) (inr-join A B (pr2 t)) -glue-join A B = pr2 (pr2 (cocone-join A B)) - -cogap-join : - {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (X : UU l3) → - cocone pr1 pr2 X → A * B → X -cogap-join A B X = map-inv-is-equiv (up-join A B X) +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + cocone-join : cocone (pr1 {A = A} {B = λ _ → B}) pr2 (A * B) + cocone-join = cocone-pushout pr1 pr2 + + up-join : + {l : Level} → universal-property-pushout l pr1 pr2 (cocone-join) + up-join = up-pushout pr1 pr2 + + equiv-up-join : + {l : Level} (X : UU l) → (A * B → X) ≃ cocone pr1 pr2 X + equiv-up-join = equiv-up-pushout pr1 pr2 + + inl-join : A → A * B + inl-join = pr1 cocone-join + + inr-join : B → A * B + inr-join = pr1 (pr2 cocone-join) + + glue-join : (t : A × B) → inl-join (pr1 t) ＝ inr-join (pr2 t) + glue-join = pr2 (pr2 cocone-join) + + cogap-join : + {l3 : Level} (X : UU l3) → cocone pr1 pr2 X → A * B → X + cogap-join X = map-inv-is-equiv (up-join X) + + compute-inl-cogap-join : + {l3 : Level} {X : UU l3} (c : cocone pr1 pr2 X) → + ( cogap-join X c ∘ inl-join) ~ horizontal-map-cocone pr1 pr2 c + compute-inl-cogap-join = compute-inl-cogap pr1 pr2 + + compute-inr-cogap-join : + {l3 : Level} {X : UU l3} (c : cocone pr1 pr2 X) → + ( cogap-join X c ∘ inr-join) ~ vertical-map-cocone pr1 pr2 c + compute-inr-cogap-join = compute-inr-cogap pr1 pr2 + + compute-glue-cogap-join : + {l3 : Level} {X : UU l3} (c : cocone pr1 pr2 X) → + ( ( cogap-join X c ·l coherence-square-cocone pr1 pr2 cocone-join) ∙h + ( compute-inr-cogap-join c ·r pr2)) ~ + ( compute-inl-cogap-join c ·r pr1) ∙h coherence-square-cocone pr1 pr2 c + compute-glue-cogap-join = compute-glue-cogap pr1 pr2 ``` ## Properties @@ -86,113 +101,114 @@ cogap-join A B X = map-inv-is-equiv (up-join A B X) ```agda is-equiv-inr-join-empty : - {l : Level} (X : UU l) → is-equiv (inr-join empty X) + {l : Level} (X : UU l) → is-equiv (inr-join {A = empty} {B = X}) is-equiv-inr-join-empty X = is-equiv-universal-property-pushout ( pr1) ( pr2) - ( cocone-join empty X) + ( cocone-join) ( is-equiv-pr1-prod-empty X) - ( up-join empty X) + ( up-join) left-unit-law-join : {l : Level} (X : UU l) → X ≃ (empty * X) -pr1 (left-unit-law-join X) = inr-join empty X +pr1 (left-unit-law-join X) = inr-join pr2 (left-unit-law-join X) = is-equiv-inr-join-empty X is-equiv-inr-join-is-empty : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → - is-empty A → is-equiv (inr-join A B) -is-equiv-inr-join-is-empty A B is-empty-A = + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-empty A → is-equiv (inr-join {A = A} {B = B}) +is-equiv-inr-join-is-empty {A = A} {B = B} is-empty-A = is-equiv-universal-property-pushout ( pr1) ( pr2) - ( cocone-join A B) + ( cocone-join) ( is-equiv-pr1-prod-is-empty A B is-empty-A) - ( up-join A B) + ( up-join) left-unit-law-join-is-empty : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → + {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-empty A → B ≃ (A * B) -pr1 (left-unit-law-join-is-empty A B is-empty-A) = inr-join A B -pr2 (left-unit-law-join-is-empty A B is-empty-A) = - is-equiv-inr-join-is-empty A B is-empty-A +pr1 (left-unit-law-join-is-empty is-empty-A) = inr-join +pr2 (left-unit-law-join-is-empty is-empty-A) = + is-equiv-inr-join-is-empty is-empty-A ``` ### The right unit law for joins ```agda is-equiv-inl-join-empty : - {l : Level} (X : UU l) → is-equiv (inl-join X empty) + {l : Level} (X : UU l) → is-equiv (inl-join {A = X} {B = empty}) is-equiv-inl-join-empty X = is-equiv-universal-property-pushout' ( pr1) ( pr2) - ( cocone-join X empty) + ( cocone-join) ( is-equiv-pr2-prod-empty X) - ( up-join X empty) + ( up-join) right-unit-law-join : {l : Level} (X : UU l) → X ≃ (X * empty) -pr1 (right-unit-law-join X) = inl-join X empty +pr1 (right-unit-law-join X) = inl-join pr2 (right-unit-law-join X) = is-equiv-inl-join-empty X is-equiv-inl-join-is-empty : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → - is-empty B → is-equiv (inl-join A B) -is-equiv-inl-join-is-empty A B is-empty-B = + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-empty B → is-equiv (inl-join {A = A} {B = B}) +is-equiv-inl-join-is-empty {A = A} {B = B} is-empty-B = is-equiv-universal-property-pushout' ( pr1) ( pr2) - ( cocone-join A B) + ( cocone-join) ( is-equiv-pr2-prod-is-empty A B is-empty-B) - ( up-join A B) + ( up-join) right-unit-law-join-is-empty : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → + {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-empty B → A ≃ (A * B) -pr1 (right-unit-law-join-is-empty A B is-empty-B) = inl-join A B -pr2 (right-unit-law-join-is-empty A B is-empty-B) = - is-equiv-inl-join-is-empty A B is-empty-B +pr1 (right-unit-law-join-is-empty is-empty-B) = inl-join +pr2 (right-unit-law-join-is-empty is-empty-B) = + is-equiv-inl-join-is-empty is-empty-B ``` ### The left zero law for joins ```agda is-equiv-inl-join-unit : - {l : Level} (X : UU l) → is-equiv (inl-join unit X) + {l : Level} (X : UU l) → is-equiv (inl-join {A = unit} {B = X}) is-equiv-inl-join-unit X = is-equiv-universal-property-pushout' ( pr1) ( pr2) - ( cocone-join unit X) + ( cocone-join) ( is-equiv-map-left-unit-law-prod) - ( up-join unit X) + ( up-join) left-zero-law-join : {l : Level} (X : UU l) → is-contr (unit * X) left-zero-law-join X = is-contr-equiv' ( unit) - ( pair (inl-join unit X) (is-equiv-inl-join-unit X)) + ( inl-join , is-equiv-inl-join-unit X) ( is-contr-unit) is-equiv-inl-join-is-contr : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → is-contr A → is-equiv (inl-join A B) + {l1 l2 : Level} (A : UU l1) (B : UU l2) → + is-contr A → is-equiv (inl-join {A = A} {B = B}) is-equiv-inl-join-is-contr A B is-contr-A = is-equiv-universal-property-pushout' ( pr1) ( pr2) - ( cocone-join A B) + ( cocone-join) ( is-equiv-pr2-prod-is-contr is-contr-A) - ( up-join A B) + ( up-join) left-zero-law-join-is-contr : {l1 l2 : Level} (A : UU l1) (B : UU l2) → is-contr A → is-contr (A * B) left-zero-law-join-is-contr A B is-contr-A = is-contr-equiv' ( A) - ( pair (inl-join A B) (is-equiv-inl-join-is-contr A B is-contr-A)) + ( inl-join , is-equiv-inl-join-is-contr A B is-contr-A) ( is-contr-A) ``` @@ -200,39 +216,40 @@ left-zero-law-join-is-contr A B is-contr-A = ```agda is-equiv-inr-join-unit : - {l : Level} (X : UU l) → is-equiv (inr-join X unit) + {l : Level} (X : UU l) → is-equiv (inr-join {A = X} {B = unit}) is-equiv-inr-join-unit X = is-equiv-universal-property-pushout ( pr1) ( pr2) - ( cocone-join X unit) + ( cocone-join) ( is-equiv-map-right-unit-law-prod) - ( up-join X unit) + ( up-join) right-zero-law-join : {l : Level} (X : UU l) → is-contr (X * unit) right-zero-law-join X = is-contr-equiv' ( unit) - ( pair (inr-join X unit) (is-equiv-inr-join-unit X)) + ( inr-join , is-equiv-inr-join-unit X) ( is-contr-unit) is-equiv-inr-join-is-contr : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → is-contr B → is-equiv (inr-join A B) + {l1 l2 : Level} (A : UU l1) (B : UU l2) → + is-contr B → is-equiv (inr-join {A = A} {B = B}) is-equiv-inr-join-is-contr A B is-contr-B = is-equiv-universal-property-pushout ( pr1) ( pr2) - ( cocone-join A B) - ( is-equiv-pr1-is-contr λ a → is-contr-B) - ( up-join A B) + ( cocone-join) + ( is-equiv-pr1-is-contr (λ _ → is-contr-B)) + ( up-join) right-zero-law-join-is-contr : {l1 l2 : Level} (A : UU l1) (B : UU l2) → is-contr B → is-contr (A * B) right-zero-law-join-is-contr A B is-contr-B = is-contr-equiv' ( B) - ( pair (inr-join A B) (is-equiv-inr-join-is-contr A B is-contr-B)) + ( inr-join , is-equiv-inr-join-is-contr A B is-contr-B) ( is-contr-B) ``` @@ -247,7 +264,7 @@ module _ is-proof-irrelevant A → is-proof-irrelevant B → is-proof-irrelevant (A * B) is-proof-irrelevant-join-is-proof-irrelevant is-proof-irrelevant-A is-proof-irrelevant-B = - cogap-join A B (is-contr (A * B)) + cogap-join (is-contr (A * B)) ( pair ( left-zero-law-join-is-contr A B ∘ is-proof-irrelevant-A) ( pair @@ -266,12 +283,13 @@ module _ ( is-proof-irrelevant-is-prop is-prop-B)) module _ - {l1 l2 : Level} ((A , is-prop-A) : Prop l1) ((B , is-prop-B) : Prop l2) + {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) where join-Prop : Prop (l1 ⊔ l2) - pr1 join-Prop = A * B - pr2 join-Prop = is-prop-join-is-prop is-prop-A is-prop-B + pr1 join-Prop = (type-Prop P) * (type-Prop Q) + pr2 join-Prop = + is-prop-join-is-prop (is-prop-type-Prop P) (is-prop-type-Prop Q) type-join-Prop : UU (l1 ⊔ l2) type-join-Prop = type-Prop join-Prop @@ -279,11 +297,11 @@ module _ is-prop-type-join-Prop : is-prop type-join-Prop is-prop-type-join-Prop = is-prop-type-Prop join-Prop - inl-join-Prop : type-hom-Prop (A , is-prop-A) join-Prop - inl-join-Prop = inl-join A B + inl-join-Prop : type-hom-Prop P join-Prop + inl-join-Prop = inl-join - inr-join-Prop : type-hom-Prop (B , is-prop-B) join-Prop - inr-join-Prop = inr-join A B + inr-join-Prop : type-hom-Prop Q join-Prop + inr-join-Prop = inr-join ``` ### Disjunction is the join of propositions @@ -304,13 +322,13 @@ module _ map-disj-join-Prop : type-join-Prop A B → type-disj-Prop A B map-disj-join-Prop = - cogap-join (type-Prop A) (type-Prop B) (type-disj-Prop A B) cocone-disj + cogap-join (type-disj-Prop A B) cocone-disj map-join-disj-Prop : type-disj-Prop A B → type-join-Prop A B map-join-disj-Prop = elim-disj-Prop A B ( join-Prop A B) - ( pair (inl-join-Prop A B) (inr-join-Prop A B)) + ( inl-join-Prop A B , inr-join-Prop A B) is-equiv-map-disj-join-Prop : is-equiv map-disj-join-Prop is-equiv-map-disj-join-Prop = @@ -339,24 +357,21 @@ module _ up-pushout-up-pushout-is-equiv ( pr1) ( pr2) - ( cocone-join (pr1 A) (pr1 B)) + ( cocone-join) ( cocone-disj) ( map-disj-join-Prop) - ( pair - ( λ _ → eq-is-prop (is-prop-type-disj-Prop A B)) - ( pair - ( λ _ → eq-is-prop (is-prop-type-disj-Prop A B)) - ( λ (a , b) → - eq-is-contr - ( is-prop-type-disj-Prop A B - ( horizontal-map-cocone pr1 pr2 - ( cocone-map pr1 pr2 - ( cocone-join (pr1 A) (pr1 B)) - ( map-disj-join-Prop)) - ( a)) - ( vertical-map-cocone pr1 pr2 cocone-disj b))))) + ( ( λ _ → eq-is-prop (is-prop-type-disj-Prop A B)) , + ( λ _ → eq-is-prop (is-prop-type-disj-Prop A B)) , + ( λ (a , b) → eq-is-contr + ( is-prop-type-disj-Prop A B + ( horizontal-map-cocone pr1 pr2 + ( cocone-map pr1 pr2 + ( cocone-join) + ( map-disj-join-Prop)) + ( a)) + ( vertical-map-cocone pr1 pr2 cocone-disj b)))) ( is-equiv-map-disj-join-Prop) - ( up-join (pr1 A) (pr1 B)) + ( up-join) ``` ## See also diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index 8a5f156df1..2011ccbfb4 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -102,7 +102,7 @@ postulate postulate glue-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} - (f : S → A) (g : S → B) → ((inl-pushout f g) ∘ f) ~ ((inr-pushout f g) ∘ g) + (f : S → A) (g : S → B) → inl-pushout f g ∘ f ~ inr-pushout f g ∘ g cocone-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}