diff --git a/references.bib b/references.bib
index c6d8309360..c2241820e2 100644
--- a/references.bib
+++ b/references.bib
@@ -513,6 +513,20 @@ @online{oeis
   howpublished = {website},
 }
 
+@phdthesis{Qui16,
+  title = {Lawvere–Tierney sheafification in Homotopy Type Theory},
+  author = {Quirin, Kevin},
+  url = {https://kevinquirin.github.io/thesis/main.pdf},
+  year = {2016},
+  month = dec,
+  number = {2016EMNA0298},
+  school = {École des Mines de Nantes},
+  abstract = {The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere–Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere–Tierney sheafification functor, which is the main theorem presented in this thesis.
+  To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities.
+  Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].},
+  langid = {english}
+}
+
 @book{Rie17,
   title     = {Category {{Theory}} in {{Context}}},
   author    = {Riehl, Emily},
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 80b0349369..4ef87dd612 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -85,6 +85,7 @@ open import foundation.connected-types public
 open import foundation.constant-maps public
 open import foundation.constant-span-diagrams public
 open import foundation.constant-type-families public
+open import foundation.continuations public
 open import foundation.contractible-maps public
 open import foundation.contractible-types public
 open import foundation.copartial-elements public
diff --git a/src/foundation/continuations.lagda.md b/src/foundation/continuations.lagda.md
new file mode 100644
index 0000000000..37edfe73e0
--- /dev/null
+++ b/src/foundation/continuations.lagda.md
@@ -0,0 +1,198 @@
+# The continuation monad
+
+```agda
+module foundation.continuations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equality-cartesian-product-types
+open import foundation.evaluation-functions
+open import foundation.function-extensionality
+open import foundation.logical-equivalences
+open import foundation.type-arithmetic-cartesian-product-types
+open import foundation.type-arithmetic-dependent-function-types
+open import foundation.type-arithmetic-empty-type
+open import foundation.type-arithmetic-unit-type
+open import foundation.unit-type
+open import foundation.universal-property-cartesian-product-types
+open import foundation.universal-property-empty-type
+open import foundation.universal-property-equivalences
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.retractions
+open import foundation-core.sections
+open import foundation-core.transport-along-identifications
+
+open import orthogonal-factorization-systems.extensions-of-maps
+open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.uniquely-eliminating-modalities
+```
+
+</details>
+
+## Idea
+
+Given a type `R`, the
+{{#concept "continuation monad" Disambiguation="on a type" Agda=continuation}}
+on `R` is the functorial construction defined on types by
+
+```text
+  A ↦ ((A → R) → R).
+```
+
+## Definitions
+
+### The operator of the continuation monad
+
+```agda
+continuation :
+  {l1 l2 : Level} (R : UU l1) (A : UU l2) → UU (l1 ⊔ l2)
+continuation R A = (A → R) → R
+```
+
+### The functorial action of the continuation monad on maps
+
+```agda
+map-continuation :
+  {l1 l2 l3 : Level} {R : UU l1} {A : UU l2} {B : UU l3} →
+  (A → B) → continuation R A → continuation R B
+map-continuation f c g = c (g ∘ f)
+```
+
+### The unit of the continuation monad
+
+```agda
+unit-continuation :
+  {l1 l2 : Level} {R : UU l1} {A : UU l2} → A → continuation R A
+unit-continuation = ev
+```
+
+### Maps into `continuation R A` extend along the unit
+
+Every `f` as in the following diagram
+[extends](orthogonal-factorization-systems.extensions-of-maps.md) along the unit
+of its domain
+
+```text
+               f
+         A -------> continuation R B
+         |           ∧
+     η_A |         ⋰
+         ∨       ⋰
+  continuation R A.
+```
+
+```agda
+module _
+  {l1 l2 l3 : Level} {R : UU l1} {A : UU l2} {B : UU l3}
+  where
+
+  extend-continuation :
+    (A → continuation R B) → (continuation R A → continuation R B)
+  extend-continuation f c g = c (λ a → f a g)
+
+  is-extension-extend-continuation :
+    (f : A → continuation R B) →
+    is-extension unit-continuation f (extend-continuation f)
+  is-extension-extend-continuation f = refl-htpy
+
+  extension-continuation :
+    (f : A → continuation R B) → extension unit-continuation f
+  extension-continuation f =
+    ( extend-continuation f , is-extension-extend-continuation f)
+```
+
+### The monoidal multiplication operation of the continuation monad
+
+```agda
+mul-continuation :
+  {l1 l2 : Level} {R : UU l1} {A : UU l2} →
+  continuation R (continuation R A) → continuation R A
+mul-continuation f c = f (ev c)
+```
+
+## Properties
+
+### The right unit law for the continuation monad
+
+```agda
+module _
+  {l1 l2 : Level} {R : UU l1} {A : UU l2}
+  where
+
+  right-unit-law-mul-continuation :
+    mul-continuation {R = R} ∘ unit-continuation {R = R} {continuation R A} ~ id
+  right-unit-law-mul-continuation = refl-htpy
+```
+
+### The continuation monad on propositions gives propositions
+
+```agda
+is-prop-continuation :
+  {l1 l2 : Level} {R : UU l1} {A : UU l2} →
+  is-prop R → is-prop (continuation R A)
+is-prop-continuation = is-prop-function-type
+
+is-prop-continuation-Prop :
+  {l1 l2 : Level} (R : Prop l1) {A : UU l2} →
+  is-prop (continuation (type-Prop R) A)
+is-prop-continuation-Prop R = is-prop-continuation (is-prop-type-Prop R)
+
+continuation-Prop :
+  {l1 l2 : Level} (R : Prop l1) (A : UU l2) → Prop (l1 ⊔ l2)
+continuation-Prop R A =
+  ( continuation (type-Prop R) A , is-prop-continuation (is-prop-type-Prop R))
+```
+
+### Computing `continuation R` on the unit type
+
+We have the [equivalence](foundation-core.equivalences.md)
+
+```text
+  continuation R unit ≃ (R → R).
+```
+
+```agda
+module _
+  {l1 : Level} {R : UU l1}
+  where
+
+  compute-unit-continuation : continuation R unit ≃ (R → R)
+  compute-unit-continuation =
+    equiv-precomp (inv-left-unit-law-function-type R) R
+```
+
+### Computing `continuation R` on the empty type
+
+We have the equivalence
+
+```text
+  continuation R empty ≃ R.
+```
+
+```agda
+module _
+  {l1 : Level} {R : UU l1}
+  where
+
+  compute-empty-continuation : continuation R empty ≃ R
+  compute-empty-continuation =
+    left-unit-law-Π-is-contr (universal-property-empty' R) ex-falso
+```
+
+## External links
+
+- [continuation monad](https://ncatlab.org/nlab/show/continuation+monad) at
+  $n$Lab
diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md
index d313b548d3..ab3e6ede25 100644
--- a/src/foundation/double-negation-modality.lagda.md
+++ b/src/foundation/double-negation-modality.lagda.md
@@ -7,14 +7,18 @@ module foundation.double-negation-modality where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
 open import foundation.double-negation
+open import foundation.empty-types
+open import foundation.logical-equivalences
+open import foundation.negation
+open import foundation.propositions
+open import foundation.unit-type
 open import foundation.universe-levels
 
-open import foundation-core.function-types
-open import foundation-core.propositions
-open import foundation-core.transport-along-identifications
-
-open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.continuation-modalities
+open import orthogonal-factorization-systems.large-lawvere-tierney-topologies
+open import orthogonal-factorization-systems.lawvere-tierney-topologies
 open import orthogonal-factorization-systems.modal-operators
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities
 ```
@@ -44,27 +48,37 @@ unit-double-negation-modality = intro-double-negation
 
 ### The double negation modality is a uniquely eliminating modality
 
+The double negation modality is an instance of a
+[continuation modality](orthogonal-factorization-systems.continuation-modalities.md).
+
 ```agda
 is-uniquely-eliminating-modality-double-negation-modality :
   {l : Level} →
   is-uniquely-eliminating-modality (unit-double-negation-modality {l})
-is-uniquely-eliminating-modality-double-negation-modality {l} {A} P =
-  is-local-dependent-type-is-prop
-    ( unit-double-negation-modality)
-    ( operator-double-negation-modality l ∘ P)
-    ( λ _ → is-prop-double-negation)
-    ( λ f z →
-      double-negation-extend
-        ( λ (a : A) →
-          tr
-            ( ¬¬_ ∘ P)
-            ( eq-is-prop is-prop-double-negation)
-            ( f a))
-        ( z))
+is-uniquely-eliminating-modality-double-negation-modality {l} =
+  is-uniquely-eliminating-modality-continuation-modality l empty-Prop
 ```
 
-This proof follows Example 1.9 in {{#cite RSS20}}.
-
-## References
+### The double negation modality defines a Lawvere–Tierney topology
 
-{{#bibliography}}
+```agda
+is-large-lawvere-tierney-topology-double-negation :
+  is-large-lawvere-tierney-topology double-negation-Prop
+is-large-lawvere-tierney-topology-double-negation =
+  λ where
+  .is-idempotent-is-large-lawvere-tierney-topology P →
+    ( double-negation-elim-neg (¬ type-Prop P) , intro-double-negation)
+  .preserves-unit-is-large-lawvere-tierney-topology →
+    preserves-unit-continuation-modality'
+  .preserves-conjunction-is-large-lawvere-tierney-topology P Q →
+    distributive-product-continuation-modality'
+
+large-lawvere-tierney-topology-double-negation :
+  large-lawvere-tierney-topology (λ l → l)
+large-lawvere-tierney-topology-double-negation =
+  λ where
+  .operator-large-lawvere-tierney-topology →
+    double-negation-Prop
+  .is-large-lawvere-tierney-topology-large-lawvere-tierney-topology →
+    is-large-lawvere-tierney-topology-double-negation
+```
diff --git a/src/foundation/raising-universe-levels.lagda.md b/src/foundation/raising-universe-levels.lagda.md
index 75fcc7d91a..ecfd5103d0 100644
--- a/src/foundation/raising-universe-levels.lagda.md
+++ b/src/foundation/raising-universe-levels.lagda.md
@@ -71,6 +71,9 @@ compute-raise : (l : Level) {l1 : Level} (A : UU l1) → A ≃ raise l A
 pr1 (compute-raise l A) = map-raise
 pr2 (compute-raise l A) = is-equiv-map-raise
 
+inv-compute-raise : (l : Level) {l1 : Level} (A : UU l1) → raise l A ≃ A
+inv-compute-raise l A = inv-equiv (compute-raise l A)
+
 Raise : (l : Level) {l1 : Level} (A : UU l1) → Σ (UU (l1 ⊔ l)) (λ X → A ≃ X)
 pr1 (Raise l A) = raise l A
 pr2 (Raise l A) = compute-raise l A
diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md
index 8cdcfabc52..ca159a3636 100644
--- a/src/foundation/unit-type.lagda.md
+++ b/src/foundation/unit-type.lagda.md
@@ -83,6 +83,9 @@ raise-terminal-map {l2 = l2} A = const A raise-star
 
 compute-raise-unit : (l : Level) → unit ≃ raise-unit l
 compute-raise-unit l = compute-raise l unit
+
+inv-compute-raise-unit : (l : Level) → raise-unit l ≃ unit
+inv-compute-raise-unit l = inv-compute-raise l unit
 ```
 
 ## Properties
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index c1d6a104fe..fae641f0d6 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -12,6 +12,7 @@ module orthogonal-factorization-systems where
 open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
+open import orthogonal-factorization-systems.continuation-modalities public
 open import orthogonal-factorization-systems.double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.double-negation-sheaves public
 open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
@@ -30,6 +31,8 @@ open import orthogonal-factorization-systems.functoriality-pullback-hom public
 open import orthogonal-factorization-systems.global-function-classes public
 open import orthogonal-factorization-systems.higher-modalities public
 open import orthogonal-factorization-systems.identity-modality public
+open import orthogonal-factorization-systems.large-lawvere-tierney-topologies public
+open import orthogonal-factorization-systems.lawvere-tierney-topologies public
 open import orthogonal-factorization-systems.lifting-operations public
 open import orthogonal-factorization-systems.lifting-structures-on-squares public
 open import orthogonal-factorization-systems.lifts-families-of-elements public
diff --git a/src/orthogonal-factorization-systems/continuation-modalities.lagda.md b/src/orthogonal-factorization-systems/continuation-modalities.lagda.md
new file mode 100644
index 0000000000..5d116f266d
--- /dev/null
+++ b/src/orthogonal-factorization-systems/continuation-modalities.lagda.md
@@ -0,0 +1,213 @@
+# Continuation modalities
+
+```agda
+module orthogonal-factorization-systems.continuation-modalities where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.continuations
+open import foundation.dependent-pair-types
+open import foundation.equality-cartesian-product-types
+open import foundation.equivalences
+open import foundation.evaluation-functions
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-cartesian-product-types
+open import foundation.unit-type
+open import foundation.universal-property-cartesian-product-types
+open import foundation.universal-property-equivalences
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.large-lawvere-tierney-topologies
+open import orthogonal-factorization-systems.local-types
+open import orthogonal-factorization-systems.modal-operators
+open import orthogonal-factorization-systems.uniquely-eliminating-modalities
+```
+
+</details>
+
+## Idea
+
+Given a [proposition](foundation-core.propositions.md) `R`, the
+[continuations monad](foundation.continuations.md) on `R`
+
+```text
+  A ↦ ((A → R) → R)
+```
+
+defines a
+[higher modality](orthogonal-factorization-systems.higher-modalities.md).
+
+## Definitions
+
+### The underlying operators of continuation modalities
+
+```agda
+module _
+  {l1 : Level} (l2 : Level) (R : Prop l1)
+  where
+
+  operator-continuation-modality : operator-modality l2 (l1 ⊔ l2)
+  operator-continuation-modality = continuation (type-Prop R)
+
+  unit-continuation-modality :
+    unit-modality operator-continuation-modality
+  unit-continuation-modality = unit-continuation
+```
+
+## Properties
+
+### The continuation monad on a proposition forms a uniquely eliminating modality
+
+```agda
+is-uniquely-eliminating-modality-continuation-modality :
+  {l1 : Level} (l : Level) (R : Prop l1) →
+  is-uniquely-eliminating-modality (unit-continuation-modality l R)
+is-uniquely-eliminating-modality-continuation-modality l R P =
+  is-local-dependent-type-is-prop
+    ( unit-continuation-modality l R)
+    ( continuation (type-Prop R) ∘ P)
+    ( λ _ → is-prop-continuation-Prop R)
+    ( λ f c →
+      extend-continuation
+        ( λ a →
+          tr
+            ( continuation (type-Prop R) ∘ P)
+            ( eq-is-prop (is-prop-continuation-Prop R))
+            ( f a))
+        ( c))
+```
+
+This proof is a generalization of the proof given in Example 1.9 of
+{{#cite RSS20}}, where the special case when `R` is the
+[empty type](foundation-core.empty-types.md) is considered.
+
+### The continuation monad on a proposition defines a Lawvere–Tierney topology
+
+Every operator taking values in propositions that has a unit map trivially
+preserves the unit type.
+
+```agda
+preserves-unit-continuation-modality' :
+  {l1 : Level} {R : UU l1} → continuation R unit ↔ unit
+preserves-unit-continuation-modality' {R = R} =
+  ( terminal-map (continuation R unit) , unit-continuation)
+
+preserves-unit-continuation-modality :
+  {l1 : Level} (R : Prop l1) → continuation (type-Prop R) unit ≃ unit
+preserves-unit-continuation-modality R =
+  equiv-iff'
+    ( continuation-Prop R unit)
+    ( unit-Prop)
+    ( preserves-unit-continuation-modality')
+```
+
+We must verify that continuations distribute over
+[products](foundation.cartesian-product-types.md). Notice that for a general
+type `R`, there are two canonical candidates for a map
+
+```text
+  continuation R A × continuation R B → continuation R (A × B)
+```
+
+either by first computing the continuation at `A` and then computing the
+continuation at `B`, or the other way around. When `R` is a proposition, these
+agree and we get the appropriate distributivity law.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {R : UU l1} {A : UU l2} {B : UU l3}
+  where
+
+  map-distributive-product-continuation :
+    continuation R (A × B) → continuation R A × continuation R B
+  pr1 (map-distributive-product-continuation f) g = f (λ (a , b) → g a)
+  pr2 (map-distributive-product-continuation f) g = f (λ (a , b) → g b)
+
+  map-inv-distributive-product-left-first-continuation :
+    continuation R A × continuation R B → continuation R (A × B)
+  map-inv-distributive-product-left-first-continuation (fa , fb) g =
+    fb (λ b → fa (λ a → g (a , b)))
+
+  map-inv-distributive-product-right-first-continuation :
+    continuation R A × continuation R B → continuation R (A × B)
+  map-inv-distributive-product-right-first-continuation (fa , fb) g =
+    fa (λ a → fb (λ b → g (a , b)))
+
+  distributive-product-continuation-modality' :
+    continuation R (A × B) ↔ continuation R A × continuation R B
+  distributive-product-continuation-modality' =
+    ( map-distributive-product-continuation ,
+      map-inv-distributive-product-left-first-continuation)
+
+module _
+  {l1 l2 l3 : Level} (R : Prop l1) {A : UU l2} {B : UU l3}
+  where
+
+  distributive-product-continuation-modality :
+    continuation (type-Prop R) (A × B) ≃
+    continuation (type-Prop R) A × continuation (type-Prop R) B
+  distributive-product-continuation-modality =
+    equiv-iff'
+      ( continuation-Prop R (A × B))
+      ( product-Prop (continuation-Prop R A) (continuation-Prop R B))
+      ( distributive-product-continuation-modality')
+```
+
+```agda
+module _
+  {l : Level} (R : Prop l)
+  where
+
+  is-large-lawvere-tierney-topology-continuation :
+    is-large-lawvere-tierney-topology (continuation-Prop R ∘ type-Prop)
+  is-large-lawvere-tierney-topology-continuation =
+    λ where
+    .is-idempotent-is-large-lawvere-tierney-topology P →
+      ( mul-continuation , unit-continuation)
+    .preserves-unit-is-large-lawvere-tierney-topology →
+      preserves-unit-continuation-modality'
+    .preserves-conjunction-is-large-lawvere-tierney-topology P Q →
+      distributive-product-continuation-modality'
+
+  continuation-large-lawvere-tierney-topology :
+    large-lawvere-tierney-topology (l ⊔_)
+  continuation-large-lawvere-tierney-topology =
+    λ where
+    .operator-large-lawvere-tierney-topology →
+      continuation-Prop R ∘ type-Prop
+    .is-large-lawvere-tierney-topology-large-lawvere-tierney-topology →
+      is-large-lawvere-tierney-topology-continuation
+```
+
+### `A → R` is `continuation R`-stable
+
+```agda
+is-continuation-stable-exp :
+  {l1 l2 : Level} (R : Prop l1) {A : UU l2} →
+  is-modal (unit-continuation-modality (l1 ⊔ l2) R) (A → type-Prop R)
+is-continuation-stable-exp R {A} =
+  is-equiv-has-converse
+    ( function-Prop A R)
+    ( continuation-Prop R (A → type-Prop R))
+    ( _∘ unit-continuation)
+```
+
+## References
+
+{{#bibliography}}
+
+## External links
+
+- [continuation monad](https://ncatlab.org/nlab/show/continuation+monad) at
+  $n$Lab
diff --git a/src/orthogonal-factorization-systems/large-lawvere-tierney-topologies.lagda.md b/src/orthogonal-factorization-systems/large-lawvere-tierney-topologies.lagda.md
new file mode 100644
index 0000000000..b6fd6cabc1
--- /dev/null
+++ b/src/orthogonal-factorization-systems/large-lawvere-tierney-topologies.lagda.md
@@ -0,0 +1,152 @@
+# Large Lawvere–Tierney topologies
+
+```agda
+module orthogonal-factorization-systems.large-lawvere-tierney-topologies where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.lawvere-tierney-topologies
+```
+
+</details>
+
+## Idea
+
+A {#concept "Lawvere–Tierney topology" Disambiguation="on types"} on types is a
+hierarchy of maps
+
+```text
+  j : {l : Level} → Prop l → Prop (δ l)
+```
+
+that is [idempotent](foundation.idempotent-maps.md) and preserves the
+[unit type](foundation.unit-type.md) and
+[binary products](foundation.conjunction.md)
+
+```text
+  j (j P) ≃ j P      j unit ≃ unit      j (P ∧ Q) ≃ j P ∧ j Q
+```
+
+such operations give rise to a notion of `j`-sheaves of types.
+
+## Definitions
+
+### The predicate on an operator on propositions of defining a Lawvere-Tierney topology
+
+```agda
+record
+  is-large-lawvere-tierney-topology
+    {δ : Level → Level} (j : {l : Level} → Prop l → Prop (δ l)) : UUω
+  where
+  field
+    is-idempotent-is-large-lawvere-tierney-topology :
+      {l : Level} (P : Prop l) → type-Prop (j (j P) ⇔ j P)
+
+    preserves-unit-is-large-lawvere-tierney-topology :
+      type-Prop (j unit-Prop ⇔ unit-Prop)
+
+    preserves-conjunction-is-large-lawvere-tierney-topology :
+      {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
+      type-Prop (j (P ∧ Q) ⇔ j P ∧ j Q)
+
+open is-large-lawvere-tierney-topology public
+```
+
+### The large type of Lawvere-Tierney topologies
+
+```agda
+record
+  large-lawvere-tierney-topology (δ : Level → Level) : UUω
+  where
+  field
+    operator-large-lawvere-tierney-topology : {l : Level} → Prop l → Prop (δ l)
+
+    is-large-lawvere-tierney-topology-large-lawvere-tierney-topology :
+      is-large-lawvere-tierney-topology operator-large-lawvere-tierney-topology
+
+  is-idempotent-large-lawvere-tierney-topology :
+    {l : Level} (P : Prop l) →
+    type-Prop
+      ( operator-large-lawvere-tierney-topology
+        ( operator-large-lawvere-tierney-topology P) ⇔
+        operator-large-lawvere-tierney-topology P)
+  is-idempotent-large-lawvere-tierney-topology =
+    is-idempotent-is-large-lawvere-tierney-topology
+      ( is-large-lawvere-tierney-topology-large-lawvere-tierney-topology)
+
+  preserves-unit-large-lawvere-tierney-topology :
+    type-Prop (operator-large-lawvere-tierney-topology unit-Prop ⇔ unit-Prop)
+  preserves-unit-large-lawvere-tierney-topology =
+    preserves-unit-is-large-lawvere-tierney-topology
+      ( is-large-lawvere-tierney-topology-large-lawvere-tierney-topology)
+
+  preserves-conjunction-large-lawvere-tierney-topology :
+    {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
+    type-Prop
+      ( operator-large-lawvere-tierney-topology (P ∧ Q) ⇔
+        operator-large-lawvere-tierney-topology P ∧
+        operator-large-lawvere-tierney-topology Q)
+  preserves-conjunction-large-lawvere-tierney-topology =
+    preserves-conjunction-is-large-lawvere-tierney-topology
+      ( is-large-lawvere-tierney-topology-large-lawvere-tierney-topology)
+
+  type-operator-large-lawvere-tierney-topology : {l : Level} → Prop l → UU (δ l)
+  type-operator-large-lawvere-tierney-topology =
+    type-Prop ∘ operator-large-lawvere-tierney-topology
+
+open large-lawvere-tierney-topology public
+```
+
+## Examples
+
+### The identity large Lawvere-Tierney topology
+
+```agda
+is-large-lawvere-tierney-topology-id : is-large-lawvere-tierney-topology id
+is-large-lawvere-tierney-topology-id =
+  λ where
+  .is-idempotent-is-large-lawvere-tierney-topology P → id-iff
+  .preserves-unit-is-large-lawvere-tierney-topology → id-iff
+  .preserves-conjunction-is-large-lawvere-tierney-topology P Q → id-iff
+
+id-large-lawvere-tierney-topology : large-lawvere-tierney-topology (λ l → l)
+id-large-lawvere-tierney-topology =
+  λ where
+  .operator-large-lawvere-tierney-topology →
+    id
+  .is-large-lawvere-tierney-topology-large-lawvere-tierney-topology →
+    is-large-lawvere-tierney-topology-id
+```
+
+## See also
+
+- [(Small) Lawvere-Tierney topologies](orthogonal-factorization-systems.lawvere-tierney-topologies.md)
+- The
+  [continuation modalities](orthogonal-factorization-systems.continuation-modalities.md)
+  define Lawvere–Tierney topologies, and as a special case so does the
+  [double negation modality](foundation.double-negation-modality.md).
+
+## References
+
+Lawvere–Tierney topologies in the context of Homotopy Type Theory are introduced
+and studied in Chapter 6 of {{#cite Qui16}}.
+
+{{#bibliography}} {{#reference Qui16}}
+
+## External links
+
+- [Lawvere–Tierney topology](https://ncatlab.org/nlab/show/Lawvere-Tierney+topology)
+  at $n$Lab
+- [Lawvere–Tierney topology](https://en.wikipedia.org/wiki/Lawvere%E2%80%93Tierney_topology)
+  at Wikipedia
diff --git a/src/orthogonal-factorization-systems/lawvere-tierney-topologies.lagda.md b/src/orthogonal-factorization-systems/lawvere-tierney-topologies.lagda.md
new file mode 100644
index 0000000000..93fdf8ad66
--- /dev/null
+++ b/src/orthogonal-factorization-systems/lawvere-tierney-topologies.lagda.md
@@ -0,0 +1,124 @@
+# Lawvere–Tierney topologies
+
+```agda
+module orthogonal-factorization-systems.lawvere-tierney-topologies where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.logical-equivalences
+open import foundation.propositional-extensionality
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.unit-type
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A (small) {#concept "Lawvere–Tierney topology" Disambiguation="on types"} on
+types is a map
+
+```text
+  j : Prop → Prop
+```
+
+that is [idempotent](foundation.idempotent-maps.md) and preserves the
+[unit type](foundation.unit-type.md) and
+[binary products](foundation.conjunction.md)
+
+```text
+  j (j P) ≃ j P      j unit ≃ unit      j (P ∧ Q) ≃ j P ∧ j Q
+```
+
+such operations give rise to a notion of `j`-sheaves of types.
+
+## Definitions
+
+### The predicate on an operator on propositions of defining a Lawvere-Tierney topology
+
+```agda
+module _
+  {l : Level} (j : Prop l → Prop l)
+  where
+
+  is-lawvere-tierney-topology-Prop : Prop (lsuc l)
+  is-lawvere-tierney-topology-Prop =
+    product-Prop
+      ( Π-Prop (Prop l) (λ P → j (j P) ⇔ j P))
+      ( product-Prop
+        ( j (raise-unit-Prop l) ⇔ unit-Prop)
+        ( Π-Prop
+          ( Prop l)
+          ( λ P →
+            Π-Prop (Prop l) (λ Q → j (P ∧ Q) ⇔ j P ∧ j Q))))
+
+  is-lawvere-tierney-topology : UU (lsuc l)
+  is-lawvere-tierney-topology = type-Prop is-lawvere-tierney-topology-Prop
+
+  is-prop-is-lawvere-tierney-topology : is-prop is-lawvere-tierney-topology
+  is-prop-is-lawvere-tierney-topology =
+    is-prop-type-Prop is-lawvere-tierney-topology-Prop
+```
+
+### The set of Lawvere-Tierney topologies
+
+```agda
+lawvere-tierney-topology : (l : Level) → UU (lsuc l)
+lawvere-tierney-topology l = Σ (Prop l → Prop l) (is-lawvere-tierney-topology)
+
+is-set-lawvere-tierney-topology :
+  {l : Level} → is-set (lawvere-tierney-topology l)
+is-set-lawvere-tierney-topology =
+  is-set-type-subtype is-lawvere-tierney-topology-Prop (is-set-subtype)
+
+set-lawvere-tierney-topology : (l : Level) → Set (lsuc l)
+set-lawvere-tierney-topology l =
+  (lawvere-tierney-topology l , is-set-lawvere-tierney-topology)
+```
+
+## Examples
+
+### The identity function on propositions defines a Lawvere–Tierney topology
+
+```agda
+is-lawvere-tierney-topology-id :
+  (l : Level) → (is-lawvere-tierney-topology (id {A = Prop l}))
+pr1 (is-lawvere-tierney-topology-id l) P =
+  id-iff
+pr1 (pr2 (is-lawvere-tierney-topology-id l)) =
+  iff-equiv (inv-compute-raise-unit l)
+pr2 (pr2 (is-lawvere-tierney-topology-id l)) Q P =
+  id-iff
+
+id-lawvere-tierney-topology : (l : Level) → lawvere-tierney-topology l
+id-lawvere-tierney-topology l = (id , is-lawvere-tierney-topology-id l)
+```
+
+## See also
+
+- [Large Lawvere-Tierney topologies](orthogonal-factorization-systems.large-lawvere-tierney-topologies.md)
+- The
+  [continuation modalities](orthogonal-factorization-systems.continuation-modalities.md)
+  define Lawvere–Tierney topologies, and as a special case so does the
+  [double negation modality](foundation.double-negation-modality.md).
+
+## References
+
+Lawvere–Tierney topologies in the context of Homotopy Type Theory are introduced
+and studied in Chapter 6 of {{#cite Qui16}}.
+
+{{#bibliography}} {{#reference Qui16}}
+
+## External links
+
+- [Lawvere–Tierney topology](https://ncatlab.org/nlab/show/Lawvere-Tierney+topology)
+  at $n$Lab
diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
index 12bfb73be0..a4fed1c61f 100644
--- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
+++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md
@@ -30,13 +30,14 @@ open import orthogonal-factorization-systems.modal-subuniverse-induction
 
 ## Idea
 
-A **reflective subuniverse** is a [subuniverse](foundation.subuniverses.md) `P`
-together with a reflecting operator `○ : UU → UU` that take values in `P`, and a
-[modal unit](orthogonal-factorization-systems.modal-operators.md) `A → ○ A` for
-all [small types](foundation-core.small-types.md) `A`, with the property that
-the types in `P` are [local](orthogonal-factorization-systems.local-types.md) at
-the modal unit for every `A`. Hence the modal types with respect to `○` are
-precisely the types in the reflective subuniverse.
+A {{#concept "reflective subuniverse" Agda=reflective-subuniverse}} is a
+[subuniverse](foundation.subuniverses.md) `P` together with a reflecting
+operator `L : 𝒰 → 𝒰` that take values in `P`, and a
+[unit](orthogonal-factorization-systems.modal-operators.md) `A → L A` for all
+types `A` in `𝒰`, with the property that the types in `P` are
+[local](orthogonal-factorization-systems.local-types.md) at the unit for every
+`A`. Hence the local types with respect to `L` are precisely the types in the
+reflective subuniverse.
 
 ## Definitions
 
@@ -47,11 +48,11 @@ is-reflective-subuniverse :
   {l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2)
 is-reflective-subuniverse {l1} P =
   Σ ( operator-modality l1 l1)
-    ( λ ○ →
-      Σ ( unit-modality ○)
-        ( λ unit-○ →
-          ( (X : UU l1) → is-in-subuniverse P (○ X)) ×
-          ( (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-○ {Y}) X)))
+    ( λ L →
+      Σ ( unit-modality L)
+        ( λ unit-L →
+          ( (X : UU l1) → is-in-subuniverse P (L X)) ×
+          ( (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-L {Y}) X)))
 ```
 
 ```agda
diff --git a/tables/higher-modalities.md b/tables/higher-modalities.md
index 7d0b5a2e02..779b99ae76 100644
--- a/tables/higher-modalities.md
+++ b/tables/higher-modalities.md
@@ -1,9 +1,10 @@
-| Modality                          | File                                                                                                          |
-| --------------------------------- | ------------------------------------------------------------------------------------------------------------- |
-| The closed modalities             | [`orthogonal-factorization-systems.closed-modalities`](orthogonal-factorization-systems.closed-modalities.md) |
-| The double negation modality      | [`foundation.double-negation-modality`](foundation.double-negation-modality.md)                               |
-| The identity modality             | [`orthogonal-factorization-systems.identity-modality`](orthogonal-factorization-systems.identity-modality.md) |
-| The open modalities               | [`orthogonal-factorization-systems.open-modalities`](orthogonal-factorization-systems.open-modalities.md)     |
-| Raising universe level modalities | [`orthogonal-factorization-systems.raise-modalities`](orthogonal-factorization-systems.raise-modalities.md)   |
-| The truncation modalities         | [`foundation.truncation-modalities`](foundation.truncation-modalities.md)                                     |
-| The zero modality                 | [`orthogonal-factorization-systems.zero-modality`](orthogonal-factorization-systems.zero-modality.md)         |
+| Modality                          | File                                                                                                                      |
+| --------------------------------- | ------------------------------------------------------------------------------------------------------------------------- |
+| The closed modalities             | [`orthogonal-factorization-systems.closed-modalities`](orthogonal-factorization-systems.closed-modalities.md)             |
+| Continuation modalities           | [`orthogonal-factorization-systems.continuation-modalities`](orthogonal-factorization-systems.continuation-modalities.md) |
+| The double negation modality      | [`foundation.double-negation-modality`](foundation.double-negation-modality.md)                                           |
+| The identity modality             | [`orthogonal-factorization-systems.identity-modality`](orthogonal-factorization-systems.identity-modality.md)             |
+| The open modalities               | [`orthogonal-factorization-systems.open-modalities`](orthogonal-factorization-systems.open-modalities.md)                 |
+| Raising universe level modalities | [`orthogonal-factorization-systems.raise-modalities`](orthogonal-factorization-systems.raise-modalities.md)               |
+| The truncation modalities         | [`foundation.truncation-modalities`](foundation.truncation-modalities.md)                                                 |
+| The zero modality                 | [`orthogonal-factorization-systems.zero-modality`](orthogonal-factorization-systems.zero-modality.md)                     |