Continuation modalities and Lawvere–Tierney topologies (#1157)

Defines continuation modalities as a generalization of the double
negation modality, and shows they define Lavwere–Tierney topologies on
types. It also improves term usage in the file about reflective
subuniverses.

---------

Co-authored-by: Egbert Rijke <[email protected]>

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},

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

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

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
+```

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

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

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