Tom de Jong 22nd May 2019

Various lemmas for working with partial elements of a type.
Includes an alternative partial order on the lifting of a type without relying
on full univalence.

Moreover, there are some lemmas on the Kleisli extension for the lifting monad.
In particular, (Ξ· ∘ f) β™― is pointwise equal to 𝓛̇ f.

Added 22 June 2024.
Excluded middle holds if and only if the lifting discretely adds a single point,
viz. 𝓛 X ≃ πŸ™ + X.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.Subsingletons

module Lifting.Miscelanea-PropExt-FunExt
        (𝓣 : Universe)
        (pe : propext 𝓣)
        (fe : Fun-Ext)
       where

open import Lifting.Construction 𝓣
open import Lifting.IdentityViaSIP 𝓣
open import Lifting.Miscelanea 𝓣
open import Lifting.Monad 𝓣

open import NotionsOfDecidability.DecidableClassifier

open import UF.Base
open import UF.ClassicalLogic
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Retracts
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.SubtypeClassifier hiding (βŠ₯)

\end{code}

Assuming propositional extensionality for 𝓣 and function extensionality, we can
prove that the lifting of a set is again a set.

\begin{code}

module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
       where

 open import Lifting.UnivalentPrecategory 𝓣 X

 lifting-of-set-is-set : is-set X β†’ is-set (𝓛 X)
 lifting-of-set-is-set i {l} {m} p q  = retract-of-prop r j p q
  where
   r : Ξ£ has-section
   r = (to-Σ-＝ , from-Σ-＝ , tofrom-Σ-＝)
   j : is-prop (Ξ£ (Ξ» p₁ β†’ transport (Ξ» P β†’ (P β†’ X) Γ— is-prop P)
                p₁ (prβ‚‚ l) ＝ prβ‚‚ m))
   j = Ξ£-is-prop
        (identifications-with-props-are-props pe fe (is-defined m)
         (being-defined-is-prop m) (is-defined l))
        (Ξ» d β†’ Γ—-is-set (Ξ -is-set fe Ξ» _ β†’ i)
                        (props-are-sets (being-prop-is-prop fe)))

 \end{code}

 We prefer to work with βŠ‘' as it yields identifications, which can be transported
 and allow for equational reasoning with ＝⟨ ⟩.
 Moreover, it has the right universe level for use in the Scott model of PCF.

 This duplicates some material from LiftingUnivalentPrecategory. However, we only
 assume propositional extensionality and function extensionality here. We do not
 rely on full univalence.

 \begin{code}

 _βŠ‘'_ : (l m : 𝓛 X) β†’ 𝓀 βŠ” 𝓣 ⁺ Μ‡
 l βŠ‘' m = is-defined l β†’ l ＝ m

 βŠ‘-to-βŠ‘' : {l m : 𝓛 X} β†’ l βŠ‘ m β†’ l βŠ‘' m
 βŠ‘-to-βŠ‘' {l} {m} a d = βŠ‘-anti pe fe fe (a , b) where
  b : m βŠ‘ l
  b = c , v where
   c : is-defined m β†’ is-defined l
   c = Ξ» _ β†’ d
   v : (e : is-defined m) β†’ value m e ＝ value l d
   v e = value m e         ＝⟨ ap (value m)
                             (being-defined-is-prop m e (pr₁ a d)) ⟩
         value m (pr₁ a d) ＝⟨ g ⁻¹ ⟩
         value l d         ∎ where
    h : is-defined l β†’ is-defined m
    h = pr₁ a
    g : value l d ＝ value m (pr₁ a d)
    g = prβ‚‚ a d

 βŠ‘'-to-βŠ‘ : {l m : 𝓛 X} β†’ l βŠ‘' m β†’ l βŠ‘ m
 βŠ‘'-to-βŠ‘ {l} {m} a = ⌜ e ⌝⁻¹ g where
  e : (l βŠ‘ m) ≃ (is-defined l β†’ l βŠ‘ m)
  e = βŠ‘-open fe fe l m
  g : is-defined l β†’ l βŠ‘ m
  g d = transport (_βŠ‘_ l) (a d) (𝓛-id l)

 βŠ‘'-is-reflexive : {l : 𝓛 X} β†’ l βŠ‘' l
 βŠ‘'-is-reflexive {l} d = refl

 βŠ‘'-is-transitive : {l m n : 𝓛 X} β†’ l βŠ‘' m β†’ m βŠ‘' n β†’ l βŠ‘' n
 βŠ‘'-is-transitive {l} {m} {n} a b d = l ＝⟨ a d ⟩
                                      m ＝⟨ b (＝-to-is-defined (a d) d) ⟩
                                      n ∎

 βŠ‘'-is-antisymmetric : {l m : 𝓛 X} β†’ l βŠ‘' m β†’ m βŠ‘' l β†’ l ＝ m
 βŠ‘'-is-antisymmetric a b = βŠ‘-anti pe fe fe (βŠ‘'-to-βŠ‘ a , βŠ‘'-to-βŠ‘ b)

 βŠ‘'-prop-valued : is-set X β†’ {l m : 𝓛 X} β†’ is-prop (l βŠ‘' m)
 βŠ‘'-prop-valued s {l} {m} =
  Ξ -is-prop fe Ξ» (d : is-defined l) β†’ lifting-of-set-is-set s

 not-defined-βŠ₯-＝ : {l : 𝓛 X} β†’ Β¬ (is-defined l) β†’ l ＝ βŠ₯
 not-defined-βŠ₯-＝ {l} nd =
  βŠ‘-anti pe fe fe
         (((Ξ» d β†’ 𝟘-elim (nd d)) , (Ξ» d β†’ 𝟘-elim (nd d))) ,
         𝟘-elim , 𝟘-induction)

 is-defined-Ξ·-＝ : {l : 𝓛 X} (d : is-defined l) β†’ l ＝ Ξ· (value l d)
 is-defined-η-＝ {l} d =
  βŠ‘-to-βŠ‘' ((Ξ» _ β†’ ⋆) , Ξ» (e : is-defined l) β†’ value-is-constant l e d) d

 ＝-to-⋍ : {l m : 𝓛 X} β†’ l ＝ m β†’ l ⋍ m
 ＝-to-⋍ {l} {m} refl = ≃-refl (is-defined l) , refl

 ⋍-to-＝ : {l m : 𝓛 X} β†’ l ⋍ m β†’ l ＝ m
 ⋍-to-＝ {l} {m} (deq , veq) = βŠ‘-anti pe fe fe (a , b)
  where
   a : l βŠ‘ m
   a = ⌜ deq ⌝ , happly veq
   b : m βŠ‘ l
   b = (⌜ deq ⌝⁻¹ , h)
    where
     h : (d : is-defined m) β†’ value m d ＝ value l (⌜ deq ⌝⁻¹ d)
     h d = value m d  ＝⟨ value-is-constant m d d' ⟩
           value m d' ＝⟨ (happly veq e)⁻¹ ⟩
           value l e  ∎
      where
       e : is-defined l
       e = ⌜ deq ⌝⁻¹ d
       d' : is-defined m
       d' = ⌜ deq ⌝ e

