Jon Sterling, started 27th Sep 2022
Andrew Swan, 7th Februrary 2024, definition of Ξ£-closed subuniverse added

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Modal.Subuniverse where

open import MLTT.Spartan
open import UF.Subsingletons
open import UF.Equiv
open import UF.Univalence

subuniverse
 : (𝓀 π“₯ : Universe)
 β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
subuniverse 𝓀 π“₯ =
 Ξ£ P κž‰ (𝓀 Μ‡ β†’ π“₯ Μ‡ ),
 Ξ  A κž‰ 𝓀 Μ‡ ,
 is-prop (P A)

subuniverse-contains
 : subuniverse 𝓀 π“₯
 β†’ 𝓀 Μ‡
 β†’ π“₯ Μ‡
subuniverse-contains P A =
 pr₁ P A

subuniverse-member
 : subuniverse 𝓀 π“₯
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
subuniverse-member P =
 Ξ£ (subuniverse-contains P)

reflection-candidate
 : subuniverse 𝓀 π“₯
 β†’ 𝓀 Μ‡
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
reflection-candidate P A =
 Ξ£ A' κž‰ subuniverse-member P ,
 (A β†’ pr₁ A')

is-reflection
 : (P : subuniverse 𝓀 π“₯)
 β†’ (A : 𝓀 Μ‡ )
 β†’ reflection-candidate P A
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
is-reflection P A (A' , Ξ·) =
 (B : _)
 β†’ subuniverse-contains P B
 β†’ is-equiv Ξ» (f : pr₁ A' β†’ B) β†’ f ∘ Ξ·

subuniverse-reflects
 : subuniverse 𝓀 π“₯
 β†’ 𝓀 Μ‡
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
subuniverse-reflects P A =
 Ξ£ A' κž‰ reflection-candidate P A ,
 is-reflection P A A'

subuniverse-is-reflective
 : subuniverse 𝓀 π“₯
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
subuniverse-is-reflective P =
 Ξ  (subuniverse-reflects P)

subuniverse-is-replete
 : subuniverse 𝓀 π“₯
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
subuniverse-is-replete P =
 (A B : _)
 β†’ A ≃ B
 β†’ subuniverse-contains P B
 β†’ subuniverse-contains P A

univalence-implies-subuniverse-is-replete
 : (ua : is-univalent 𝓀)
 β†’ (P : subuniverse 𝓀 π“₯)
 β†’ subuniverse-is-replete P
univalence-implies-subuniverse-is-replete ua P A B e =
 transport⁻¹
  (subuniverse-contains P)
  (eqtoid ua A B e)

subuniverse-is-sigma-closed
 : (P : subuniverse 𝓀 π“₯)
 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
subuniverse-is-sigma-closed P =
 (A : _) β†’
 (B : A β†’ _) β†’
 pr₁ P A β†’
 ((a : A) β†’ pr₁ P (B a)) β†’
 pr₁ P (Ξ£ B)
\end{code}