Andrew Swan, started 12 February 2024

This is an implementation of open modalities. Like the other results
in this directory, it is covered in [1].

[1] Rijke, Shulman, Spitters, Modalities in homotopy type theory,
https://doi.org/10.23638/LMCS-16(1:2)2020

\begin{code}
{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

open import Modal.Subuniverse

open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Equiv-FunExt
open import UF.FunExt
open import UF.Subsingletons

module Modal.Open

\end{code}

Function extensionality is required for even some quite basic results
about open modalities, so we will assume it throughout.

\begin{code}

(fe : funext π€ π€)

\end{code}

There is an open modality for each proposition P. We fix such a
proposition throughout.

\begin{code}

(P : π€ Μ )
(P-is-prop : is-prop P)
where

open-unit : (A : π€ Μ ) β A β (P β A)
open-unit A a _ = a

is-open-modal : π€ Μ β π€ Μ
is-open-modal A = is-equiv (open-unit A)

open-subuniverse : subuniverse π€ π€
open-subuniverse =
is-open-modal , Ξ» A β being-equiv-is-prop'' fe _

\end{code}

The reflection has a very simple description - it just sends A to the
exponential P β A. We then need to check that it is a reflection.

\begin{code}

exponential-is-modal : (A : π€ Μ ) β is-open-modal (P β A)
exponential-is-modal A =
((Ξ» f p β f p p) ,
(Ξ» f β
dfunext
fe
(Ξ» p β dfunext fe (Ξ» q β ap (Ξ» r β f r q) (P-is-prop _ _))))) ,
(Ξ» f p β f p p) ,
(Ξ» f β refl)

exponential-is-reflection
: (A : π€ Μ )
β is-reflection open-subuniverse
A
(((P β A) , (exponential-is-modal A)) , Ξ» a _ β a)
exponential-is-reflection A B B-modal =
qinvs-are-equivs
_
((Ξ» g β prβ (prβ B-modal) β Ξ» f β g β f) ,
(Ξ» j β dfunext fe (is-retraction j)) ,
Ξ» g β dfunext fe (Ξ» a β prβ (prβ B-modal) (g a)))
where
lemma
: (j : (P β A) β B)
β (Ξ» f β (j β open-unit A β f)) βΌ (open-unit B) β j
lemma j f =
dfunext fe
(Ξ» z β ap j (dfunext fe (Ξ» z' β ap f (P-is-prop z z'))))

is-retraction
: (j : (P β A) β B)
β prβ (prβ B-modal) β (Ξ» f β (j β open-unit A β f)) βΌ j
is-retraction j f =
prβ (prβ B-modal) (j β open-unit A β f)
οΌβ¨ ap (prβ (prβ B-modal)) (lemma j f) β©
prβ (prβ B-modal) (open-unit B (j f))
οΌβ¨ prβ (prβ B-modal) (j f) β©
j f β

open-is-reflective : subuniverse-is-reflective open-subuniverse
open-is-reflective A =
(((P β A) , (exponential-is-modal A)) , (open-unit A)) ,
exponential-is-reflection A

\end{code}

using only function extensionality rather than univalence, and that it
is Ξ£-closed. This confirms that it is a modality.

\begin{code}

open-is-replete : subuniverse-is-replete open-subuniverse
open-is-replete A B e B-modal =
β-2-out-of-3-left
(prβ (βcong' fe fe e))
(β-is-equiv β e β-is-equiv B-modal)

open-is-sigma-closed : subuniverse-is-sigma-closed open-subuniverse
open-is-sigma-closed A B A-modal B-modal =
β-2-out-of-3-left
β Ξ Ξ£-distr-β β-is-equiv
β unit-equiv β-is-equiv
where
unit-equiv : Ξ£ B β (Ξ£ f κ (P β A) , ((z : P) β B (f z)))
unit-equiv =
Ξ£-bicong _ _
((open-unit A) , A-modal)
(Ξ» a β (open-unit (B a)) , (B-modal a))

\end{code}

We add a useful lemma for the absoluteness of compactness: if P is a
true proposition then the open modality is trivial, in the sense that
all types are modal.

\begin{code}

P-true-implies-all-modal
: (z : P) β (A : π€ Μ ) β is-open-modal A
P-true-implies-all-modal z A =
qinvs-are-equivs
(open-unit A)
((Ξ» f β f z) ,
((Ξ» a β refl) ,
(Ξ» f β dfunext fe (Ξ» z' β ap f (P-is-prop z z')))))

\end{code}