From 4264b327f83a4a00c19c771d7dd37a3a9e87a7f4 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 6 Sep 2024 18:23:35 +0200
Subject: [PATCH] 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                                |  17 +
 src/modal-type-theory.lagda.md                |  19 +-
 ...ction-on-homotopies-flat-modality.lagda.md |  70 ++++
 ...n-identifications-crisp-functions.lagda.md | 139 ++++++++
 ...-on-identifications-flat-modality.lagda.md |  99 ++++++
 .../crisp-cartesian-product-types.lagda.md    | 183 ++++++++++
 .../crisp-coproduct-types.lagda.md            | 162 +++++++++
 .../crisp-dependent-function-types.lagda.md   | 141 ++++++++
 .../crisp-dependent-pair-types.lagda.md       | 146 ++++++++
 .../crisp-function-types.lagda.md             | 127 +++++++
 .../crisp-identity-types.lagda.md             | 161 ++++++++-
 .../crisp-law-of-excluded-middle.lagda.md     |   9 +-
 .../crisp-pullbacks.lagda.md                  | 185 ++++++++++
 src/modal-type-theory/crisp-types.lagda.md    |  75 ++++
 ...roperty-flat-discrete-crisp-types.lagda.md |  62 ++++
 .../flat-dependent-function-types.lagda.md    |  56 ---
 .../flat-dependent-pair-types.lagda.md        |  90 -----
 .../flat-discrete-crisp-types.lagda.md        | 329 ++++++++++++++++++
 .../flat-discrete-types.lagda.md              | 100 ------
 src/modal-type-theory/flat-modality.lagda.md  | 147 ++++----
 .../flat-sharp-adjunction.lagda.md            | 256 ++++----------
 .../functoriality-flat-modality.lagda.md      | 187 ++++++++++
 .../functoriality-sharp-modality.lagda.md     |  59 ++++
 .../sharp-codiscrete-maps.lagda.md            |  22 +-
 .../sharp-codiscrete-types.lagda.md           | 204 ++++++++---
 src/modal-type-theory/sharp-modality.lagda.md | 260 ++++++++++++--
 ...sport-along-crisp-identifications.lagda.md | 169 +++++++++
 ...roperty-flat-discrete-crisp-types.lagda.md | 102 ++++++
 28 files changed, 2963 insertions(+), 613 deletions(-)
 create mode 100644 src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md
 create mode 100644 src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md
 create mode 100644 src/modal-type-theory/action-on-identifications-flat-modality.lagda.md
 create mode 100644 src/modal-type-theory/crisp-cartesian-product-types.lagda.md
 create mode 100644 src/modal-type-theory/crisp-coproduct-types.lagda.md
 create mode 100644 src/modal-type-theory/crisp-dependent-function-types.lagda.md
 create mode 100644 src/modal-type-theory/crisp-dependent-pair-types.lagda.md
 create mode 100644 src/modal-type-theory/crisp-function-types.lagda.md
 create mode 100644 src/modal-type-theory/crisp-pullbacks.lagda.md
 create mode 100644 src/modal-type-theory/crisp-types.lagda.md
 create mode 100644 src/modal-type-theory/dependent-universal-property-flat-discrete-crisp-types.lagda.md
 delete mode 100644 src/modal-type-theory/flat-dependent-function-types.lagda.md
 delete mode 100644 src/modal-type-theory/flat-dependent-pair-types.lagda.md
 create mode 100644 src/modal-type-theory/flat-discrete-crisp-types.lagda.md
 delete mode 100644 src/modal-type-theory/flat-discrete-types.lagda.md
 create mode 100644 src/modal-type-theory/functoriality-flat-modality.lagda.md
 create mode 100644 src/modal-type-theory/functoriality-sharp-modality.lagda.md
 create mode 100644 src/modal-type-theory/transport-along-crisp-identifications.lagda.md
 create mode 100644 src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md

