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}

We can show moreover that the reflective subuniverse is replete,
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}