module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         {π“₯ : Universe}
         {Y : π“₯ Μ‡ }
       where

 β™―-is-defined : (f : X β†’ 𝓛 Y) (l : 𝓛 X) β†’ is-defined ((f β™―) l) β†’ is-defined l
 β™―-is-defined f l = pr₁

 β™―-on-total-element : (f : X β†’ 𝓛 Y) {l : 𝓛 X} (d : is-defined l)
                    β†’ (f β™―) l ＝ f (value l d)
 β™―-on-total-element f {l} d =
  (f β™―) l               ＝⟨ ap (f β™―) (is-defined-Ξ·-＝ d) ⟩
  (f β™―) (Ξ· (value l d)) ＝⟨ ⋍-to-＝ (Kleisli-Law₁ f (value l d)) ⟩
  f (value l d)         ∎

 open import Lifting.UnivalentPrecategory 𝓣 Y

 𝓛̇-β™―-∼ : (f : X β†’ Y) β†’ (Ξ· ∘ f) β™― ∼ 𝓛̇ f
 𝓛̇-β™―-∼ f l = βŠ‘-anti pe fe fe (a , b)
  where
   a : ((Ξ· ∘ f) β™―) l βŠ‘ (𝓛̇ f) l
   a = p , q
    where
     p : is-defined (((Ξ· ∘ f) β™―) l) β†’ is-defined (𝓛̇ f l)
     p = β™―-is-defined (Ξ· ∘ f) l
     q : (d : is-defined (((Ξ· ∘ f) β™―) l))
       β†’ value (((Ξ· ∘ f) β™―) l) d ＝ value (𝓛̇ f l) (β™―-is-defined (Ξ· ∘ f) l d)
     q d = refl
   b : (𝓛̇ f) l βŠ‘ ((Ξ· ∘ f) β™―) l
   b = r , s
    where
     r : is-defined (𝓛̇ f l) β†’ is-defined (((Ξ· ∘ f) β™―) l)
     r d = d , ⋆
     s : (d : is-defined (𝓛̇ f l))
       β†’ value (𝓛̇ f l) d ＝ value (((Ξ· ∘ f) β™―) l) (r d)
     s d = refl

