Basic properties of the flat modality (#1078)

This is the replacement of #1005.

Proves a series of basic properties of the flat modality.

## Summary

### General properties

- [X] The universal property of flat discrete crisp types
- [x] ~The dependent universal property of flat discrete crisp types~
- [X] Functoriality of flat
- [X] Flat is idempotent
- [x] A crisp type is crisply flat discrete if its counit has a crisp
section

### Left exactness of flat

- [X] Flat distributes over identity types
- [X] The crisp identity types of flat discrete crisp types are flat
discrete
- [X] Flat distributes over dependent pair types
- [X] Flat distributes over product types
- [x] Flat distributes over pullbacks
- [x] ~Flat distributes over sequential limits~
- [x] The unit type is flat discrete

### Right exactness of flat

- [X] The empty type is flat discrete
- [X] The natural numbers are flat discrete
- [X] Flat distributes over coproduct types
- [x] ~Flat distributes over pushouts~
- [x] ~Flat distributes over coequalizers~
- [x] ~Flat distributes over sequential colimits~

### Notes
- The constructor for the flat modality is renamed from `cons-flat` to
`intro-flat`. This makes it easier to distinguish from `counit-flat`.
- In the future, we will probably want to prove `crisp-based-ind-Id`
from the existence of the sharp modality rather than postulating it. The
same is true for the modal induction principle of the sharp modality.
- This PR does some ground work with the sharp modality too.

references.bib

@@ -146,6 +146,13 @@ @article{CR21
   keywords    = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory}
 }
 
+@online{DavidJaz/Cohesion,
+  title        = {DavidJaz/Cohesion},
+  author       = {David Jaz Meyers},
+  url          = {https://github.com/DavidJaz/Cohesion},
+  howpublished = {{{GitHub}} repository}
+}
+
 @article{dJE23,
   title       = {{On Small Types in Univalent Foundations}},
   author      = {de Jong, Tom and Escardó, Martín Hötzel},
@@ -409,6 +416,16 @@ @book{MRR88
   isbn        = {978-0-387-96640-3 978-1-4419-8640-5}
 }
 
+@misc{Mye21,
+  title         = {Modal Fracture of Higher Groups},
+  author        = {David Jaz Myers},
+  year          = {2021},
+  eprint        = {2106.15390},
+  archiveprefix = {arXiv},
+  eprintclass   = {math},
+  primaryclass  = {math.CT}
+}
+
 @online{OEIS,
   title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}} ({{OEIS}})},
   organization = {{{OEIS}} Foundation Inc.},

src/modal-type-theory.lagda.md

@@ -9,14 +9,27 @@
 ```agda
 module modal-type-theory where
 
+open import modal-type-theory.action-on-homotopies-flat-modality public
+open import modal-type-theory.action-on-identifications-crisp-functions public
+open import modal-type-theory.action-on-identifications-flat-modality public
+open import modal-type-theory.crisp-cartesian-product-types public
+open import modal-type-theory.crisp-coproduct-types public
+open import modal-type-theory.crisp-dependent-function-types public
+open import modal-type-theory.crisp-dependent-pair-types public
+open import modal-type-theory.crisp-function-types public
 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.crisp-pullbacks public
+open import modal-type-theory.crisp-types public
+open import modal-type-theory.dependent-universal-property-flat-discrete-crisp-types public
+open import modal-type-theory.flat-discrete-crisp-types public
 open import modal-type-theory.flat-modality public
 open import modal-type-theory.flat-sharp-adjunction public
+open import modal-type-theory.functoriality-flat-modality public
+open import modal-type-theory.functoriality-sharp-modality 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
+open import modal-type-theory.transport-along-crisp-identifications public
+open import modal-type-theory.universal-property-flat-discrete-crisp-types public
 ```

src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md

@@ -0,0 +1,70 @@
+# The action on homotopies of the flat modality
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.action-on-homotopies-flat-modality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-identifications-flat-modality
+open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-flat-modality
+```
+
+</details>
+
+## Idea
+
+Given a crisp [homotopy](foundation-core.homotopies.md) of maps `f ~ g`, then
+there is a homotopy `♭ f ~ ♭ g` where `♭ f` is the
+[functorial action of the flat modality on maps](modal-type-theory.functoriality-flat-modality.md).
+
+## Definitions
+
+### The flat modality's action on crisp homotopies
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
+  {@♭ f g : (@♭ x : A) → B x}
+  where
+
+  action-flat-crisp-htpy :
+    @♭ ((@♭ x : A) → f x ＝ g x) →
+    action-flat-crisp-dependent-map f ~ action-flat-crisp-dependent-map g
+  action-flat-crisp-htpy H (intro-flat x) = ap-flat (H x)
+```
+
+### The flat modality's action on homotopies
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2}
+  {@♭ f g : (x : A) → B x}
+  where
+
+  action-flat-htpy :
+    @♭ f ~ g → action-flat-dependent-map f ~ action-flat-dependent-map g
+  action-flat-htpy H = action-flat-crisp-htpy (λ x → H x)
+```
+
+## Properties
+
+### Computing the flat action on the reflexivity homotopy
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2} {@♭ f : (@♭ x : A) → B x}
+  where
+
+  compute-action-flat-refl-htpy :
+    action-flat-crisp-htpy (λ x → (refl {x = f x})) ~ refl-htpy
+  compute-action-flat-refl-htpy (intro-flat x) = refl
+```