diff --git a/references.bib b/references.bib
index 7d87266a6f..723dd550cc 100644
--- a/references.bib
+++ b/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.},
diff --git a/src/modal-type-theory.lagda.md b/src/modal-type-theory.lagda.md
index 073d022d0e..872f769c29 100644
--- a/src/modal-type-theory.lagda.md
+++ b/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
 ```
diff --git a/src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md b/src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md
new file mode 100644
index 0000000000..028fdaeee2
--- /dev/null
+++ b/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
+```
diff --git a/src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md b/src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md
new file mode 100644
index 0000000000..5b28c70c99
--- /dev/null
+++ b/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)
+```
diff --git a/src/modal-type-theory/action-on-identifications-flat-modality.lagda.md b/src/modal-type-theory/action-on-identifications-flat-modality.lagda.md
new file mode 100644
index 0000000000..a573dcddf1
--- /dev/null
+++ b/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
+```
diff --git a/src/modal-type-theory/crisp-cartesian-product-types.lagda.md b/src/modal-type-theory/crisp-cartesian-product-types.lagda.md
new file mode 100644
index 0000000000..000d78c746
--- /dev/null
+++ b/src/modal-type-theory/crisp-cartesian-product-types.lagda.md
@@ -0,0 +1,183 @@
+# Crisp cartesian product types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.crisp-cartesian-product-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositional-truncations
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+
+open import modal-type-theory.flat-discrete-crisp-types
+open import modal-type-theory.flat-modality
+```
+
+</details>
+
+## Idea
+
+We say a [cartesian product type](foundation-core.cartesian-product-types.md) is
+{{#concept "crisp" Disambiguation="cartesian product type"}} if it is formed in
+a [crisp context](modal-type-theory.crisp-types.md).
+
+## Properties
+
+### Flat distributes over cartesian product types
+
+This is Theorem 6.9 of {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  map-distributive-flat-product : ♭ (A × B) → ♭ A × ♭ B
+  pr1 (map-distributive-flat-product (intro-flat (x , y))) = intro-flat x
+  pr2 (map-distributive-flat-product (intro-flat (x , y))) = intro-flat y
+
+  map-inv-distributive-flat-product : ♭ A × ♭ B → ♭ (A × B)
+  map-inv-distributive-flat-product (intro-flat x , intro-flat y) =
+    intro-flat (x , y)
+
+  is-section-map-distributive-flat-product :
+    is-section map-inv-distributive-flat-product map-distributive-flat-product
+  is-section-map-distributive-flat-product (intro-flat x) = refl
+
+  is-retraction-map-distributive-flat-product :
+    is-retraction
+      ( map-inv-distributive-flat-product)
+      ( map-distributive-flat-product)
+  is-retraction-map-distributive-flat-product (intro-flat x , intro-flat y) =
+    refl
+
+  section-distributive-flat-product : section map-distributive-flat-product
+  pr1 section-distributive-flat-product = map-inv-distributive-flat-product
+  pr2 section-distributive-flat-product =
+    is-retraction-map-distributive-flat-product
+
+  retraction-distributive-flat-product :
+    retraction map-distributive-flat-product
+  pr1 retraction-distributive-flat-product = map-inv-distributive-flat-product
+  pr2 retraction-distributive-flat-product =
+    is-section-map-distributive-flat-product
+
+  is-equiv-map-distributive-flat-product :
+    is-equiv map-distributive-flat-product
+  pr1 is-equiv-map-distributive-flat-product = section-distributive-flat-product
+  pr2 is-equiv-map-distributive-flat-product =
+    retraction-distributive-flat-product
+
+  distributive-flat-product : ♭ (A × B) ≃ ♭ A × ♭ B
+  pr1 distributive-flat-product = map-distributive-flat-product
+  pr2 distributive-flat-product = is-equiv-map-distributive-flat-product
+
+  inv-distributive-flat-product : ♭ A × ♭ B ≃ ♭ (A × B)
+  inv-distributive-flat-product = inv-equiv distributive-flat-product
+```
+
+### Computing the flat counit on a cartesian product type
+
+The counit of the flat modality computes as the counit on each component of a
+crisp dependent pair type.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  compute-counit-flat-product :
+    counit-flat {A = A × B} ~
+    ( map-product counit-flat counit-flat ∘ map-distributive-flat-product)
+  compute-counit-flat-product (intro-flat x) = refl
+```
+
+### Flat discrete crisp types are closed under cartesian products
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  is-flat-discrete-crisp-product :
+    is-flat-discrete-crisp A →
+    is-flat-discrete-crisp B →
+    is-flat-discrete-crisp (A × B)
+  is-flat-discrete-crisp-product is-disc-A is-disc-B =
+    is-equiv-left-map-triangle
+      ( counit-flat)
+      ( map-product counit-flat counit-flat)
+      ( map-distributive-flat-product)
+      ( λ where (intro-flat _) → refl)
+      ( is-equiv-map-distributive-flat-product)
+      ( is-equiv-map-product counit-flat counit-flat is-disc-A is-disc-B)
+```
+
+### A factor is a flat discrete crisp type if the cartesian product is a flat discrete crisp type and the other factor is inhabited
+
+```agda
+  is-flat-discrete-crisp-right-factor-product' :
+    is-flat-discrete-crisp (A × B) → A → is-flat-discrete-crisp B
+  is-flat-discrete-crisp-right-factor-product'
+    is-disc-product-A-B x =
+    is-equiv-right-factor-is-equiv-map-product'
+      ( counit-flat)
+      ( counit-flat)
+      ( x)
+      ( is-equiv-right-map-triangle
+        counit-flat
+        ( map-product counit-flat counit-flat)
+        ( map-distributive-flat-product)
+        ( λ where (intro-flat _) → refl)
+        ( is-disc-product-A-B)
+        ( is-equiv-map-distributive-flat-product))
+
+  is-flat-discrete-crisp-right-factor-product :
+    is-flat-discrete-crisp (A × B) → is-inhabited A → is-flat-discrete-crisp B
+  is-flat-discrete-crisp-right-factor-product
+    is-disc-product-A-B =
+    rec-trunc-Prop
+      ( is-flat-discrete-crisp-Prop B)
+      ( is-flat-discrete-crisp-right-factor-product' is-disc-product-A-B)
+
+  is-flat-discrete-crisp-left-factor-product' :
+    is-flat-discrete-crisp (A × B) → B → is-flat-discrete-crisp A
+  is-flat-discrete-crisp-left-factor-product'
+    is-disc-product-A-B x =
+    is-equiv-left-factor-is-equiv-map-product'
+      ( counit-flat)
+      ( counit-flat)
+      ( x)
+      ( is-equiv-right-map-triangle
+        counit-flat
+        ( map-product counit-flat counit-flat)
+        ( map-distributive-flat-product)
+        ( λ where (intro-flat _) → refl)
+        ( is-disc-product-A-B)
+        ( is-equiv-map-distributive-flat-product))
+
+  is-flat-discrete-crisp-left-factor-product :
+    is-flat-discrete-crisp (A × B) → is-inhabited B → is-flat-discrete-crisp A
+  is-flat-discrete-crisp-left-factor-product
+    is-disc-product-A-B =
+    rec-trunc-Prop
+      ( is-flat-discrete-crisp-Prop A)
+      ( is-flat-discrete-crisp-left-factor-product' is-disc-product-A-B)
+```
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/crisp-coproduct-types.lagda.md b/src/modal-type-theory/crisp-coproduct-types.lagda.md
new file mode 100644
index 0000000000..1fc84587d7
--- /dev/null
+++ b/src/modal-type-theory/crisp-coproduct-types.lagda.md
@@ -0,0 +1,162 @@
+# Crisp coproduct types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.crisp-coproduct-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-coproduct-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-discrete-crisp-types
+open import modal-type-theory.flat-modality
+```
+
+</details>
+
+## Idea
+
+We say a [coproduct type](foundation-core.coproduct-types.md) is
+{{#concept "crisp" Disambiguation="coproduct type"}} if it is formed in a
+[crisp context](modal-type-theory.crisp-types.md).
+
+## Definitions
+
+### Crisp case analysis
+
+This is Theorem 5.4 of {{#cite Shu18}}, although the proof is much simpler.
+
+```agda
+crisp-ind-coproduct :
+  {@♭ l1 l2 l3 : Level}
+  {@♭ A : UU l1} {@♭ B : UU l2} {@♭ C : @♭ A + B → UU l3} →
+  @♭ ((@♭ x : A) → C (inl x)) →
+  @♭ ((@♭ y : B) → C (inr y)) →
+  ((@♭ u : A + B) → C u)
+crisp-ind-coproduct f g (inl x) = f x
+crisp-ind-coproduct f g (inr y) = g y
+
+crisp-rec-coproduct :
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ C : UU l3} →
+  @♭ ((@♭ x : A) → C) →
+  @♭ ((@♭ y : B) → C) →
+  (@♭ (A + B) → C)
+crisp-rec-coproduct = crisp-ind-coproduct
+```
+
+## Properties
+
+### Flat distributes over coproduct types
+
+This is Corollary 5.5 of {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  map-distributive-flat-coproduct : ♭ (A + B) → ♭ A + ♭ B
+  map-distributive-flat-coproduct (intro-flat (inl x)) = inl (intro-flat x)
+  map-distributive-flat-coproduct (intro-flat (inr x)) = inr (intro-flat x)
+
+  map-inv-distributive-flat-coproduct : ♭ A + ♭ B → ♭ (A + B)
+  map-inv-distributive-flat-coproduct (inl (intro-flat x)) = intro-flat (inl x)
+  map-inv-distributive-flat-coproduct (inr (intro-flat x)) = intro-flat (inr x)
+
+  is-section-map-distributive-flat-coproduct :
+    is-section
+      ( map-inv-distributive-flat-coproduct)
+      ( map-distributive-flat-coproduct)
+  is-section-map-distributive-flat-coproduct (intro-flat (inl x)) = refl
+  is-section-map-distributive-flat-coproduct (intro-flat (inr x)) = refl
+
+  is-retraction-map-distributive-flat-coproduct :
+    is-retraction
+      ( map-inv-distributive-flat-coproduct)
+      ( map-distributive-flat-coproduct)
+  is-retraction-map-distributive-flat-coproduct (inl (intro-flat x)) = refl
+  is-retraction-map-distributive-flat-coproduct (inr (intro-flat x)) = refl
+
+  section-distributive-flat-coproduct : section map-distributive-flat-coproduct
+  pr1 section-distributive-flat-coproduct = map-inv-distributive-flat-coproduct
+  pr2 section-distributive-flat-coproduct =
+    is-retraction-map-distributive-flat-coproduct
+
+  retraction-distributive-flat-coproduct :
+    retraction map-distributive-flat-coproduct
+  pr1 retraction-distributive-flat-coproduct =
+    map-inv-distributive-flat-coproduct
+  pr2 retraction-distributive-flat-coproduct =
+    is-section-map-distributive-flat-coproduct
+
+  is-equiv-map-distributive-flat-coproduct :
+    is-equiv map-distributive-flat-coproduct
+  pr1 is-equiv-map-distributive-flat-coproduct =
+    section-distributive-flat-coproduct
+  pr2 is-equiv-map-distributive-flat-coproduct =
+    retraction-distributive-flat-coproduct
+
+  distributive-flat-coproduct : ♭ (A + B) ≃ ♭ A + ♭ B
+  pr1 distributive-flat-coproduct = map-distributive-flat-coproduct
+  pr2 distributive-flat-coproduct = is-equiv-map-distributive-flat-coproduct
+
+  inv-distributive-flat-coproduct : ♭ A + ♭ B ≃ ♭ (A + B)
+  inv-distributive-flat-coproduct = inv-equiv distributive-flat-coproduct
+```
+
+### Computing the flat counit on a coproduct type
+
+The counit of the flat modality computes as the counit on each component of a
+crisp dependent pair type.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  compute-counit-flat-coproduct :
+    counit-flat {A = A + B} ~
+    map-coproduct counit-flat counit-flat ∘ map-distributive-flat-coproduct
+  compute-counit-flat-coproduct (intro-flat (inl x)) = refl
+  compute-counit-flat-coproduct (intro-flat (inr x)) = refl
+```
+
+### A crisp coproduct type is flat discrete if both summands are
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  abstract
+    is-flat-discrete-crisp-coproduct :
+      is-flat-discrete-crisp A →
+      is-flat-discrete-crisp B →
+      is-flat-discrete-crisp (A + B)
+    is-flat-discrete-crisp-coproduct is-disc-A is-disc-B =
+      is-equiv-left-map-triangle
+        ( counit-flat)
+        ( map-coproduct counit-flat counit-flat)
+        ( map-distributive-flat-coproduct)
+        ( λ where
+          (intro-flat (inl x)) → refl
+          (intro-flat (inr x)) → refl)
+        ( is-equiv-map-distributive-flat-coproduct)
+        ( is-equiv-map-coproduct is-disc-A is-disc-B)
+```
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/crisp-dependent-function-types.lagda.md b/src/modal-type-theory/crisp-dependent-function-types.lagda.md
new file mode 100644
index 0000000000..a5034fb664
--- /dev/null
+++ b/src/modal-type-theory/crisp-dependent-function-types.lagda.md
@@ -0,0 +1,141 @@
+# Crisp dependent function types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.crisp-dependent-function-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.sections
+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
+
+We say a [dependent function type](foundation.dependent-function-types.md) is
+{{#concept "crisp" Disambiguation="dependent function type"}} if it is formed in
+a [crisp context](modal-type-theory.crisp-types.md).
+
+A dependent function `f` from `A` to `B` may be assumed to be a
+{{#concept "crisp dependent function" Disambiguation="of crisp types"}} given
+that its domain and codomain are crisp. By this we mean it is a crisp element of
+its type, written `@♭ f : (x : A) → B x`. We may also assume that a dependent
+function is
+{{#concept "defined on crisp elements" Disambiguation="dependent function on a crisp type"}}
+if its definition assumes that the elements of its domain are crisp, written
+`f : (@♭ x : A) → B x`. Being crisp, and being defined on crisp elements are
+independent properties. A dependent function may be crisp and defined on
+cohesive elements, and it may be cohesive but defined on crisp elements. Indeed,
+all configurations are possible when both `A` and `B` are crisp:
+
+|                              | Crisp dependent function | Cohesive dependent function |
+| ---------------------------: | -----------------------: | --------------------------: |
+|    Defined on crisp elements |  `@♭ ((@♭ x : A) → B x)` |          `(@♭ x : A) → B x` |
+| Defined on cohesive elements |     `@♭ ((x : A) → B x)` |             `(x : A) → B x` |
+
+Note, since assuming that a hypothesis is crisp is _less_ general, assuming that
+a hypothesis assumes that a hypothesis is crisp is _more_ general. Hence
+assuming the dependent function is cohesive and defined on crisp elements
+`f : (@♭ x : A) → B x` is the _weakest_ assumption one can make given that `A`
+is crisp, while assuming the dependent function is crisp and defined on cohesive
+elements `@♭ f : (x : A) → B x` is the strongest, given that `B` is also crisp.
+
+## Properties
+
+### Flat distributes in one direction over dependent function types
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
+  where
+
+  map-distributive-flat-crisp-Π : ♭ ((@♭ x : A) → B x) → ((@♭ x : A) → ♭ (B x))
+  map-distributive-flat-crisp-Π (intro-flat f) x = intro-flat (f x)
+
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2}
+  where
+
+  map-distributive-flat-Π :
+    ♭ ((x : A) → B x) → ((x : ♭ A) → action-flat-family B x)
+  map-distributive-flat-Π (intro-flat f) (intro-flat x) = intro-flat (f x)
+```
+
+### Postcomposition by the flat counit induces an equivalence under the flat modality on dependent function types
+
+This is Theorem 6.14 in {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
+  where
+
+  map-action-flat-dependent-map-postcomp-counit-flat :
+    ♭ ((u : ♭ A) → action-flat-crisp-family B u) →
+    ♭ ((u : ♭ A) → family-over-flat B u)
+  map-action-flat-dependent-map-postcomp-counit-flat (intro-flat f) =
+    intro-flat (λ where (intro-flat x) → counit-flat (f (intro-flat x)))
+
+  map-inv-action-flat-dependent-map-postcomp-counit-flat :
+    ♭ ((u : ♭ A) → family-over-flat B u) →
+    ♭ ((u : ♭ A) → action-flat-crisp-family B u)
+  map-inv-action-flat-dependent-map-postcomp-counit-flat (intro-flat f) =
+    intro-flat (λ where (intro-flat y) → intro-flat (f (intro-flat y)))
+
+  is-section-map-inv-action-flat-dependent-map-postcomp-counit-flat :
+    is-section
+      ( map-action-flat-dependent-map-postcomp-counit-flat)
+      ( map-inv-action-flat-dependent-map-postcomp-counit-flat)
+  is-section-map-inv-action-flat-dependent-map-postcomp-counit-flat
+    (intro-flat f) =
+    ap-flat (eq-htpy (λ where (intro-flat x) → refl))
+
+  is-retraction-map-inv-action-flat-dependent-map-postcomp-counit-flat :
+    is-retraction
+      ( map-action-flat-dependent-map-postcomp-counit-flat)
+      ( map-inv-action-flat-dependent-map-postcomp-counit-flat)
+  is-retraction-map-inv-action-flat-dependent-map-postcomp-counit-flat
+    (intro-flat f) =
+    ap-flat
+      ( eq-htpy
+        ( λ where
+          (intro-flat x) → is-crisp-retraction-intro-flat (f (intro-flat x))))
+
+  is-equiv-action-flat-depdendent-map-postcomp-counit-flat :
+    is-equiv map-action-flat-dependent-map-postcomp-counit-flat
+  is-equiv-action-flat-depdendent-map-postcomp-counit-flat =
+    is-equiv-is-invertible
+      ( map-inv-action-flat-dependent-map-postcomp-counit-flat)
+      ( is-section-map-inv-action-flat-dependent-map-postcomp-counit-flat)
+      ( is-retraction-map-inv-action-flat-dependent-map-postcomp-counit-flat)
+
+  equiv-action-flat-depdendent-map-postcomp-counit-flat :
+    ♭ ((u : ♭ A) → action-flat-crisp-family B u) ≃
+    ♭ ((u : ♭ A) → family-over-flat B u)
+  equiv-action-flat-depdendent-map-postcomp-counit-flat =
+    ( map-action-flat-dependent-map-postcomp-counit-flat ,
+      is-equiv-action-flat-depdendent-map-postcomp-counit-flat)
+```
+
+## See also
+
+- [Flat discrete crisp types](modal-type-theory.flat-discrete-crisp-types.md)
+  for crisp types that are flat modal.
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/crisp-dependent-pair-types.lagda.md b/src/modal-type-theory/crisp-dependent-pair-types.lagda.md
new file mode 100644
index 0000000000..69ac59e250
--- /dev/null
+++ b/src/modal-type-theory/crisp-dependent-pair-types.lagda.md
@@ -0,0 +1,146 @@
+# Crisp dependent pair types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.crisp-dependent-pair-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-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-discrete-crisp-types
+open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-flat-modality
+```
+
+</details>
+
+## Idea
+
+We say a [dependent pair type](foundation.dependent-pair-types.md) is
+{{#concept "crisp" Disambiguation="dependent pair type"}} if it is formed in a
+[crisp context](modal-type-theory.crisp-types.md). Here, we study the
+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) (action-flat-crisp-family B)
+```
+
+## Properties
+
+### Flat distributes over Σ-types
+
+This is Lemma 6.8 of {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2}
+  where
+
+  map-distributive-flat-Σ : ♭ (Σ A B) → Σ-♭ A (λ x → B x)
+  pr1 (map-distributive-flat-Σ (intro-flat (x , y))) = intro-flat x
+  pr2 (map-distributive-flat-Σ (intro-flat (x , y))) = intro-flat y
+
+  map-inv-distributive-flat-Σ : Σ-♭ A (λ x → B x) → ♭ (Σ A B)
+  map-inv-distributive-flat-Σ (intro-flat x , intro-flat y) = intro-flat (x , y)
+
+  is-section-map-distributive-flat-Σ :
+    is-section map-inv-distributive-flat-Σ map-distributive-flat-Σ
+  is-section-map-distributive-flat-Σ (intro-flat _) = refl
+
+  is-retraction-map-distributive-flat-Σ :
+    is-retraction map-inv-distributive-flat-Σ map-distributive-flat-Σ
+  is-retraction-map-distributive-flat-Σ (intro-flat _ , intro-flat _) = refl
+
+  section-distributive-flat-Σ : section map-distributive-flat-Σ
+  pr1 section-distributive-flat-Σ = map-inv-distributive-flat-Σ
+  pr2 section-distributive-flat-Σ = is-retraction-map-distributive-flat-Σ
+
+  retraction-distributive-flat-Σ : retraction map-distributive-flat-Σ
+  pr1 retraction-distributive-flat-Σ = map-inv-distributive-flat-Σ
+  pr2 retraction-distributive-flat-Σ = is-section-map-distributive-flat-Σ
+
+  is-equiv-map-distributive-flat-Σ : is-equiv map-distributive-flat-Σ
+  pr1 is-equiv-map-distributive-flat-Σ = section-distributive-flat-Σ
+  pr2 is-equiv-map-distributive-flat-Σ = retraction-distributive-flat-Σ
+
+  distributive-flat-Σ : ♭ (Σ A B) ≃ Σ-♭ A (λ x → B x)
+  pr1 distributive-flat-Σ = map-distributive-flat-Σ
+  pr2 distributive-flat-Σ = is-equiv-map-distributive-flat-Σ
+
+  inv-distributive-flat-Σ : Σ-♭ A (λ x → B x) ≃ ♭ (Σ A B)
+  inv-distributive-flat-Σ = inv-equiv distributive-flat-Σ
+```
+
+### Computing the flat counit on a dependent pair type
+
+The counit of the flat modality computes as the counit on each component of a
+crisp dependent pair type.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2}
+  where
+
+  compute-counit-flat-Σ :
+    counit-flat {A = Σ A B} ~
+    ( map-Σ B counit-flat (λ where (intro-flat _) → counit-flat)) ∘
+    ( map-distributive-flat-Σ)
+  compute-counit-flat-Σ (intro-flat _) = refl
+```
+
+### A crisp dependent pair type over a flat discrete type is flat discrete if and only if the family is flat discrete
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2}
+  (is-disc-A : is-flat-discrete-crisp A)
+  where
+
+  is-flat-discrete-crisp-Σ :
+    is-flat-discrete-crisp-family (λ x → B x) → is-flat-discrete-crisp (Σ A B)
+  is-flat-discrete-crisp-Σ is-disc-B =
+    is-equiv-left-map-triangle
+      ( counit-flat)
+      ( map-Σ B counit-flat (λ where (intro-flat _) → counit-flat))
+      ( map-distributive-flat-Σ)
+      ( λ where (intro-flat _) → refl)
+      ( is-equiv-map-distributive-flat-Σ)
+      ( is-equiv-map-Σ B is-disc-A (λ where (intro-flat x) → is-disc-B x))
+
+  is-flat-discrete-crisp-family-is-flat-discrete-crisp-Σ :
+    is-flat-discrete-crisp (Σ A B) → is-flat-discrete-crisp-family (λ x → B x)
+  is-flat-discrete-crisp-family-is-flat-discrete-crisp-Σ is-disc-Σ-B x =
+    is-fiberwise-equiv-is-equiv-map-Σ
+      ( B)
+      ( counit-flat)
+      ( λ where (intro-flat _) → counit-flat)
+      ( is-disc-A)
+      ( is-equiv-right-map-triangle
+        ( counit-flat)
+        ( _)
+        ( map-distributive-flat-Σ)
+        ( λ where (intro-flat _) → refl)
+        ( is-disc-Σ-B)
+        ( is-equiv-map-distributive-flat-Σ))
+      ( intro-flat x)
+```
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/crisp-function-types.lagda.md b/src/modal-type-theory/crisp-function-types.lagda.md
new file mode 100644
index 0000000000..57b0ed3e46
--- /dev/null
+++ b/src/modal-type-theory/crisp-function-types.lagda.md
@@ -0,0 +1,127 @@
+# Crisp function types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.crisp-function-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.identity-types
+open import foundation.postcomposition-functions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-identifications-flat-modality
+open import modal-type-theory.crisp-dependent-function-types
+open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-flat-modality
+```
+
+</details>
+
+## Idea
+
+We say a [function type](foundation-core.function-types.md) is
+{{#concept "crisp" Disambiguation="function type"}} if it is formed in a
+[crisp context](modal-type-theory.crisp-types.md).
+
+A function `f` from `A` to `B` may be assumed to be a
+{{#concept "crisp function" Disambiguation="of crisp types"}} given that its
+domain and codomain are crisp. By this we mean it is a crisp element of its
+type, written `@♭ f : A → B`. We may also assume that a function is
+{{#concept "defined on crisp elements" Disambiguation="function on a crisp type"}}
+if its definition assumes that the elements of its domain are crisp, written
+`f : @♭ A → B`. Being crisp, and being defined on crisp elements are independent
+properties. A function may be crisp and defined on cohesive elements, and it may
+be cohesive but defined on crisp elements. Indeed, all configurations are
+possible when both `A` and `B` are crisp:
+
+|                              |  Crisp function | Cohesive function |
+| ---------------------------: | --------------: | ----------------: |
+|    Defined on crisp elements | `@♭ (@♭ A → B)` |        `@♭ A → B` |
+| Defined on cohesive elements |    `@♭ (A → B)` |           `A → B` |
+
+Note, since assuming that a hypothesis is crisp is _less_ general, assuming that
+a hypothesis assumes that a hypothesis is crisp is _more_ general. Hence
+assuming the function is cohesive and defined on crisp elements `f : @♭ A → B`
+is the _weakest_ assumption one can make given that `A` is crisp, while assuming
+it is crisp and defined on cohesive elements `@♭ f : A → B` is the strongest,
+given that `B` is also crisp.
+
+## Properties
+
+### Flat distributes in one direction over function types
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  map-distributive-flat-crisp-function-types : ♭ (@♭ A → B) → (@♭ A → ♭ B)
+  map-distributive-flat-crisp-function-types = map-distributive-flat-crisp-Π
+
+  map-distributive-flat-function-types : ♭ (A → B) → (♭ A → ♭ B)
+  map-distributive-flat-function-types f (intro-flat x) =
+    map-distributive-flat-Π f (intro-flat x)
+```
+
+### Postcomposition by the flat counit induces an equivalence `♭ (♭ A → ♭ B) ≃ ♭ (♭ A → B)`
+
+This is Theorem 6.14 in {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  map-inv-action-flat-map-postcomp-counit-flat : ♭ (♭ A → B) → ♭ (♭ A → ♭ B)
+  map-inv-action-flat-map-postcomp-counit-flat (intro-flat f) =
+    intro-flat (λ where (intro-flat y) → intro-flat (f (intro-flat y)))
+
+  is-section-map-inv-action-flat-map-postcomp-counit-flat :
+    is-section
+      ( action-flat-map (postcomp (♭ A) counit-flat))
+      ( map-inv-action-flat-map-postcomp-counit-flat)
+  is-section-map-inv-action-flat-map-postcomp-counit-flat (intro-flat f) =
+    ap-flat (eq-htpy (λ where (intro-flat _) → refl))
+
+  is-retraction-map-inv-action-flat-map-postcomp-counit-flat :
+    is-retraction
+      ( action-flat-map (postcomp (♭ A) counit-flat))
+      ( map-inv-action-flat-map-postcomp-counit-flat)
+  is-retraction-map-inv-action-flat-map-postcomp-counit-flat (intro-flat f) =
+    ap-flat
+      ( eq-htpy
+        ( λ where
+          (intro-flat x) → is-crisp-retraction-intro-flat (f (intro-flat x))))
+
+  is-equiv-action-flat-map-postcomp-counit-flat :
+    is-equiv (action-flat-map (postcomp (♭ A) (counit-flat {A = B})))
+  is-equiv-action-flat-map-postcomp-counit-flat =
+    is-equiv-is-invertible
+      ( map-inv-action-flat-map-postcomp-counit-flat)
+      ( is-section-map-inv-action-flat-map-postcomp-counit-flat)
+      ( is-retraction-map-inv-action-flat-map-postcomp-counit-flat)
+
+  equiv-action-flat-map-postcomp-counit-flat : ♭ (♭ A → ♭ B) ≃ ♭ (♭ A → B)
+  pr1 equiv-action-flat-map-postcomp-counit-flat =
+    action-flat-map (postcomp (♭ A) counit-flat)
+  pr2 equiv-action-flat-map-postcomp-counit-flat =
+    is-equiv-action-flat-map-postcomp-counit-flat
+```
+
+## See also
+
+- [Flat discrete crisp types](modal-type-theory.flat-discrete-crisp-types.md)
+  for crisp types that are flat modal.
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/crisp-identity-types.lagda.md b/src/modal-type-theory/crisp-identity-types.lagda.md
index 87b191d9dc..adffea8d96 100644
--- a/src/modal-type-theory/crisp-identity-types.lagda.md
+++ b/src/modal-type-theory/crisp-identity-types.lagda.md
@@ -9,8 +9,16 @@ module modal-type-theory.crisp-identity-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.retractions
+open import foundation.retracts-of-types
+open import foundation.sections
 open import foundation.universe-levels
+
+open import modal-type-theory.flat-modality
 ```
 
 </details>
@@ -18,20 +26,155 @@ open import foundation.universe-levels
 ## Idea
 
 We record here some basic facts about
-[identity types](foundation-core.identity-types.md) in crisp contexts.
+[identity types](foundation-core.identity-types.md) in
+[crisp contexts](modal-type-theory.crisp-types.md).
 
-## Properties
+## Definitions
+
+### Weak crisp identification induction
 
 ```agda
-ind-path-crisp :
+weak-crisp-based-ind-Id :
   {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {@♭ a : A} →
-  (C : (@♭ y : A) (p : a ＝ y) → UU l2) →
+  (C : (@♭ y : A) → (a ＝ y) → UU l2) →
   C a refl →
   (@♭ y : A) (@♭ p : a ＝ y) → C y p
-ind-path-crisp C b _ refl = b
+weak-crisp-based-ind-Id C b _ refl = b
+```
+
+### Based crisp identification induction
+
+Below we postulate the
+{{#concept "crisp identity induction principle" Agda=crisp-based-ind-Id}} as
+introduced in {{#cite Shu18}}. Note that this principle should follow from the
+flat modality's relation to the
+[sharp modality](modal-type-theory.sharp-modality.md), and the stronger
+`pointwise-sharp` construction as considered in {{#cite DavidJaz/Cohesion}}.
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ x : A}
+  (@♭ C : (@♭ y : A) → @♭ (x ＝ y) → UU l2)
+  (@♭ d : (C x refl))
+  where
+
+  postulate
+    crisp-based-ind-Id : {@♭ y : A} (@♭ p : x ＝ y) → C y p
+    compute-crisp-based-ind-Id : crisp-based-ind-Id {x} refl ＝ d
+```
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1}
+  (@♭ C : (@♭ x y : A) → @♭ (x ＝ y) → UU l2)
+  (@♭ d : ((@♭ x : A) → C x x refl))
+  where
+
+  crisp-ind-Id : {@♭ x y : A} (@♭ p : x ＝ y) → C x y p
+  crisp-ind-Id {x} {y} p = crisp-based-ind-Id (λ y p → C x y p) (d x) {y} p
+
+  compute-crisp-ind-Id : (@♭ x : A) → crisp-ind-Id {x} refl ＝ d x
+  compute-crisp-ind-Id x = compute-crisp-based-ind-Id (λ y p → C x y p) (d x)
+```
+
+## Properties
+
+### Characterizing equality in the image of the flat modality
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  where
+
+  Eq-flat : ♭ A → ♭ A → UU l
+  Eq-flat (intro-flat x) (intro-flat y) = ♭ (x ＝ y)
+
+  refl-Eq-flat : (u : ♭ A) → Eq-flat u u
+  refl-Eq-flat (intro-flat x) = intro-flat refl
+
+  Eq-eq-flat : (u v : ♭ A) → u ＝ v → Eq-flat u v
+  Eq-eq-flat u .u refl = refl-Eq-flat u
+
+  eq-Eq-flat : (u v : ♭ A) → Eq-flat u v → u ＝ v
+  eq-Eq-flat (intro-flat x) (intro-flat .x) (intro-flat refl) = refl
+```
+
+The retraction part is easy:
+
+```agda
+  is-retraction-eq-Eq-flat :
+    (u v : ♭ A) → is-retraction (Eq-eq-flat u v) (eq-Eq-flat u v)
+  is-retraction-eq-Eq-flat (intro-flat x) (intro-flat .x) refl = refl
+
+  retraction-Eq-eq-flat : (u v : ♭ A) → retraction (Eq-eq-flat u v)
+  pr1 (retraction-Eq-eq-flat u v) = eq-Eq-flat u v
+  pr2 (retraction-Eq-eq-flat u v) = is-retraction-eq-Eq-flat u v
+
+  retract-Eq-flat :
+    (u v : ♭ A) → (u ＝ v) retract-of (Eq-flat u v)
+  pr1 (retract-Eq-flat u v) = Eq-eq-flat u v
+  pr1 (pr2 (retract-Eq-flat u v)) = eq-Eq-flat u v
+  pr2 (pr2 (retract-Eq-flat u v)) = is-retraction-eq-Eq-flat u v
+
+  is-injective-Eq-eq-flat :
+    (u v : ♭ A) → is-injective (Eq-eq-flat u v)
+  is-injective-Eq-eq-flat u v =
+    is-injective-retraction (Eq-eq-flat u v) (retraction-Eq-eq-flat u v)
+```
+
+To show it is also a section, however, we need the stronger crisp identity
+induction principle, which we have only postulated so far.
+
+```agda
+  is-section-eq-Eq-flat :
+    (u v : ♭ A) → is-section (Eq-eq-flat u v) (eq-Eq-flat u v)
+  is-section-eq-Eq-flat (intro-flat x) (intro-flat y) (intro-flat p) =
+    crisp-ind-Id
+      ( λ x y p →
+        ( Eq-eq-flat
+          ( intro-flat x)
+          ( intro-flat y)
+          ( eq-Eq-flat (intro-flat x) (intro-flat y) (intro-flat p))) ＝
+        ( intro-flat p))
+      ( λ _ → refl)
+      ( p)
+```
 
-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
+```agda
+  is-equiv-Eq-eq-flat : (u v : ♭ A) → is-equiv (Eq-eq-flat u v)
+  is-equiv-Eq-eq-flat u v =
+    is-equiv-is-invertible
+      ( eq-Eq-flat u v)
+      ( is-section-eq-Eq-flat u v)
+      ( is-retraction-eq-Eq-flat u v)
+
+  extensionality-flat : (u v : ♭ A) → (u ＝ v) ≃ Eq-flat u v
+  pr1 (extensionality-flat u v) = Eq-eq-flat u v
+  pr2 (extensionality-flat u v) = is-equiv-Eq-eq-flat u v
+```
+
+The following is Theorem 6.1 in {{#cite Shu18}}.
+
+```agda
+  crisp-extensionality-flat :
+    (@♭ x y : A) → (intro-flat x ＝ intro-flat y) ≃ ♭ (x ＝ y)
+  crisp-extensionality-flat x y =
+    extensionality-flat (intro-flat x) (intro-flat y)
 ```
+
+The following is Corollary 6.2 in {{#cite Shu18}}.
+
+```agda
+  crisp-flat-extensionality-flat :
+    (@♭ u v : ♭ A) → (u ＝ v) ≃ ♭ (counit-flat u ＝ counit-flat v)
+  crisp-flat-extensionality-flat (intro-flat x) (intro-flat y) =
+    extensionality-flat (intro-flat x) (intro-flat y)
+```
+
+## See also
+
+- We show that identity types between crisp elements of flat discrete crisp
+  types are flat discrete crisp in
+  [`modal-type-theory.flat-discrete-crisp-types`](modal-type-theory.flat-discrete-crisp-types.md).
+- [Action on identifications of crisp functions](modal-type-theory.action-on-identifications-crisp-functions.md)
+- [Transport along crisp identifications](modal-type-theory.transport-along-crisp-identifications.md)
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
index 6770f4d7f0..a5a795e2f0 100644
--- a/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md
+++ b/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md
@@ -14,7 +14,6 @@ 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
 ```
 
@@ -22,8 +21,8 @@ open import foundation-core.propositions
 
 ## Idea
 
-The **crisp law of excluded middle** asserts that any crisp
-[proposition](foundation-core.propositions.md) `P` is
+The {{#concept "crisp law of excluded middle" Agda=Crisp-LEM}} asserts that any
+crisp [proposition](foundation-core.propositions.md) `P` is
 [decidable](foundation.decidable-types.md).
 
 ## Definition
@@ -48,3 +47,7 @@ pr2 (pr2 (decidable-prop-Crisp-Prop lem P)) = lem P
 ## See also
 
 - [The law of excluded middle](foundation.law-of-excluded-middle.md)
+
+## References
+
+{{#bibliography}} {{#reference Shu18}}
diff --git a/src/modal-type-theory/crisp-pullbacks.lagda.md b/src/modal-type-theory/crisp-pullbacks.lagda.md
new file mode 100644
index 0000000000..0ba9b014f2
--- /dev/null
+++ b/src/modal-type-theory/crisp-pullbacks.lagda.md
@@ -0,0 +1,185 @@
+# Crisp pullbacks
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.crisp-pullbacks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-pullbacks
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-cospan-diagrams
+open import foundation.pullbacks
+open import foundation.standard-pullbacks
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-identifications-crisp-functions
+open import modal-type-theory.action-on-identifications-flat-modality
+open import modal-type-theory.crisp-dependent-pair-types
+open import modal-type-theory.crisp-identity-types
+open import modal-type-theory.flat-discrete-crisp-types
+open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-flat-modality
+```
+
+</details>
+
+## Idea
+
+We say a [pullback](foundation-core.pullbacks.md) is
+{{#concept "crisp" Disambiguation="pullback"}} if it is formed in a
+[crisp context](modal-type-theory.crisp-types.md).
+
+**Comment.** The results in this file should hold more generally for
+[crisp maps defined on crisp elements](modal-type-theory.crisp-function-types.md)
+`@♭ f : @♭ A → X` and `@♭ g : @♭ B → X`.
+
+## Properties
+
+### Flat distributes over standard pullbacks
+
+```agda
+module _
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3}
+  (@♭ f : A → X) (@♭ g : B → X)
+  where
+
+  map-distributive-flat-standard-pullback :
+    ♭ (standard-pullback f g) →
+    standard-pullback (action-flat-map f) (action-flat-map g)
+  map-distributive-flat-standard-pullback (intro-flat (x , y , p)) =
+    ( intro-flat x , intro-flat y , ap-flat p)
+
+  map-inv-distributive-flat-standard-pullback :
+    @♭ standard-pullback (action-flat-map f) (action-flat-map g) →
+    ♭ (standard-pullback f g)
+  map-inv-distributive-flat-standard-pullback
+    (intro-flat x , intro-flat y , p) =
+    intro-flat (x , y , ap counit-flat p)
+
+  is-crisp-section-map-distributive-flat-standard-pullback :
+    (@♭ x : ♭ (standard-pullback f g)) →
+    map-inv-distributive-flat-standard-pullback
+      ( map-distributive-flat-standard-pullback x) ＝
+    ( x)
+  is-crisp-section-map-distributive-flat-standard-pullback
+    ( intro-flat (x , y , p)) =
+    crisp-ap
+      ( intro-flat)
+      ( eq-pair-eq-fiber
+        ( eq-pair-eq-fiber
+          ( is-crisp-section-ap-flat p)))
+
+  is-crisp-retraction-map-distributive-flat-standard-pullback :
+    (@♭ x : standard-pullback (action-flat-map f) (action-flat-map g)) →
+    map-distributive-flat-standard-pullback
+      ( map-inv-distributive-flat-standard-pullback x) ＝
+    ( x)
+  is-crisp-retraction-map-distributive-flat-standard-pullback
+    ( intro-flat x , intro-flat y , p) =
+      eq-pair-eq-fiber
+        ( eq-pair-eq-fiber
+          ( crisp-based-ind-Id
+            ( λ where
+              (intro-flat y) p → crisp-ap intro-flat (ap counit-flat p) ＝ p)
+            ( refl)
+            ( p)))
+```
+
+### Computing the flat counit on a standard pullback
+
+The counit of the flat modality computes as the counit on each component of a
+crisp dependent pair type.
+
+```agda
+module _
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3}
+  (@♭ f : A → X) (@♭ g : B → X)
+  where
+
+  counit-flat-hom-cospan-diagram :
+    hom-cospan-diagram (action-flat-map f) (action-flat-map g) f g
+  counit-flat-hom-cospan-diagram =
+    ( counit-flat ,
+      counit-flat ,
+      counit-flat ,
+      inv-htpy (naturality-counit-flat f) ,
+      inv-htpy (naturality-counit-flat g))
+
+  compute-counit-flat-standard-pullback :
+    ( map-standard-pullback
+      ( f)
+      ( g)
+      ( action-flat-map f)
+      ( action-flat-map g)
+      ( counit-flat-hom-cospan-diagram)) ∘
+    ( map-distributive-flat-standard-pullback f g) ~
+    counit-flat {A = standard-pullback f g}
+  compute-counit-flat-standard-pullback (intro-flat (x , y , p)) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( right-unit ∙ is-crisp-section-ap-flat p))
+```
+
+### A crisp standard pullback is flat discrete if its factors are
+
+```agda
+module _
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3}
+  (@♭ f : A → X) (@♭ g : B → X)
+  where
+
+  is-flat-discrete-crisp-standard-pullback-is-flat-discrete-crisp-factors :
+    is-flat-discrete-crisp X →
+    is-flat-discrete-crisp A →
+    is-flat-discrete-crisp B →
+    is-flat-discrete-crisp (standard-pullback f g)
+  is-flat-discrete-crisp-standard-pullback-is-flat-discrete-crisp-factors
+    bX bA bB =
+    is-flat-discrete-crisp-Σ
+      ( bA)
+      ( λ a →
+        is-flat-discrete-crisp-Σ
+        ( bB)
+        ( λ b → is-flat-discrete-crisp-Id (is-emb-is-equiv bX)))
+```
+
+### A crisp pullback is flat discrete if its factors are
+
+```agda
+module _
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3}
+  (@♭ f : A → X) (@♭ g : B → X)
+  where
+
+  is-flat-discrete-crisp-pullback-is-flat-discrete-crisp-factors :
+    {@♭ l4 : Level} {@♭ C : UU l4} (@♭ c : cone f g C) →
+    @♭ is-pullback f g c →
+    is-flat-discrete-crisp X →
+    is-flat-discrete-crisp A →
+    is-flat-discrete-crisp B →
+    is-flat-discrete-crisp C
+  is-flat-discrete-crisp-pullback-is-flat-discrete-crisp-factors c H bX bA bB =
+    is-flat-discrete-crisp-equiv'
+      ( gap f g c , H)
+      ( is-flat-discrete-crisp-standard-pullback-is-flat-discrete-crisp-factors
+        ( f)
+        ( g)
+        ( bX)
+        ( bA)
+        ( bB))
+```
+
+## References
+
+{{#bibliography}} {{#reference Shu18}}
diff --git a/src/modal-type-theory/crisp-types.lagda.md b/src/modal-type-theory/crisp-types.lagda.md
new file mode 100644
index 0000000000..fc0a210f20
--- /dev/null
+++ b/src/modal-type-theory/crisp-types.lagda.md
@@ -0,0 +1,75 @@
+# Crisp types
+
+```agda
+module modal-type-theory.crisp-types where
+```
+
+## Idea
+
+In cohesive type theory, and more generally spatial type theory, one endows
+types with an additional structure of cohesion, as modeled by
+[cohesive topoi](https://ncatlab.org/nlab/show/cohesive+topos) and
+[local topoi](https://ncatlab.org/nlab/show/local+geometric+morphism#LocalTopos)
+respectively. Examples include endowing types with real topological structure
+{{#cite Shu18}} and endowing types with symmetric simplicial structure
+{{#cite Mye21}}.
+
+One starts by introducing two modes of hypotheses: _cohesive_ and _crisp_. A
+{{#concept "cohesive" Disambiguation="hypothesis"}} hypothesis is the standard
+mode of hypothesis. In formalizations in the agda-unimath library made outside
+of this module, every hypothesis may be understood to be a cohesive hypothesis.
+These hypotheses come with the implicit assumption that their construction is
+respectful of the cohesive structure of the context. Cohesive hypotheses have no
+restrictions on the contexts in which they may be formed.
+
+{{#concept "Crisp" Disambiguation="hypothesis"}} hypotheses are, in contrast,
+hypotheses that are "indifferent" to the cohesive structure on types, and may
+only be judged in contexts made entirely out of crisp hypotheses, called _crisp
+contexts_. The indifference to cohesion is made concrete by the
+[flat](modal-type-theory.flat-modality.md) and
+[sharp](modal-type-theory.sharp-modality.md) modalities.
+
+For instance, in the framework of real-cohesive type theory, where every type is
+endowed with real topological structure, a cohesive variable is understood as
+one which varies _continuously_ with the real topology of its type. A crisp
+variable on the other hand, is one that may vary _discontinuously_ with respect
+to this topology.
+
+In Agda, we state that an assumption is crisp by prepending the symbol `@♭` to
+the hypothesis. For instance, to hypothesize two elements of an arbitrary type,
+one which is crisp and one which is cohesive, we may in a type signature write
+
+```text
+  (@♭ l : Level) (@♭ A : UU l) (@♭ x : A) (y : A).
+```
+
+Observe that for us to be able to assume `x` is crisp at all, we must also
+assume that the type `A` and the universe level `l` are crisp, following the
+rule that crisp hypotheses may only be formed in crisp contexts.
+
+So what does it mean for `A` to be a {{#concept "crisp type"}}? Since the
+universe of types is itself a type, and every type comes equipped with cohesive
+structure, it means that the definition of `A` is indifferent to the cohesive
+structure on the universe.
+
+Note that saying a type is crisp is very different to saying that the cohesive
+structure of the type is trivial, which one could in one way informally state as
+"it consists of only crisp elements". Crisp types whose cohesive structure is
+trivial in this sense is captured by
+[flat discrete crisp types](modal-type-theory.flat-discrete-crisp-types.md).
+
+## See also
+
+- [Crisp function types](modal-type-theory.crisp-function-types.md)
+- [The flat modality](modal-type-theory.flat-modality.md)
+
+## References
+
+{{#bibliography}}
+
+## External links
+
+- [Flat Modality](https://agda.readthedocs.io/en/latest/language/flat.html) on
+  the Agda documentation pages.
+- [spatial type theory](https://ncatlab.org/nlab/show/spatial+type+theory) at
+  $n$Lab.
diff --git a/src/modal-type-theory/dependent-universal-property-flat-discrete-crisp-types.lagda.md b/src/modal-type-theory/dependent-universal-property-flat-discrete-crisp-types.lagda.md
new file mode 100644
index 0000000000..1754d487ba
--- /dev/null
+++ b/src/modal-type-theory/dependent-universal-property-flat-discrete-crisp-types.lagda.md
@@ -0,0 +1,62 @@
+# Dependent universal property of flat discrete crisp types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.dependent-universal-property-flat-discrete-crisp-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.equivalences
+open import foundation.universe-levels
+
+open import modal-type-theory.flat-modality
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "dependent universal property" Disambiguation="of flat discrete crisp types"}}
+of a [flat discrete crisp type](modal-type-theory.flat-discrete-crisp-types.md)
+`A` states that for any [crisp](modal-type-theory.crisp-types.md) type family
+[defined on crisp elements](modal-type-theory.crisp-function-types.md)
+`@♭ B : @♭ A → 𝒰`,
+[postcomposition](foundation-core.postcomposition-functions.md) by the counit of
+the [flat modality](modal-type-theory.flat-modality.md) induces an
+[equivalence](foundation-core.equivalences.md) under the flat modality.
+
+## Definitions
+
+### The dependent universal property of flat discrete crisp types
+
+```agda
+dependent-coev-flat :
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2} →
+  ♭ ((@♭ x : A) → ♭ (B x)) → ♭ ((@♭ x : A) → B x)
+dependent-coev-flat (intro-flat f) = intro-flat (λ x → counit-flat (f x))
+```
+
+```text
+dependent-universal-property-flat-discrete-crisp-type :
+  {@♭ l1 : Level} (@♭ A : UU l1) → UUω
+dependent-universal-property-flat-discrete-crisp-type A =
+  {@♭ l : Level} {@♭ B : @♭ A → UU l} → is-equiv (dependent-coev-flat {B = B})
+```
+
+## Properties
+
+### Flat discrete crisp types satisfy the dependent universal property of flat discrete crisp types
+
+This remains to be formalized.
+
+## See also
+
+- [The universal property of flat discrete crisp types](modal-type-theory.universal-property-flat-discrete-crisp-types.md)
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-dependent-function-types.lagda.md b/src/modal-type-theory/flat-dependent-function-types.lagda.md
deleted file mode 100644
index 45cdb77663..0000000000
--- a/src/modal-type-theory/flat-dependent-function-types.lagda.md
+++ /dev/null
@@ -1,56 +0,0 @@
-# Flat dependent function types
-
-```agda
-{-# OPTIONS --cohesion --flat-split #-}
-
-module modal-type-theory.flat-dependent-function-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.universe-levels
-
-open import modal-type-theory.flat-modality
-```
-
-</details>
-
-## 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
-
-{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-dependent-pair-types.lagda.md b/src/modal-type-theory/flat-dependent-pair-types.lagda.md
deleted file mode 100644
index b59f618c57..0000000000
--- a/src/modal-type-theory/flat-dependent-pair-types.lagda.md
+++ /dev/null
@@ -1,90 +0,0 @@
-# Flat dependent pair types
-
-```agda
-{-# OPTIONS --cohesion --flat-split #-}
-
-module modal-type-theory.flat-dependent-pair-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.dependent-pair-types
-open import foundation.equivalences
-open import foundation.function-types
-open import foundation.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
-```
-
-</details>
-
-## 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
-
-{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-discrete-crisp-types.lagda.md b/src/modal-type-theory/flat-discrete-crisp-types.lagda.md
new file mode 100644
index 0000000000..0aa7b7204b
--- /dev/null
+++ b/src/modal-type-theory/flat-discrete-crisp-types.lagda.md
@@ -0,0 +1,329 @@
+# Flat discrete crisp types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.flat-discrete-crisp-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.booleans
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+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.retractions
+open import foundation.sections
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-homotopies-flat-modality
+open import modal-type-theory.crisp-identity-types
+open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-flat-modality
+```
+
+</details>
+
+## Idea
+
+A crisp type is said to be
+{{$concept "flat discrete" Disambiguation="crisp type" Agda=is-flat-discrete-crisp}}
+if it is [flat](modal-type-theory.flat-modality.md) modal. I.e. if the flat
+counit is an [equivalence](foundation-core.equivalences.md) at that type.
+
+**Terminology.** In {{#cite Shu18}} this is called a _crisply discrete type_. We
+add "flat" as a descriptor to disambiguate from other possible notions of
+"discrete types", such as
+[types with decidable equality `foundation.discrete-types`](foundation.discrete-types.md).
+Moreover, we prefer "discrete crisp type" over "crisply discrete type", as the
+former suggests that we assume that the type is crisp, and not that the proof
+that it is discrete itself is crisp.
+
+## Definitions
+
+### Flat discrete crisp types
+
+```agda
+module _
+  {@♭ l : Level} (@♭ A : UU l)
+  where
+
+  is-flat-discrete-crisp : UU l
+  is-flat-discrete-crisp = is-equiv (counit-flat {l} {A})
+
+  is-property-is-flat-discrete-crisp : is-prop is-flat-discrete-crisp
+  is-property-is-flat-discrete-crisp =
+    is-property-is-equiv (counit-flat {l} {A})
+
+  is-flat-discrete-crisp-Prop : Prop l
+  is-flat-discrete-crisp-Prop = is-equiv-Prop (counit-flat {l} {A})
+```
+
+### Flat discrete crisp type families
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1}
+  where
+
+  is-flat-discrete-crisp-family : (@♭ B : @♭ A → UU l2) → UU (l1 ⊔ l2)
+  is-flat-discrete-crisp-family B = (@♭ x : A) → is-flat-discrete-crisp (B x)
+```
+
+## Properties
+
+### If the flat counit has a crisp section then it is an equivalence
+
+This is Lemma 6.17 in {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l} (@♭ s : A → ♭ A) (@♭ H : counit-flat ∘ s ~ id)
+  where
+
+  htpy-retraction-counit-flat-has-crisp-section : s ∘ counit-flat ~ id
+  htpy-retraction-counit-flat-has-crisp-section (intro-flat x) =
+    inv (is-crisp-retraction-intro-flat (s x)) ∙
+    action-flat-htpy H (intro-flat x)
+
+  retraction-counit-flat-has-crisp-section : retraction (counit-flat {A = A})
+  retraction-counit-flat-has-crisp-section =
+    ( s , htpy-retraction-counit-flat-has-crisp-section)
+
+  is-flat-discrete-crisp-has-crisp-section : is-flat-discrete-crisp A
+  is-flat-discrete-crisp-has-crisp-section =
+    ( (s , H) , retraction-counit-flat-has-crisp-section)
+
+is-flat-discrete-crisp-crisp-section :
+  {@♭ l : Level} {@♭ A : UU l} →
+  @♭ section (counit-flat {A = A}) → is-flat-discrete-crisp A
+is-flat-discrete-crisp-crisp-section (s , H) =
+  is-flat-discrete-crisp-has-crisp-section s H
+```
+
+### Flat discrete crisp types are closed under equivalences
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  is-flat-discrete-crisp-equiv :
+    @♭ A ≃ B → is-flat-discrete-crisp A → is-flat-discrete-crisp B
+  is-flat-discrete-crisp-equiv e bB =
+    is-equiv-htpy-equiv'
+      ( e ∘e (counit-flat , bB) ∘e action-flat-equiv (inv-equiv e))
+      ( λ where (intro-flat x) → is-section-map-inv-equiv e x)
+
+  is-flat-discrete-crisp-equiv' :
+    @♭ A ≃ B → is-flat-discrete-crisp B → is-flat-discrete-crisp A
+  is-flat-discrete-crisp-equiv' e bB =
+    is-equiv-htpy-equiv'
+      ( inv-equiv e ∘e (counit-flat , bB) ∘e action-flat-equiv e)
+      ( λ where (intro-flat x) → is-retraction-map-inv-equiv e x)
+```
+
+### Types `♭ A` are flat discrete
+
+This is Theorem 6.18 of {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  where
+
+  is-flat-discrete-crisp-flat : is-flat-discrete-crisp (♭ A)
+  is-flat-discrete-crisp-flat = is-equiv-flat-counit-flat
+```
+
+### The crisp identity types of flat discrete crisp types are flat discrete
+
+Given crisp elements `x` and `y` of `A` We have a
+[commuting triangle](foundation-core.commuting-triangles-of-maps.md)
+
+```text
+                               ♭ (x ＝ y)
+                                  ∧   |
+                     Eq-eq-flat /~    |
+                              /       |
+  (intro-flat x ＝ intro-flat y)      | counit-flat
+                              \       |
+               ap (counit-flat) \     |
+                                  ∨   ∨
+                                 (x ＝ y)
+```
+
+where the top-left map `Eq-eq-flat` is an equivalence. Thus, the right map is an
+equivalence and `x ＝ y` is a flat discrete crisp type for all crisp `x` and `y`
+if and only if the flat counit of `A` is an
+[embedding](foundation-core.embeddings.md) on crisp elements. In particular, if
+`A` is a flat discrete crisp type then its crisp identity types are too.
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  ( is-crisp-emb-counit-flat-A :
+    (@♭ x y : A) → is-equiv (ap (counit-flat) {intro-flat x} {intro-flat y}))
+  {@♭ x y : A}
+  where
+
+  is-flat-discrete-crisp-Id' : is-flat-discrete-crisp (x ＝ y)
+  is-flat-discrete-crisp-Id' =
+    is-equiv-right-map-triangle
+      ( ap counit-flat {intro-flat x} {intro-flat y})
+      ( counit-flat)
+      ( Eq-eq-flat (intro-flat x) (intro-flat y))
+      ( λ where refl → refl)
+      ( is-crisp-emb-counit-flat-A x y)
+      ( is-equiv-Eq-eq-flat (intro-flat x) (intro-flat y))
+
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  (is-emb-counit-flat-A : is-emb (counit-flat {A = A}))
+  {@♭ x y : A}
+  where
+
+  is-flat-discrete-crisp-Id : is-flat-discrete-crisp (x ＝ y)
+  is-flat-discrete-crisp-Id =
+    is-flat-discrete-crisp-Id'
+      ( λ x y → is-emb-counit-flat-A (intro-flat x) (intro-flat y))
+
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  where
+
+  is-flat-discrete-crisp-flat-Id :
+    {@♭ u v : ♭ A} → is-flat-discrete-crisp (u ＝ v)
+  is-flat-discrete-crisp-flat-Id {intro-flat x} {intro-flat y} =
+    is-flat-discrete-crisp-Id (is-emb-is-equiv is-flat-discrete-crisp-flat)
+```
+
+### The empty type is flat discrete
+
+```agda
+map-is-flat-discrete-crisp-empty : empty → ♭ empty
+map-is-flat-discrete-crisp-empty ()
+
+is-section-map-is-flat-discrete-crisp-empty :
+  is-section counit-flat map-is-flat-discrete-crisp-empty
+is-section-map-is-flat-discrete-crisp-empty ()
+
+is-retraction-map-is-flat-discrete-crisp-empty :
+  is-retraction counit-flat map-is-flat-discrete-crisp-empty
+is-retraction-map-is-flat-discrete-crisp-empty (intro-flat ())
+
+abstract
+  is-flat-discrete-crisp-empty : is-flat-discrete-crisp empty
+  is-flat-discrete-crisp-empty =
+    is-equiv-is-invertible
+      ( map-is-flat-discrete-crisp-empty)
+      ( is-section-map-is-flat-discrete-crisp-empty)
+      ( is-retraction-map-is-flat-discrete-crisp-empty)
+```
+
+### The unit type is flat discrete
+
+```agda
+map-is-flat-discrete-crisp-unit : unit → ♭ unit
+map-is-flat-discrete-crisp-unit star = intro-flat star
+
+is-section-map-is-flat-discrete-crisp-unit :
+  is-section counit-flat map-is-flat-discrete-crisp-unit
+is-section-map-is-flat-discrete-crisp-unit _ = refl
+
+is-retraction-map-is-flat-discrete-crisp-unit :
+  is-retraction counit-flat map-is-flat-discrete-crisp-unit
+is-retraction-map-is-flat-discrete-crisp-unit (intro-flat _) = refl
+
+abstract
+  is-flat-discrete-crisp-unit : is-flat-discrete-crisp unit
+  is-flat-discrete-crisp-unit =
+    is-equiv-is-invertible
+      ( map-is-flat-discrete-crisp-unit)
+      ( is-section-map-is-flat-discrete-crisp-unit)
+      ( is-retraction-map-is-flat-discrete-crisp-unit)
+```
+
+### The type of booleans is flat discrete
+
+```agda
+map-is-flat-discrete-crisp-bool : bool → ♭ bool
+map-is-flat-discrete-crisp-bool true = intro-flat true
+map-is-flat-discrete-crisp-bool false = intro-flat false
+
+is-section-map-is-flat-discrete-crisp-bool :
+  is-section counit-flat map-is-flat-discrete-crisp-bool
+is-section-map-is-flat-discrete-crisp-bool true = refl
+is-section-map-is-flat-discrete-crisp-bool false = refl
+
+is-retraction-map-is-flat-discrete-crisp-bool :
+  is-retraction counit-flat map-is-flat-discrete-crisp-bool
+is-retraction-map-is-flat-discrete-crisp-bool (intro-flat true) = refl
+is-retraction-map-is-flat-discrete-crisp-bool (intro-flat false) = refl
+
+abstract
+  is-flat-discrete-crisp-bool : is-flat-discrete-crisp bool
+  is-flat-discrete-crisp-bool =
+    is-equiv-is-invertible
+      ( map-is-flat-discrete-crisp-bool)
+      ( is-section-map-is-flat-discrete-crisp-bool)
+      ( is-retraction-map-is-flat-discrete-crisp-bool)
+```
+
+### The type of natural numbers is flat discrete
+
+```agda
+map-is-flat-discrete-crisp-ℕ : ℕ → ♭ ℕ
+map-is-flat-discrete-crisp-ℕ zero-ℕ = intro-flat zero-ℕ
+map-is-flat-discrete-crisp-ℕ (succ-ℕ x) =
+  action-flat-map succ-ℕ (map-is-flat-discrete-crisp-ℕ x)
+
+compute-map-is-flat-discrete-crisp-ℕ :
+  (@♭ x : ℕ) → map-is-flat-discrete-crisp-ℕ x ＝ intro-flat x
+compute-map-is-flat-discrete-crisp-ℕ zero-ℕ =
+  refl
+compute-map-is-flat-discrete-crisp-ℕ (succ-ℕ x) =
+  ap (action-flat-map succ-ℕ) (compute-map-is-flat-discrete-crisp-ℕ x)
+
+is-section-map-is-flat-discrete-crisp-ℕ :
+  is-section counit-flat map-is-flat-discrete-crisp-ℕ
+is-section-map-is-flat-discrete-crisp-ℕ zero-ℕ =
+  refl
+is-section-map-is-flat-discrete-crisp-ℕ (succ-ℕ x) =
+  ( naturality-counit-flat succ-ℕ (map-is-flat-discrete-crisp-ℕ x)) ∙
+  ( ap succ-ℕ (is-section-map-is-flat-discrete-crisp-ℕ x))
+
+is-retraction-map-is-flat-discrete-crisp-ℕ :
+  is-retraction counit-flat map-is-flat-discrete-crisp-ℕ
+is-retraction-map-is-flat-discrete-crisp-ℕ (intro-flat x) =
+  compute-map-is-flat-discrete-crisp-ℕ x
+
+abstract
+  is-flat-discrete-crisp-ℕ : is-flat-discrete-crisp ℕ
+  is-flat-discrete-crisp-ℕ =
+    is-equiv-is-invertible
+      ( map-is-flat-discrete-crisp-ℕ)
+      ( is-section-map-is-flat-discrete-crisp-ℕ)
+      ( is-retraction-map-is-flat-discrete-crisp-ℕ)
+```
+
+## See also
+
+- [Sharp codiscrete types](modal-type-theory.sharp-codiscrete-types.md) for the
+  dual notion.
+- [The universal property of flat discrete crisp types](modal-type-theory.universal-property-flat-discrete-crisp-types.md)
+- [The dependent universal property of flat discrete crisp types](modal-type-theory.dependent-universal-property-flat-discrete-crisp-types.md)
+
+## References
+
+{{#bibliography}} {{#references Shu18}} {{#references Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/flat-discrete-types.lagda.md b/src/modal-type-theory/flat-discrete-types.lagda.md
deleted file mode 100644
index 1a8de9a979..0000000000
--- a/src/modal-type-theory/flat-discrete-types.lagda.md
+++ /dev/null
@@ -1,100 +0,0 @@
-# Flat discrete types
-
-```agda
-{-# OPTIONS --cohesion --flat-split #-}
-
-module modal-type-theory.flat-discrete-types where
-```
-
-<details><summary>Imports</summary>
-
-```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
-```
-
-</details>
-
-## 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
index 9ae682fecf..d3b1c42c08 100644
--- a/src/modal-type-theory/flat-modality.lagda.md
+++ b/src/modal-type-theory/flat-modality.lagda.md
@@ -11,8 +11,6 @@ module modal-type-theory.flat-modality where
 ```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
@@ -23,8 +21,8 @@ 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_.
+The {{#concept "flat modality" Agda=♭}} is an axiomatized comonadic modality we
+adjoin to our type theory by use of _crisp type theory_.
 
 ## Definition
 
@@ -32,17 +30,17 @@ theory by use of _crisp type theory_.
 
 ```agda
 data ♭ {@♭ l : Level} (@♭ A : UU l) : UU l where
-  cons-flat : @♭ A → ♭ A
+  intro-flat : @♭ A → ♭ A
+
+flat : {@♭ l : Level} (@♭ A : UU l) → UU l
+flat = ♭
 ```
 
 ### 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
+counit-flat (intro-flat x) = x
 ```
 
 ### Flat dependent elimination
@@ -50,62 +48,39 @@ counit-flat (cons-flat x) = counit-crisp x
 ```agda
 ind-flat :
   {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level} (C : ♭ A → UU l2) →
-  ((@♭ u : A) → C (cons-flat u)) →
+  ((@♭ u : A) → C (intro-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
+ind-flat C f (intro-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)
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {C : UU l2} →
+  (@♭ A → C) → ♭ A → C
+rec-flat {C = C} = ind-flat (λ _ → C)
 ```
 
-### Flat action on maps
+### Crispening statements
 
 ```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
+crispen :
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {P : A → UU l2} →
+  ((x : A) → P x) → ((@♭ x : A) → P x)
+crispen f x = f x
 ```
 
-## Properties
-
-### Crisp assumptions are weaker
+### The associated family over `♭ A` to a type family defined on crisp elements of `A`
 
 ```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
+family-over-flat :
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} (@♭ P : @♭ A → UU l2) → ♭ A → UU l2
+family-over-flat P (intro-flat x) = P x
 ```
 
+## Properties
+
 ### The flat modality is idempotent
 
 ```agda
@@ -113,50 +88,65 @@ 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-section-intro-flat : (@♭ x : A) → counit-flat (intro-flat x) ＝ x
+  is-crisp-section-intro-flat _ = refl
 
-  is-crisp-retraction-cons-flat : (@♭ x : ♭ A) → cons-flat (counit-flat x) ＝ x
-  is-crisp-retraction-cons-flat (cons-flat _) = refl
+  is-crisp-retraction-intro-flat : (@♭ x : ♭ A) → intro-flat (counit-flat x) ＝ x
+  is-crisp-retraction-intro-flat (intro-flat _) = refl
 ```
 
+#### The equivalence `♭ A ≃ ♭ (♭ A)`
+
 ```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)
+  diagonal-flat (intro-flat x) = intro-flat (intro-flat x)
+
+  is-retraction-diagonal-flat : is-retraction counit-flat diagonal-flat
+  is-retraction-diagonal-flat (intro-flat (intro-flat _)) = refl
+
+  is-section-diagonal-flat : is-section counit-flat diagonal-flat
+  is-section-diagonal-flat (intro-flat _) = refl
+
+  section-diagonal-flat : section diagonal-flat
+  pr1 section-diagonal-flat = counit-flat
+  pr2 section-diagonal-flat = is-retraction-diagonal-flat
 
-  is-section-flat-counit-flat :
-    diagonal-flat ∘ map-flat-counit-flat ~ id
-  is-section-flat-counit-flat (cons-flat (cons-flat _)) = refl
+  retraction-diagonal-flat : retraction diagonal-flat
+  pr1 retraction-diagonal-flat = counit-flat
+  pr2 retraction-diagonal-flat = is-section-diagonal-flat
 
-  is-retraction-flat-counit-flat :
-    map-flat-counit-flat ∘ diagonal-flat ~ id
-  is-retraction-flat-counit-flat (cons-flat _) = refl
+  abstract
+    is-equiv-diagonal-flat : is-equiv diagonal-flat
+    pr1 is-equiv-diagonal-flat = section-diagonal-flat
+    pr2 is-equiv-diagonal-flat = retraction-diagonal-flat
 
-  section-flat-counit-flat : section map-flat-counit-flat
+  equiv-diagonal-flat : ♭ A ≃ ♭ (♭ A)
+  pr1 equiv-diagonal-flat = diagonal-flat
+  pr2 equiv-diagonal-flat = is-equiv-diagonal-flat
+```
+
+#### The equivalence `♭ (♭ A) ≃ ♭ A`
+
+```agda
+  section-flat-counit-flat : section (counit-flat {A = ♭ A})
   pr1 section-flat-counit-flat = diagonal-flat
-  pr2 section-flat-counit-flat = is-retraction-flat-counit-flat
+  pr2 section-flat-counit-flat = is-section-diagonal-flat
 
-  retraction-flat-counit-flat : retraction map-flat-counit-flat
+  retraction-flat-counit-flat : retraction (counit-flat {A = ♭ A})
   pr1 retraction-flat-counit-flat = diagonal-flat
-  pr2 retraction-flat-counit-flat = is-section-flat-counit-flat
+  pr2 retraction-flat-counit-flat = is-retraction-diagonal-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
+  abstract
+    is-equiv-flat-counit-flat : is-equiv (counit-flat {A = ♭ A})
+    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
+  equiv-flat-counit-flat = inv-equiv equiv-diagonal-flat
 ```
 
 ## See also
@@ -164,9 +154,14 @@ module _
 - 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.
+- [Flat discrete crisp types](modal-type-theory.flat-discrete-crisp-types.md)
+  for crisp types that are flat modal.
 
 ## References
 
 {{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
+
+## External links
+
+- [Flat Modality](https://agda.readthedocs.io/en/latest/language/flat.html) on
+  the Agda documentation pages.
diff --git a/src/modal-type-theory/flat-sharp-adjunction.lagda.md b/src/modal-type-theory/flat-sharp-adjunction.lagda.md
index 7a249c4771..e0f9f2a500 100644
--- a/src/modal-type-theory/flat-sharp-adjunction.lagda.md
+++ b/src/modal-type-theory/flat-sharp-adjunction.lagda.md
@@ -9,26 +9,20 @@ module modal-type-theory.flat-sharp-adjunction where
 <details><summary>Imports</summary>
 
 ```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.retractions
+open import foundation.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.action-on-identifications-flat-modality
 open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-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
 ```
 
 </details>
@@ -47,69 +41,35 @@ 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
+redundancy between the postulated axioms, and they are likely to change in the
+future.
 
-### Crisp induction for `♯`
+## Definitions
 
-Sharp-Codiscrete types are local at the flat counit.
+### Crisp recursion for the sharp modality
 
 ```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
-```
+module _
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {C : UU l2}
+  (f : (@♭ x : A) → C)
+  where
 
-### Crisp elimination of `♯`
+  crisp-rec-sharp : A → ♯ C
+  crisp-rec-sharp = crisp-ind-sharp (λ _ → C) f
 
-```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
+module _
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {C : UU l2}
+  (is-codisc-C : is-sharp-codiscrete C) (f : (@♭ x : A) → C)
+  where
 
-### Crisp recursion for `♯`
+  crisp-rec-sharp-codiscrete : A → C
+  crisp-rec-sharp-codiscrete =
+    crisp-ind-sharp-codiscrete (λ _ → C) (λ _ → is-codisc-C) f
 
-```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)
+  compute-crisp-rec-sharp-codiscrete :
+    (@♭ x : A) → crisp-rec-sharp-codiscrete x ＝ f x
+  compute-crisp-rec-sharp-codiscrete =
+    compute-crisp-ind-sharp-codiscrete (λ _ → C) (λ _ → is-codisc-C) f
 ```
 
 ## Properties
@@ -121,25 +81,25 @@ crisp-tr-sharp :
 crisp-tr-sharp refl {x} = uniqueness-crisp-elim-sharp x
 ```
 
-### Crisp induction on `♯` implies typal induction
+### Crisp induction on `♯` implies cohesive induction
 
 ```agda
-ind-crisp-ind-sharp :
+ind-crisp-ind-sharp-codiscrete :
   {@♭ 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
+ind-crisp-ind-sharp-codiscrete {A = A} C is-codisc-C f x' =
+  crisp-ind-sharp-codiscrete
     ( λ 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))))
+          ( λ p → is-codisc-C (tr ♯ p y))))
     ( λ A' →
-      crisp-ind-sharp
+      crisp-ind-sharp-codiscrete
         ( λ y → (p : A' ＝ A) → C (tr ♯ p y))
-        ( λ y → is-sharp-codiscrete-Π (λ p → is-sharp-codiscrete-C (tr ♯ p y)))
+        ( λ y → is-sharp-codiscrete-Π (λ p → is-codisc-C (tr ♯ p y)))
         ( λ x p → tr C (crisp-tr-sharp p) (f (tr id p (crisp-elim-sharp x)))))
     ( A)
     ( x')
@@ -148,67 +108,55 @@ ind-crisp-ind-sharp {A = A} C is-sharp-codiscrete-C f x' =
 
 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
+### Flat eats 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
+  action-flat-map-elim-sharp : ♭ (♯ A) → ♭ A
+  action-flat-map-elim-sharp = action-flat-crisp-map crisp-elim-sharp
+
+  action-flat-map-unit-sharp : ♭ A → ♭ (♯ A)
+  action-flat-map-unit-sharp = action-flat-map unit-sharp
+
+  is-section-action-flat-map-unit-sharp :
+    is-section action-flat-map-elim-sharp action-flat-map-unit-sharp
+  is-section-action-flat-map-unit-sharp (intro-flat x) =
+    ap-flat (compute-crisp-elim-sharp x)
+
+  is-retraction-action-flat-map-unit-sharp :
+    is-retraction action-flat-map-elim-sharp action-flat-map-unit-sharp
+  is-retraction-action-flat-map-unit-sharp (intro-flat x) =
+    ap-flat (uniqueness-crisp-elim-sharp x)
+
+  is-equiv-action-flat-map-elim-sharp : is-equiv action-flat-map-elim-sharp
+  pr1 (pr1 is-equiv-action-flat-map-elim-sharp) = action-flat-map-unit-sharp
+  pr2 (pr1 is-equiv-action-flat-map-elim-sharp) =
+    is-section-action-flat-map-unit-sharp
+  pr1 (pr2 is-equiv-action-flat-map-elim-sharp) = action-flat-map-unit-sharp
+  pr2 (pr2 is-equiv-action-flat-map-elim-sharp) =
+    is-retraction-action-flat-map-unit-sharp
+
+  equiv-action-flat-map-elim-sharp : ♭ (♯ A) ≃ ♭ A
+  pr1 equiv-action-flat-map-elim-sharp = action-flat-map-elim-sharp
+  pr2 equiv-action-flat-map-elim-sharp = is-equiv-action-flat-map-elim-sharp
+
+  is-equiv-action-flat-map-unit-sharp : is-equiv action-flat-map-unit-sharp
+  pr1 (pr1 is-equiv-action-flat-map-unit-sharp) = action-flat-map-elim-sharp
+  pr2 (pr1 is-equiv-action-flat-map-unit-sharp) =
+    is-retraction-action-flat-map-unit-sharp
+  pr1 (pr2 is-equiv-action-flat-map-unit-sharp) = action-flat-map-elim-sharp
+  pr2 (pr2 is-equiv-action-flat-map-unit-sharp) =
+    is-section-action-flat-map-unit-sharp
+
+  equiv-action-flat-map-unit-sharp : ♭ A ≃ ♭ (♯ A)
+  pr1 equiv-action-flat-map-unit-sharp = action-flat-map-unit-sharp
+  pr2 equiv-action-flat-map-unit-sharp = is-equiv-action-flat-map-unit-sharp
 ```
 
-### Sharp after flat
+### Sharp eats flat
 
 ```agda
 module _
@@ -218,71 +166,19 @@ module _
   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)))
+  ap-sharp-intro-flat : ♯ A → ♯ (♭ A)
+  ap-sharp-intro-flat = rec-sharp (crisp-rec-sharp intro-flat)
 ```
 
 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
+- In [sharp 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).
 
diff --git a/src/modal-type-theory/functoriality-flat-modality.lagda.md b/src/modal-type-theory/functoriality-flat-modality.lagda.md
new file mode 100644
index 0000000000..9f822969d8
--- /dev/null
+++ b/src/modal-type-theory/functoriality-flat-modality.lagda.md
@@ -0,0 +1,187 @@
+# Functoriality of the flat modality
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.functoriality-flat-modality where
+```
+
+<details><summary>Imports</summary>
+
+```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.retracts-of-types
+open import foundation.sections
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-identifications-flat-modality
+open import modal-type-theory.flat-modality
+```
+
+</details>
+
+## Idea
+
+The [flat modality](modal-type-theory.flat-modality.md) is functorial.
+
+- Given a map `f : A → B`, there is a map `♭f : ♭ A → ♭ B`
+- Given two composable maps `f` and `g`, the image of their composite computes
+  as `♭(g ∘ f) ~ ♭g ∘ ♭f`
+- The identity is mapped to the identity.
+
+## Definitions
+
+### The flat modality's action on type families
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1}
+  where
+
+  action-flat-crisp-family : @♭ (@♭ A → UU l2) → ♭ A → UU l2
+  action-flat-crisp-family B (intro-flat x) = ♭ (B x)
+
+  action-flat-family : @♭ (A → UU l2) → ♭ A → UU l2
+  action-flat-family B = action-flat-crisp-family (crispen B)
+```
+
+### The flat modality's action on maps
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1}
+  where
+
+  action-flat-crisp-dependent-map :
+    {@♭ B : @♭ A → UU l2} →
+    @♭ ((@♭ x : A) → B x) →
+    ((x : ♭ A) → action-flat-crisp-family B x)
+  action-flat-crisp-dependent-map f (intro-flat x) = intro-flat (f x)
+
+  action-flat-dependent-map :
+    {@♭ B : A → UU l2} →
+    @♭ ((x : A) → B x) →
+    ((x : ♭ A) → action-flat-family B x)
+  action-flat-dependent-map f = action-flat-crisp-dependent-map (crispen f)
+
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  action-flat-crisp-map : @♭ (@♭ A → B) → (♭ A → ♭ B)
+  action-flat-crisp-map f (intro-flat x) =
+    action-flat-crisp-dependent-map f (intro-flat x)
+
+  action-flat-map : @♭ (A → B) → (♭ A → ♭ B)
+  action-flat-map f = action-flat-crisp-map (crispen f)
+```
+
+### The flat modality's coaction on maps
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  coap-map-flat : (♭ A → ♭ B) → (@♭ A → B)
+  coap-map-flat f x = counit-flat (f (intro-flat x))
+
+  is-crisp-retraction-coap-map-flat :
+    (@♭ f : @♭ A → B) → coap-map-flat (action-flat-crisp-map f) ＝ f
+  is-crisp-retraction-coap-map-flat _ = refl
+```
+
+## Properties
+
+### Naturality of the flat counit
+
+The counit of the flat modality is natural with respect to the action on maps:
+we have [commuting squares](foundation-core.commuting-squares-of-maps.md)
+
+```text
+               ♭ f
+         ♭ A ------> ♭ B
+          |           |
+ counit-♭ |           | counit-♭
+          ∨           ∨
+          A --------> B.
+                f
+```
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  naturality-counit-flat :
+    (@♭ f : A → B) → counit-flat ∘ action-flat-map f ~ f ∘ counit-flat
+  naturality-counit-flat f (intro-flat x) = refl
+```
+
+### Functoriality of the action on maps
+
+```agda
+module _
+  {@♭ l1 : Level} {@♭ A : UU l1}
+  where
+
+  preserves-id-action-flat-map : action-flat-map (id {A = A}) ~ id
+  preserves-id-action-flat-map (intro-flat x) = refl
+
+module _
+  {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ C : UU l3}
+  where
+
+  preserves-comp-action-flat-map :
+    (@♭ f : A → B) (@♭ g : B → C) →
+    action-flat-map (g ∘ f) ~ action-flat-map g ∘ action-flat-map f
+  preserves-comp-action-flat-map f g (intro-flat x) = refl
+```
+
+### The functorial action preserves equivalences
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ f : A → B}
+  where
+
+  action-flat-section : @♭ section f → section (action-flat-map f)
+  pr1 (action-flat-section (g , H)) = action-flat-map g
+  pr2 (action-flat-section (g , H)) (intro-flat x) = ap-flat (H x)
+
+  action-flat-retraction : @♭ retraction f → retraction (action-flat-map f)
+  pr1 (action-flat-retraction (g , H)) = action-flat-map g
+  pr2 (action-flat-retraction (g , H)) (intro-flat x) = ap-flat (H x)
+
+  is-equiv-ap-is-equiv-map-flat : @♭ is-equiv f → is-equiv (action-flat-map f)
+  is-equiv-ap-is-equiv-map-flat (s , r) =
+    ( action-flat-section s , action-flat-retraction r)
+
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
+  where
+
+  action-flat-retract : @♭ (A retract-of B) → ♭ A retract-of ♭ B
+  action-flat-retract (f , r) = (action-flat-map f , action-flat-retraction r)
+
+  action-flat-equiv : @♭ (A ≃ B) → ♭ A ≃ ♭ B
+  action-flat-equiv (f , H) =
+    (action-flat-map f , is-equiv-ap-is-equiv-map-flat H)
+```
+
+## 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 crisp types](modal-type-theory.flat-discrete-crisp-types.md)
+  for crisp types that are flat modal.
+
+## References
+
+{{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
diff --git a/src/modal-type-theory/functoriality-sharp-modality.lagda.md b/src/modal-type-theory/functoriality-sharp-modality.lagda.md
new file mode 100644
index 0000000000..673562dad9
--- /dev/null
+++ b/src/modal-type-theory/functoriality-sharp-modality.lagda.md
@@ -0,0 +1,59 @@
+# Functoriality of the sharp modality
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.functoriality-sharp-modality where
+```
+
+<details><summary>Imports</summary>
+
+```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 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.modal-subuniverse-induction
+```
+
+</details>
+
+## Idea
+
+The [sharp modality](modal-type-theory.sharp-modality.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).
+
+## Definitions
+
+### The sharp modality's action on maps
+
+```agda
+action-sharp-map :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → (♯ A → ♯ B)
+action-sharp-map f = rec-sharp (unit-sharp ∘ f)
+```
diff --git a/src/modal-type-theory/sharp-codiscrete-maps.lagda.md b/src/modal-type-theory/sharp-codiscrete-maps.lagda.md
index 2dab4ff828..b6f62e6748 100644
--- a/src/modal-type-theory/sharp-codiscrete-maps.lagda.md
+++ b/src/modal-type-theory/sharp-codiscrete-maps.lagda.md
@@ -20,31 +20,25 @@ 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).
+A map is said to be
+{{#concept "sharp codiscrete" Disambiguation="map" Agda=is-sharp-codiscrete-map}}
+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 : UU (l1 ⊔ l2)
+  is-sharp-codiscrete-map = is-sharp-codiscrete-family (fiber f)
+
   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 is-sharp-codiscrete-map
   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
index 010ddf83e5..887f38e44e 100644
--- a/src/modal-type-theory/sharp-codiscrete-types.lagda.md
+++ b/src/modal-type-theory/sharp-codiscrete-types.lagda.md
@@ -9,9 +9,11 @@ module modal-type-theory.sharp-codiscrete-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
+open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
@@ -21,15 +23,16 @@ open import foundation.universe-levels
 open import modal-type-theory.sharp-modality
 
 open import orthogonal-factorization-systems.higher-modalities
+open import orthogonal-factorization-systems.modal-operators
 ```
 
 </details>
 
 ## 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.
+A type is said to be {{#concept "sharp codiscrete" Agda=is-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
 
@@ -43,23 +46,88 @@ here and in the files on
 file on the [sharp modality](modal-type-theory.sharp-modality.md), and they may
 be subject to change in the future.
 
-## Definition
+## Definitions
+
+### Sharp codiscrete types
 
 ```agda
-is-sharp-codiscrete : {l : Level} (A : UU l) → UU l
-is-sharp-codiscrete {l} A = is-equiv (unit-sharp {l} {A})
+module _
+  {l : Level} (A : UU l)
+  where
+
+  is-sharp-codiscrete : UU l
+  is-sharp-codiscrete = is-modal unit-sharp A
+
+  is-sharp-codiscrete-Prop : Prop l
+  is-sharp-codiscrete-Prop = is-modal-Prop unit-sharp A
+
+  is-property-is-sharp-codiscrete : is-prop is-sharp-codiscrete
+  is-property-is-sharp-codiscrete = is-property-is-modal unit-sharp A
+```
+
+### Sharp codiscrete families
 
+```agda
 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)
+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
+```
+
+### The subuniverse of sharp codiscrete types
+
+```agda
+Sharp-Codiscrete-Type : (l : Level) → UU (lsuc l)
+Sharp-Codiscrete-Type l = Σ (UU l) (is-sharp-codiscrete)
+
+module _
+  {l : Level} (A : Sharp-Codiscrete-Type l)
+  where
+
+  type-Sharp-Codiscrete-Type : UU l
+  type-Sharp-Codiscrete-Type = pr1 A
+
+  is-sharp-codiscrete-type-Sharp-Codiscrete-Type :
+    is-sharp-codiscrete type-Sharp-Codiscrete-Type
+  is-sharp-codiscrete-type-Sharp-Codiscrete-Type = pr2 A
+```
+
+### Crisp induction for sharp codiscrete types
+
+The following is Theorem 3.3 in {{#cite Shu18}}.
+
+```agda
+crisp-ind-sharp-codiscrete :
+  {@♭ 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
+crisp-ind-sharp-codiscrete C is-codisc-C f x =
+  map-inv-is-equiv (is-codisc-C x) (crisp-ind-sharp C f x)
+
+compute-crisp-ind-sharp-codiscrete :
+  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : A → UU l2)
+  (is-codisc-C : (x : A) → is-sharp-codiscrete (C x))
+  (f : (@♭ x : A) → C x) →
+  (@♭ x : A) → crisp-ind-sharp-codiscrete C is-codisc-C f x ＝ f x
+compute-crisp-ind-sharp-codiscrete C is-codisc-C f x =
+  ( ap (map-inv-is-equiv (is-codisc-C x)) (compute-crisp-ind-sharp C f x)) ∙
+  ( is-retraction-map-inv-is-equiv (is-codisc-C x) (f x))
 ```
 
 ## Postulates
 
-### The identity types of `♯` are codiscrete
+### The identity types of `♯ A` are sharp codiscrete
 
 ```agda
 postulate
@@ -69,14 +137,14 @@ postulate
 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 =
+is-sharp-codiscrete-Id x y is-sharp-A =
   map-tr-equiv
     ( is-sharp-codiscrete)
-    ( inv-equiv-ap-is-emb (is-emb-is-equiv is-sharp-codiscrete-A))
+    ( inv-equiv-ap-is-emb (is-emb-is-equiv is-sharp-A))
     ( is-sharp-codiscrete-Id-sharp (unit-sharp x) (unit-sharp y))
 ```
 
-### A `Π`-type is codiscrete if its codomain is
+### A dependent function type is codiscrete if its codomain is
 
 ```agda
 postulate
@@ -84,45 +152,24 @@ postulate
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
     ((x : A) → is-sharp-codiscrete (B x)) →
     is-sharp-codiscrete ((x : A) → B x)
+
+is-sharp-codiscrete-function-type :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  is-sharp-codiscrete B →
+  is-sharp-codiscrete (A → B)
+is-sharp-codiscrete-function-type is-sharp-B =
+  is-sharp-codiscrete-Π (λ _ → is-sharp-B)
 ```
 
 ### The universe of codiscrete types is codiscrete
 
 ```agda
 postulate
-  is-sharp-codiscrete-Sharp-Codiscrete :
-    (l : Level) → is-sharp-codiscrete (Sharp-Codiscrete l)
+  is-sharp-codiscrete-Sharp-Codiscrete-Type :
+    (l : Level) → is-sharp-codiscrete (Sharp-Codiscrete-Type 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
+### The sharp higher modality
 
 ```agda
 module _
@@ -140,7 +187,72 @@ module _
   pr2 (pr2 sharp-higher-modality) = is-higher-modality-sharp
 ```
 
-### Types in the image of `♯` are codiscrete
+### Iterated crisp induction for sharp codiscrete types
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {l3 : Level}
+  {@♭ A : UU l1} {@♭ B : A → UU l2} (C : (x : A) → B x → UU l3)
+  (is-codisc-C : (x : A) (y : B x) → is-sharp-codiscrete (C x y))
+  (f : (@♭ x : A) (@♭ y : B x) → C x y)
+  where
+
+  crisp-binary-ind-sharp-codiscrete : (x : A) (y : B x) → C x y
+  crisp-binary-ind-sharp-codiscrete =
+    crisp-ind-sharp-codiscrete
+      ( λ x → (y : B x) → C x y)
+      ( λ x → is-sharp-codiscrete-Π (is-codisc-C x))
+      ( λ x → crisp-ind-sharp-codiscrete (C x) (is-codisc-C x) (f x))
+
+  compute-crisp-binary-ind-sharp-codiscrete :
+    (@♭ x : A) (@♭ y : B x) → crisp-binary-ind-sharp-codiscrete x y ＝ f x y
+  compute-crisp-binary-ind-sharp-codiscrete x y =
+    ( htpy-eq
+      ( compute-crisp-ind-sharp-codiscrete
+        ( λ x → (y : B x) → C x y)
+        ( λ x → is-sharp-codiscrete-Π (is-codisc-C x))
+        ( λ x → crisp-ind-sharp-codiscrete (C x) (is-codisc-C x) (f x))
+        ( x))
+      ( y)) ∙
+    ( compute-crisp-ind-sharp-codiscrete (C x) (is-codisc-C x) (f x) y)
+
+module _
+  {@♭ l1 l2 l3 : Level} {l4 : Level}
+  {@♭ A : UU l1} {@♭ B : A → UU l2} {@♭ C : (x : A) → B x → UU l3}
+  (D : (x : A) (y : B x) → C x y → UU l4)
+  (is-codisc-D : (x : A) (y : B x) (z : C x y) → is-sharp-codiscrete (D x y z))
+  (f : (@♭ x : A) (@♭ y : B x) (@♭ z : C x y) → D x y z)
+  where
+
+  crisp-ternary-ind-sharp-codiscrete : (x : A) (y : B x) (z : C x y) → D x y z
+  crisp-ternary-ind-sharp-codiscrete =
+    crisp-ind-sharp-codiscrete
+      ( λ x → (y : B x) (z : C x y) → D x y z)
+      ( λ x →
+        is-sharp-codiscrete-Π (λ y → is-sharp-codiscrete-Π (is-codisc-D x y)))
+      ( λ x → crisp-binary-ind-sharp-codiscrete (D x) (is-codisc-D x) (f x))
+
+  compute-crisp-ternary-ind-sharp-codiscrete :
+    (@♭ x : A) (@♭ y : B x) (@♭ z : C x y) →
+    crisp-ternary-ind-sharp-codiscrete x y z ＝ f x y z
+  compute-crisp-ternary-ind-sharp-codiscrete x y z =
+    ( htpy-eq
+      ( htpy-eq
+        ( compute-crisp-ind-sharp-codiscrete
+          ( λ x → (y : B x) (z : C x y) → D x y z)
+          ( λ x →
+            is-sharp-codiscrete-Π
+              ( λ y → is-sharp-codiscrete-Π (is-codisc-D x y)))
+          ( λ x → crisp-binary-ind-sharp-codiscrete (D x) (is-codisc-D x) (f x))
+          ( x))
+        ( y))
+      ( z)) ∙
+    ( compute-crisp-binary-ind-sharp-codiscrete (D x) (is-codisc-D x) (f x) y z)
+```
+
+## Properties
+
+### Types in the image of the sharp modality are codiscrete
 
 ```agda
 is-sharp-codiscrete-sharp : {l : Level} (X : UU l) → is-sharp-codiscrete (♯ X)
@@ -150,5 +262,5 @@ is-sharp-codiscrete-sharp {l} =
 
 ## See also
 
-- [Flat discrete types](modal-type-theory.flat-discrete-types.md) for the dual
-  notion.
+- [Flat discrete crisp types](modal-type-theory.flat-discrete-crisp-types.md)
+  for a partial dual notion.
diff --git a/src/modal-type-theory/sharp-modality.lagda.md b/src/modal-type-theory/sharp-modality.lagda.md
index 6788e8ef3a..ba9c2f224e 100644
--- a/src/modal-type-theory/sharp-modality.lagda.md
+++ b/src/modal-type-theory/sharp-modality.lagda.md
@@ -26,22 +26,26 @@ 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
+The {{#concept "sharp modality" Agda=♯}} `♯` is an axiomatized
+[monadic modality](orthogonal-factorization-systems.higher-modalities.md) that
+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
+In this file, we postulate that `♯` is a
+[modal operator](orthogonal-factorization-systems.modal-operators.md) with a
+crisp elimination principle and 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.
+
+- In the file about
+  [sharp codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we
+  currently 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
+that they are likely to change in the future.
 
 ## Postulates
 
@@ -49,17 +53,217 @@ axioms, and they may be subject to change in the future.
 postulate
   ♯ : {l : Level} (A : UU l) → UU l
 
-  @♭ unit-sharp : {l : Level} {A : UU l} → A → ♯ A
+  unit-sharp : {l : Level} {A : UU l} → A → ♯ A
+
+sharp : {l : Level} (A : UU l) → UU l
+sharp = ♯
+```
+
+### Crisp elimination for the sharp modality
+
+Given a crisp element `x :: ♯ A` we recover an element of `A`. We postulate that
+this construction is a crisp
+[coherent inverse](foundation-core.coherently-invertible-maps.md) to the sharp
+unit.
+
+```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))
+```
+
+**Rewriting.** In the future we may enable rewrite rules for the computation and
+uniqueness property of the crisp elimination principle for the sharp modality.
+
+```text
+  {-# REWRITE compute-crisp-elim-sharp uniqueness-crisp-elim-sharp #-}
+```
+
+### Crisp induction for the sharp modality
+
+The
+{{#concept "crisp induction principle" Disambiguation="for the sharp modality" Agda=crisp-ind-sharp}}
+for the sharp modality is a crisp version of the principle that 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) → C x) → (x : A) → ♯ (C x)
+
+  compute-crisp-ind-sharp :
+    {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : A → UU l2)
+    (f : (@♭ x : A) → C x) →
+    (@♭ x : A) → crisp-ind-sharp C f x ＝ unit-sharp (f x)
+```
+
+**Rewriting.** In the future, we may enable a rewriting for the computation rule
+of the crisp induction principle for the sharp modality.
+
+```text
+  {-# REWRITE compute-crisp-ind-sharp #-}
+```
+
+### Modal induction for the sharp modality
+
+We postulate that sharp satisfies a
+[modal induction principle](orthogonal-factorization-systems.modal-induction.md)
+below.
+
+**Note.** It should also be possible to construct it from the more general
+`pointwise-sharp` considered below, but we leave this for future work.
 
+```agda
+postulate
   ind-sharp :
     {l1 l2 : Level} {A : UU l1} (C : ♯ A → UU l2) →
     ((x : A) → ♯ (C (unit-sharp x))) →
-    ((x : ♯ A) → ♯ (C 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
+    ind-sharp C f ∘ unit-sharp ~ f
+```
+
+### The sharp modality's action on "pointwise" type families
+
+**TODO.** This section consists entirely of unfinished work that is not
+typechecked as part of the library. This code is included as notes for future
+work.
+
+```text
+postulate
+  pointwise-sharp :
+    {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} → (@♭ A → UU l2) → A → UU l2
+```
+
+```text
+postulate
+  unit-pointwise-sharp :
+    {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level}
+    {B : @♭ A → UU l2} (a : (@♭ x : A) → B x) →
+    (x : A) → pointwise-sharp B x
+
+  elim-pointwise-sharp :
+    {@♭ l1 l2 : Level} {@♭ A : UU l1} {B : @♭ A → UU l2}
+    (f : (@♭ x : A) → pointwise-sharp B x) → (@♭ x : A) → B x
+
+  compute-pointwise-sharp :
+    {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level}
+    (B : A → UU l2) (x : A) → pointwise-sharp (λ a → B a) x ＝ ♯ (B x)
+
+  {-# REWRITE compute-pointwise-sharp #-}
+
+  compute-unit-pointwise-sharp :
+    {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level}
+    {B : @♭ A → UU l2} (f : (@♭ x : A) → B x)
+    (@♭ x : A) → unit-pointwise-sharp f x ＝ unit-sharp (f x)
+
+  -- {-# REWRITE compute-unit-pointwise-sharp #-}
+
+syntax elim-pointwise-sharp (λ γ → a) ctx = let♯ γ ::= ctx in♯ a ↓↓♯
+```
+
+**Warning:** When normalizing `λ B x → unit-pointwise-sharp f x`, the rewrite
+`compute-unit-pointwise-sharp` will fire turning it into `unit-sharp (f x)`,
+which is ill-typed on cohesive `x : A` (and the typechecker complains).
+{{#cite DavidJaz/Cohesion}} (May be outdated info)
+
+```text
+postulate
+  compute-elim-pointwise-sharp :
+    {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
+    (@♭ f : (@♭ x : A) → pointwise-sharp B x)
+    (@♭ x : A) → elim-pointwise-sharp f x ＝ crisp-elim-sharp (f x)
+
+  {-# REWRITE compute-elim-pointwise-sharp #-}
+```
+
+#### Uncrispening contexts
+
+```text
+record
+  context-uncrisp-sharp
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} : UU (lsuc (l1 ⊔ l2))
+  where
+  constructor ctx
+  field
+    ᶜB : A → UU l2
+    ᶜf : (@♭ x : A) → ♯ (ᶜB x)
+    ᶜa : A
+
+open context-uncrisp-sharp
+
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1}
+  where
+
+  uncrisp-sharp : (B : A → UU l2) (f : (@♭ x : A) → ♯ (B x)) → (x : A) → ♯ (B x)
+  uncrisp-sharp B f x =
+    unit-pointwise-sharp (λ γ → crisp-elim-sharp ((ᶜf γ) (ᶜa γ))) (ctx B f x)
+
+  compute-uncrisp-sharp :
+    (@♭ B : A → UU l2) (@♭ f : (@♭ x : A) → ♯ (B x)) (@♭ x : A) →
+    uncrisp-sharp B f x ＝ f x
+  compute-uncrisp-sharp B f x =
+    compute-unit-pointwise-sharp
+      ( λ γ → crisp-elim-sharp ((ᶜf γ) (ᶜa γ)))
+      ( ctx B f x)
+
+module _
+  {@♭ l1 l2 l3 : Level}
+  {@♭ A : UU l1} {@♭ B : A → UU l2}
+  where
+
+  uncrisp-sharp² :
+    (C : (x : A) → B x → UU l3)
+    (f : (@♭ x : A) (@♭ y : B x) → ♯ (C x y))
+    (x : A) (y : B x) → ♯ (C x y)
+  uncrisp-sharp² C f x y =
+    uncrisp-sharp (λ (x , y) → C x y) (λ p → f (pr1 p) (pr2 p)) (x , y)
+
+  compute-uncrisp-sharp² :
+    (@♭ C : (x : A) → B x → UU l3)
+    (@♭ f : (@♭ x : A) (@♭ y : B x) → ♯ (C x y))
+    (@♭ x : A) (@♭ y : B x) → uncrisp-sharp² C f x y ＝ f x y
+  compute-uncrisp-sharp² C f x y =
+    compute-uncrisp-sharp (λ (x , y) → C x y) (λ p → f (pr1 p) (pr2 p)) (x , y)
+```
+
+#### Sharp induction revisited
+
+The following definitions rely on rewrite rules.
+
+```text
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} (@♭ C : ♯ A → UU l2)
+  (@♭ f : (x : A) → ♯ (C (unit-sharp x)))
+  where
+
+  ind-sharp' : (x : ♯ A) → ♯ (C x)
+  ind-sharp' =
+    crisp-ind-sharp C (λ x → crisp-elim-sharp (f (crisp-elim-sharp x)))
+
+  compute-ind-sharp' : (@♭ x : A) → ind-sharp' (unit-sharp x) ＝ f x
+  compute-ind-sharp' x =
+    compute-crisp-ind-sharp C
+      ( λ x → crisp-elim-sharp (f (crisp-elim-sharp x)))
+      ( unit-sharp x)
 ```
 
 ## Definitions
@@ -69,11 +273,11 @@ postulate
 ```agda
 sharp-locally-small-operator-modality :
   (l : Level) → locally-small-operator-modality l l l
-pr1 (sharp-locally-small-operator-modality l) = ♯ {l}
+pr1 (sharp-locally-small-operator-modality l) = ♯
 pr2 (sharp-locally-small-operator-modality l) A = is-locally-small' {l} {♯ A}
 ```
 
-### The sharp induction principle
+### The sharp modality's induction principle
 
 ```agda
 induction-principle-sharp :
@@ -128,7 +332,7 @@ compute-ind-subuniverse-sharp =
     ( induction-principle-subuniverse-sharp)
 ```
 
-### Sharp recursion
+### The sharp modality's recursion principle
 
 ```agda
 rec-sharp :
@@ -194,23 +398,7 @@ compute-rec-subuniverse-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
 
 {{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}}
-{{#reference Felixwellen/DCHoTT-Agda}}
+{{#reference Felixwellen/DCHoTT-Agda}} {{#reference DavidJaz/Cohesion}}
diff --git a/src/modal-type-theory/transport-along-crisp-identifications.lagda.md b/src/modal-type-theory/transport-along-crisp-identifications.lagda.md
new file mode 100644
index 0000000000..5ca52cc131
--- /dev/null
+++ b/src/modal-type-theory/transport-along-crisp-identifications.lagda.md
@@ -0,0 +1,169 @@
+# Transport along crisp identifications
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.transport-along-crisp-identifications 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.crisp-identity-types
+```
+
+</details>
+
+## Idea
+
+Given a [crisp](modal-type-theory.crisp-types.md) type family `B` that is
+[defined on crisp elements](modal-type-theory.crisp-function-types.md) of `A`, a
+crisp [identification](foundation-core.identity-types.md) `p : x ＝ y` in `A`
+and a crisp element `b : B x`, we can
+{{#concept "transport" Disambiguation="along crisp identifications" Agda=crisp-tr}}
+the element `b` along the crisp identification `p` to obtain an element
+`crisp-tr B p b : B y`.
+
+This is a strengthening of
+[transport along identifications](foundation.transport-along-identifications.md)
+for crisp identifications, because the type family `B` is allowed to depend only
+crisply on the base type `A`.
+
+## Definitions
+
+### Transport along crisp identifications
+
+```agda
+crisp-tr :
+  {@♭ l1 l2 : Level} {@♭ A : UU l1}
+  (@♭ B : @♭ A → UU l2) {@♭ x y : A}
+  (@♭ p : x ＝ y) → @♭ B x → B y
+crisp-tr B refl x = x
+```
+
+## Properties
+
+### Transport preserves concatenation of crisp identifications
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
+  where
+
+  crisp-tr-concat :
+    {@♭ x y z : A} (@♭ p : x ＝ y) (@♭ q : y ＝ z) (@♭ b : B x) →
+    crisp-tr B (p ∙ q) b ＝ crisp-tr B q (crisp-tr B p b)
+  crisp-tr-concat p q b =
+    crisp-based-ind-Id
+      ( λ y q → crisp-tr B (p ∙ q) b ＝ crisp-tr B q (crisp-tr B p b))
+      ( crisp-based-ind-Id
+        ( λ y p → crisp-tr B (p ∙ refl) b ＝ crisp-tr B p b)
+        ( refl)
+        ( p))
+      ( q)
+```
+
+### Transposing crisp transport along the inverse of a crisp identification
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
+  where
+
+  eq-transpose-crisp-tr :
+    {@♭ x y : A} (@♭ p : x ＝ y) {@♭ u : B x} {@♭ v : B y} →
+    @♭ v ＝ crisp-tr B p u → crisp-tr B (inv p) v ＝ u
+  eq-transpose-crisp-tr p {u} {.(crisp-tr B p u)} refl =
+    crisp-based-ind-Id (λ y p → crisp-tr B (inv p) (crisp-tr B p u) ＝ u) refl p
+
+  eq-transpose-crisp-tr' :
+    {@♭ x y : A} (@♭ p : x ＝ y) {@♭ u : B x} {@♭ v : B y} →
+    @♭ crisp-tr B p u ＝ v → u ＝ crisp-tr B (inv p) v
+  eq-transpose-crisp-tr' p {u} {.(crisp-tr B p u)} refl =
+    crisp-based-ind-Id (λ y p → u ＝ crisp-tr B (inv p) (crisp-tr B p u)) refl p
+```
+
+### Every crisp family of maps preserves crisp transport
+
+```agda
+preserves-crisp-tr :
+  {@♭ l1 l2 l3 : Level} {@♭ I : UU l1}
+  {@♭ A : @♭ I → UU l2} {@♭ B : @♭ I → UU l3}
+  (@♭ f : (@♭ i : I) → A i → B i)
+  {@♭ i j : I} (@♭ p : i ＝ j) (@♭ x : A i) →
+  f j (crisp-tr A p x) ＝ crisp-tr B p (f i x)
+preserves-crisp-tr {A = A} {B} f {i} p x =
+  crisp-based-ind-Id
+    ( λ j p → f j (crisp-tr A p x) ＝ crisp-tr B p (f i x))
+    ( refl)
+    ( p)
+```
+
+### Transporting along the action on crisp identifications of a function
+
+```agda
+crisp-tr-ap :
+  {@♭ l1 l2 l3 l4 : Level}
+  {@♭ A : UU l1} {@♭ B : @♭ A → UU l2} {@♭ C : UU l3} {@♭ D : @♭ C → UU l4}
+  (@♭ f : A → C) (@♭ g : (@♭ x : A) → B x → D (f x))
+  {@♭ x y : A} (@♭ p : x ＝ y) (@♭ z : B x) →
+  crisp-tr D (ap f p) (g x z) ＝ g y (crisp-tr B p z)
+crisp-tr-ap {A = A} {B} {C} {D} f g {x} p z =
+  crisp-based-ind-Id
+    ( λ y p → crisp-tr D (ap f p) (g x z) ＝ g y (crisp-tr B p z))
+    ( refl)
+    ( p)
+```
+
+### Computing maps out of crisp identity types as crisp transports
+
+```agda
+module _
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2} {@♭ a : A}
+  (@♭ f : (@♭ x : A) → @♭ (a ＝ x) → B x)
+  where
+
+  compute-map-out-of-crisp-identity-type :
+    (@♭ x : A) (@♭ p : a ＝ x) → f x p ＝ crisp-tr B p (f a refl)
+  compute-map-out-of-crisp-identity-type x p =
+    crisp-based-ind-Id (λ x p → f x p ＝ crisp-tr B p (f a refl)) refl p
+```
+
+### Computing crisp transport in the crisp type family of crisp identifications with a fixed target
+
+```agda
+crisp-tr-Id-left :
+  {@♭ l : Level} {@♭ A : UU l} {@♭ a b c : A} (@♭ q : b ＝ c) (@♭ p : b ＝ a) →
+  crisp-tr (_＝ a) q p ＝ (inv q ∙ p)
+crisp-tr-Id-left {a = a} q p =
+  crisp-based-ind-Id (λ y q → crisp-tr (_＝ a) q p ＝ (inv q ∙ p)) refl q
+```
+
+### Computing crisp transport in the crisp type family of crisp identifications with a fixed source
+
+```agda
+crisp-tr-Id-right :
+  {@♭ l : Level} {@♭ A : UU l} {@♭ a b c : A} (@♭ q : b ＝ c) (@♭ p : a ＝ b) →
+  crisp-tr (a ＝_) q p ＝ (p ∙ q)
+crisp-tr-Id-right {a = a} q p =
+  crisp-based-ind-Id (λ y q → crisp-tr (a ＝_) q p ＝ (p ∙ q)) (inv right-unit) q
+```
+
+### Substitution law for crisp transport
+
+```agda
+substitution-law-crisp-tr :
+  {@♭ l1 l2 l3 : Level} {@♭ X : UU l1} {@♭ A : UU l2} (@♭ B : @♭ A → UU l3)
+  (@♭ f : X → A)
+  {@♭ x y : X} (@♭ p : x ＝ y) {@♭ x' : B (f x)} →
+  crisp-tr B (ap f p) x' ＝ crisp-tr (λ (@♭ x : X) → B (f x)) p x'
+substitution-law-crisp-tr {X = X} B f p {x'} =
+  crisp-based-ind-Id
+    ( λ y p → crisp-tr B (ap f p) x' ＝ crisp-tr (λ (@♭ x : X) → B (f x)) p x')
+    ( refl)
+    ( p)
+```
diff --git a/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md b/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md
new file mode 100644
index 0000000000..a6bd8f03a0
--- /dev/null
+++ b/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md
@@ -0,0 +1,102 @@
+# The universal property of flat discrete crisp types
+
+```agda
+{-# OPTIONS --cohesion --flat-split #-}
+
+module modal-type-theory.universal-property-flat-discrete-crisp-types where
+```
+
+<details><summary>Imports</summary>
+
+```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.identity-types
+open import foundation.postcomposition-functions
+open import foundation.universal-property-equivalences
+open import foundation.universe-levels
+
+open import modal-type-theory.action-on-identifications-crisp-functions
+open import modal-type-theory.crisp-function-types
+open import modal-type-theory.flat-discrete-crisp-types
+open import modal-type-theory.flat-modality
+open import modal-type-theory.functoriality-flat-modality
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "universal property" Disambiguation="of flat discrete crisp types" Agda=universal-property-flat-discrete-crisp-type}}
+of a [flat discrete crisp type](modal-type-theory.flat-discrete-crisp-types.md)
+`A` states that under the [flat modality](modal-type-theory.flat-modality.md)
+`♭`, `A` is colocal at the counit of `♭`.
+
+By this we mean that for every [crisp type](modal-type-theory.crisp-types.md)
+`B` the map
+
+```text
+  coev-flat : ♭ (A → ♭ B) → ♭ (A → B)
+```
+
+is an [equivalence](foundation-core.equivalences.md).
+
+## Definitions
+
+### The universal property of flat discrete crisp types
+
+```agda
+coev-flat :
+  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} → ♭ (A → ♭ B) → ♭ (A → B)
+coev-flat {A = A} (intro-flat f) = intro-flat (postcomp A counit-flat f)
+
+universal-property-flat-discrete-crisp-type :
+  {@♭ l1 : Level} (@♭ A : UU l1) → UUω
+universal-property-flat-discrete-crisp-type A =
+  {@♭ l : Level} {@♭ B : UU l} → is-equiv (coev-flat {A = A} {B = B})
+```
+
+## Properties
+
+### Flat discrete crisp types satisfy the universal property of flat discrete crisp types
+
+This is Corollary 6.15 of {{#cite Shu18}}.
+
+```agda
+module _
+  {@♭ l : Level} {@♭ A : UU l}
+  where
+
+  abstract
+    universal-property-is-flat-discrete-crisp :
+      @♭ is-flat-discrete-crisp A →
+      universal-property-flat-discrete-crisp-type A
+    universal-property-is-flat-discrete-crisp
+      is-disc-A {B = B} =
+      is-equiv-htpy-equiv
+        ( ( action-flat-equiv
+            ( equiv-precomp (inv-equiv (counit-flat , is-disc-A)) B)) ∘e
+          ( equiv-action-flat-map-postcomp-counit-flat) ∘e
+          ( action-flat-equiv (equiv-precomp (counit-flat , is-disc-A) (♭ B))))
+        ( λ where
+          (intro-flat f) →
+            crisp-ap
+              ( intro-flat)
+              ( eq-htpy
+                ( λ x →
+                  ap
+                    ( counit-flat ∘ f)
+                    ( inv (is-section-map-inv-is-equiv is-disc-A x)))))
+```
+
+## See also
+
+- [The dependent universal property of flat discrete crisp types](modal-type-theory.dependent-universal-property-flat-discrete-crisp-types.md)
+
+## References
+
+{{#bibliography}} {{#reference Shu18}}