\end{code}

Added 22 June 2024.
Excluded middle holds if and only if the lifting discretely adds a single point,
viz. 𝓛 X ≃ πŸ™ + X.

\begin{code}

lifting-of-πŸ™-is-Ξ© : 𝓛 (πŸ™{𝓀}) ≃ Ξ© 𝓣
lifting-of-πŸ™-is-Ξ© =
 𝓛 πŸ™                         β‰ƒβŸ¨ Ξ£-cong (Ξ» P β†’ Γ—-cong (β†’πŸ™ fe) π•šπ••) ⟩
 (Ξ£ P κž‰ 𝓣 Μ‡ , πŸ™ Γ— is-prop P) β‰ƒβŸ¨ Ξ£-cong (Ξ» P β†’ πŸ™-lneutral) ⟩
 Ξ© 𝓣                         β– 

EM-gives-classical-lifting : (X : 𝓀 Μ‡ ) β†’ EM 𝓣 β†’ 𝓛 X ≃ (πŸ™{𝓀} + X)
EM-gives-classical-lifting {𝓀} X em =
 𝓛 X                                 β‰ƒβŸ¨ I   ⟩
 (Ξ£ P κž‰ 𝓣 Μ‡ , is-prop P Γ— (P β†’ X))   β‰ƒβŸ¨ II  ⟩
 (Ξ£ P κž‰ Ξ© 𝓣 , (P holds β†’ X))         β‰ƒβŸ¨ III ⟩
 (Ξ£ b κž‰ 𝟚 , (ΞΉ b holds β†’ X))         β‰ƒβŸ¨ IV  ⟩
 (Ξ£ b κž‰ πŸ™ + πŸ™ , (ΞΉ (e b) holds β†’ X)) β‰ƒβŸ¨ V   ⟩
 (πŸ™ Γ— (𝟘 β†’ X)) + (πŸ™ Γ— (πŸ™ β†’ X))       β‰ƒβŸ¨ VI  ⟩
 (𝟘 β†’ X) + (πŸ™ β†’ X)                   β‰ƒβŸ¨ VII ⟩
 (πŸ™ + X)                             β– 
  where
   ΞΉ : 𝟚 β†’ Ξ© 𝓣
   ΞΉ = inclusion-of-booleans
   e : πŸ™{𝓀} + πŸ™{𝓀} β†’ 𝟚
   e = ⌜ 𝟚-≃-πŸ™+πŸ™ ⌝⁻¹

   I   = Ξ£-cong (Ξ» _ β†’ Γ—-comm)
   II  = ≃-sym Ξ£-assoc
   III = ≃-sym (Ξ£-change-of-variable-≃ _
                 (EM-gives-𝟚-is-the-type-of-propositions fe pe em))
   IV  = ≃-sym (Ξ£-change-of-variable-≃ _ (≃-sym 𝟚-≃-πŸ™+πŸ™))
   V   = ≃-sym (Ξ£+-split πŸ™ πŸ™ (Ξ» b β†’ ΞΉ (e b) holds β†’ X))
   VI  = +-cong πŸ™-lneutral πŸ™-lneutral
   VII = +-cong (≃-sym (πŸ˜β†’ fe)) (≃-sym (πŸ™β†’ fe))

classical-lifting-of-πŸ™-gives-EM : 𝓛 (πŸ™{𝓀}) ≃ (πŸ™{𝓀} + πŸ™{𝓀}) β†’ EM 𝓣
classical-lifting-of-πŸ™-gives-EM e =
 𝟚-is-the-type-of-propositions-gives-EM fe pe I
  where
   I = 𝟚     β‰ƒβŸ¨ 𝟚-≃-πŸ™+πŸ™ ⟩
       πŸ™ + πŸ™ β‰ƒβŸ¨ ≃-sym e ⟩
       𝓛 πŸ™   β‰ƒβŸ¨ lifting-of-πŸ™-is-Ξ© ⟩
       Ξ© 𝓣   β– 

classical-lifting-gives-EM : ((X : 𝓀 Μ‡ ) β†’ 𝓛 X ≃ πŸ™{𝓀} + X) β†’ EM 𝓣
classical-lifting-gives-EM h = classical-lifting-of-πŸ™-gives-EM (h πŸ™)

\end{code}