src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md

@@ -0,0 +1,139 @@
+# The action on identifications of crisp functions
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.action-on-identifications-crisp-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+
+open import modal-type-theory.crisp-identity-types
+```
+
+</details>
+
+## Idea
+
+A function defined on [crisp elements](modal-type-theory.crisp-types.md)
+`f : @♭ A → B` preserves crisp
+[identifications](foundation-core.identity-types.md), in the sense that it maps
+a crisp identification `p : x ＝ y` in `A` to an identification
+`crisp-ap f p : f x ＝ f y` in `B`. This action on identifications can be
+understood as crisp functoriality of crisp identity types.
+
+This is a strengthening of the
+[action on identifications of functions](foundation.action-on-identifications-functions.md)
+for crisp identifications, because the function `f : A → B` is allowed to be
+defined over only crisp elements of its domain.
+
+## Definition
+
+### The functorial action of functions on crisp identity types
+
+```agda
+crisp-ap :
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {B : UU l2} (f : @♭ A → B)
+  {@♭ x y : A} → @♭ (x ＝ y) → f x ＝ f y
+crisp-ap f refl = refl
+```
+
+## Properties
+
+### The identity function acts trivially on identifications
+
+```agda
+crisp-ap-id :
+  {@♭ l : Level} {@♭ A : UU l} {@♭ x y : A} (@♭ p : x ＝ y) →
+  crisp-ap (λ x → x) p ＝ p
+crisp-ap-id p = crisp-based-ind-Id (λ y p → crisp-ap (λ x → x) p ＝ p) refl p
+```
+
+### The action on identifications of a composite function is the composite of the actions
+
+```agda
+crisp-ap-comp :
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ C : UU l3}
+  (@♭ g : @♭ B → C) (@♭ f : @♭ A → B) {@♭ x y : A} (@♭ p : x ＝ y) →
+  crisp-ap (λ x → g (f x)) p ＝ crisp-ap g (crisp-ap f p)
+crisp-ap-comp g f {x} =
+  crisp-based-ind-Id
+    ( λ y p → crisp-ap (λ x → g (f x)) p ＝ crisp-ap g (crisp-ap f p))
+    ( refl)
+
+crisp-ap-comp-assoc :
+  {@♭ l1 l2 l3 l4 : Level}
+  {@♭ A : UU l1} {@♭ B : UU l2} {@♭ C : UU l3} {@♭ D : UU l4}
+  (@♭ h : @♭ C → D) (@♭ g : B → C) (@♭ f : @♭ A → B)
+  {@♭ x y : A} (@♭ p : x ＝ y) →
+  crisp-ap (λ z → h (g z)) (crisp-ap f p) ＝
+  crisp-ap h (crisp-ap (λ z → g (f z)) p)
+crisp-ap-comp-assoc h g f =
+  crisp-based-ind-Id
+    ( λ y p →
+      crisp-ap (λ z → h (g z)) (crisp-ap f p) ＝
+      crisp-ap h (crisp-ap (λ z → g (f z)) p))
+    ( refl)
+```
+
+### The action on identifications of any map preserves `refl`
+
+```agda
+crisp-ap-refl :
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {B : UU l2}
+  (f : @♭ A → B) (@♭ x : A) →
+  crisp-ap f (refl {x = x}) ＝ refl
+crisp-ap-refl f x = refl
+```
+
+### The action on identifications of any map preserves concatenation of identifications
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} (@♭ f : @♭ A → B)
+  where
+
+  crisp-ap-concat :
+    {@♭ x y z : A} (@♭ p : x ＝ y) (@♭ q : y ＝ z) →
+    crisp-ap f (p ∙ q) ＝ crisp-ap f p ∙ crisp-ap f q
+  crisp-ap-concat p =
+    crisp-based-ind-Id
+      ( λ z q → crisp-ap f (p ∙ q) ＝ crisp-ap f p ∙ crisp-ap f q)
+      (crisp-ap (crisp-ap f) right-unit ∙ inv right-unit)
+
+  crisp-compute-right-refl-ap-concat :
+    {@♭ x y : A} (@♭ p : x ＝ y) →
+    crisp-ap-concat p refl ＝ crisp-ap (crisp-ap f) right-unit ∙ inv right-unit
+  crisp-compute-right-refl-ap-concat p =
+    compute-crisp-based-ind-Id
+      ( λ z q → crisp-ap f (p ∙ q) ＝ crisp-ap f p ∙ crisp-ap f q)
+      (crisp-ap (crisp-ap f) right-unit ∙ inv right-unit)
+```
+
+### The action on identifications of any map preserves inverses
+
+```agda
+crisp-ap-inv :
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  (@♭ f : @♭ A → B) {@♭ x y : A} (@♭ p : x ＝ y) →
+  crisp-ap f (inv p) ＝ inv (crisp-ap f p)
+crisp-ap-inv f =
+  crisp-based-ind-Id
+    ( λ y p → crisp-ap f (inv p) ＝ inv (crisp-ap f p))
+    ( refl)
+```
+
+### The action on identifications of a constant map is constant
+
+```agda
+crisp-ap-const :
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} (@♭ b : B) {@♭ x y : A}
+  (@♭ p : x ＝ y) → crisp-ap (λ _ → b) p ＝ refl
+crisp-ap-const b =
+  crisp-based-ind-Id (λ y p → crisp-ap (λ _ → b) p ＝ refl) (refl)
+```

