Continuation modalities and Lawvere–Tierney topologies

references.bib

@@ -475,6 +475,20 @@ @online{OEIS
   url          = {https://oeis.org/}
 }
 
+@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

@@ -84,6 +84,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,197 @@
+# Continuations
+
+```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`,
+{{#concept "continuations" Disambiguation="on a type" Agda=continuation}} on `R`
+
+```text
+  A ↦ ((A → R) → R)
+```
+
+defines a monad on types.
+
+## Definitions
+
+### The continuation operator
+
+```agda
+continuation :
+  {l1 l2 : Level} (R : UU l1) (A : UU l2) → UU (l1 ⊔ l2)
+continuation R A = ((A → R) → R)
+```
+
+### The functorial action on maps of continuations
+
+```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 operation
+
+```agda
+unit-continuation :
+  {l1 l2 : Level} {R : UU l1} {A : UU l2} → A → continuation R A
+unit-continuation = ev
+```
+
+### Maps into continuations extend along the unit
+
+Every `f` as in the following diagram extends 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 on continuations
+
+```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 continuations
+
+```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
+```
+
+### Continuations on propositions are 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 continuations at 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 continuations at 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.extensions-double-lifts-families-of-elements public
 open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public
@@ -29,6 +30,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