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.
UniMath · Nov 24, 2023 · f9d879c · f9d879c
1 parent 4bfc70a
commit f9d879c
Show file tree

Hide file tree

Showing 55 changed files with 3,330 additions and 518 deletions.
diff --git 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
@@ -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)).
 
+<!--
 - **Double quoted strings**: Replaces double quoted strings with single quoted
   strings.
+-->
 
 - **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.
 
+<!--
 - **Python scripts formatting**: Performs `autopep8` formatting on Python
   scripts. Note that this script takes care of most formatting for Python
   scripts, so you should not worry about formatting them.
+-->
 
 - **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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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