src/modal-type-theory/action-on-identifications-flat-modality.lagda.md

@@ -0,0 +1,99 @@
+# The action on identifications of the flat modality
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.action-on-identifications-flat-modality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-identifications-crisp-functions
+open import modal-type-theory.crisp-identity-types
+open import modal-type-theory.flat-modality
+```
+
+</details>
+
+## Idea
+
+Given a crisp [identification](foundation-core.identity-types.md) `x ＝ y` in
+`A`, then there is an identification `intro-flat x ＝ intro-flat y` in `♭ A`.
+
+## Definitions
+
+### The action on identifications of the flat modality
+
+```agda
+module _
+  {@♭ l1 : Level} {@♭ A : UU l1} {@♭ x y : A}
+  where
+
+  ap-flat : @♭ x ＝ y → intro-flat x ＝ intro-flat y
+  ap-flat = crisp-ap intro-flat
+```
+
+## Properties
+
+### Computing the flat modality's action on reflexivity
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l} {@♭ x : A}
+  where
+
+  compute-refl-ap-flat : ap-flat (refl {x = x}) ＝ refl
+  compute-refl-ap-flat = refl
+```
+
+### The action on identifications of the flat modality is a crisp section of the action on identifications of its counit
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  where
+
+  is-crisp-section-ap-flat :
+    {@♭ x y : A} (@♭ p : x ＝ y) → ap (counit-flat) (ap-flat p) ＝ p
+  is-crisp-section-ap-flat =
+    crisp-based-ind-Id
+      ( λ y p → ap (counit-flat) (ap-flat p) ＝ p)
+      ( refl)
+```
+
+### The action on identifications of the flat modality from {{#cite Shu18}}
+
+**Note.** While we record the constructions from Corollary 6.3 {{#cite Shu18}}
+here, the construction of `ap-flat` is preferred elsewhere.
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  where
+
+  ap-flat' :
+    {@♭ x y : A} → @♭ (x ＝ y) → intro-flat x ＝ intro-flat y
+  ap-flat' {x} {y} p =
+    eq-Eq-flat (intro-flat x) (intro-flat y) (intro-flat p)
+
+  compute-refl-ap-flat' :
+    {@♭ x : A} → ap-flat' (refl {x = x}) ＝ refl
+  compute-refl-ap-flat' = refl
+
+  is-crisp-section-ap-flat' :
+    {@♭ x y : A} (@♭ p : x ＝ y) → ap (counit-flat) (ap-flat' p) ＝ p
+  is-crisp-section-ap-flat' =
+    crisp-based-ind-Id
+      ( λ y p → ap (counit-flat) (ap-flat' p) ＝ p)
+      ( refl)
+
+  compute-ap-flat' :
+    {@♭ x y : A} (@♭ p : x ＝ y) → ap-flat p ＝ ap-flat' p
+  compute-ap-flat' =
+    crisp-based-ind-Id (λ y p → ap-flat p ＝ ap-flat' p) refl
+```