Martin Escardo

Properties of the type of truth values.

\begin{code}

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

module UF.SubtypeClassifier-Properties where

open import MLTT.Spartan
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Hedberg
open import UF.Lower-FunExt
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier

Ī©-is-set : funext š“¤ š“¤ ā†’ propext š“¤ ā†’ is-set (Ī© š“¤)
Ī©-is-set {š“¤} fe pe = Id-collapsibles-are-sets pc
 where
  A : (p q : Ī© š“¤) ā†’ š“¤ Ģ‡
  A p q = (p holds ā†’ q holds) Ɨ (q holds ā†’ p holds)

  A-is-prop : (p q : Ī© š“¤) ā†’ is-prop (A p q)
  A-is-prop p q = Ī£-is-prop (Ī -is-prop fe
                              (Ī» _ ā†’ holds-is-prop q))
                              (Ī» _ ā†’ Ī -is-prop fe (Ī» _ ā†’ holds-is-prop p))

  g : (p q : Ī© š“¤) ā†’ p ļ¼ q ā†’ A p q
  g p q e = (b , c)
   where
    a : p holds ļ¼ q holds
    a = ap _holds e

    b : p holds ā†’ q holds
    b = transport id a

    c : q holds ā†’ p holds
    c = transport id (a ā»Ā¹)

  h  : (p q : Ī© š“¤) ā†’ A p q ā†’ p ļ¼ q
  h p q (u , v) = Ī©-extensionality pe fe u v

  f  : (p q : Ī© š“¤) ā†’ p ļ¼ q ā†’ p ļ¼ q
  f p q e = h p q (g p q e)

  wconstant-f : (p q : Ī© š“¤) (d e : p ļ¼ q) ā†’ f p q d ļ¼ f p q e
  wconstant-f p q d e = ap (h p q) (A-is-prop p q (g p q d) (g p q e))

  pc : {p q : Ī© š“¤} ā†’ Ī£ f źž‰ (p ļ¼ q ā†’ p ļ¼ q) , wconstant f
  pc {p} {q} = (f p q , wconstant-f p q)

Ī©-extensionality-ā‰ƒ : propext š“¤
                   ā†’ funext š“¤ š“¤
                   ā†’ {p q : Ī© š“¤}
                   ā†’ ((p holds) ā†” (q holds)) ā‰ƒ (p ļ¼ q)
Ī©-extensionality-ā‰ƒ pe fe {p} {q} =
 logically-equivalent-props-are-equivalent
  (Ɨ-is-prop
    (Ī -is-prop fe (Ī» _ ā†’ holds-is-prop q))
    (Ī -is-prop fe (Ī» _ ā†’ holds-is-prop p)))
  (Ī©-is-set fe pe)
  (Ī» (f , g) ā†’ to-Ī©-ļ¼ fe (pe (holds-is-prop p) (holds-is-prop q) f g))
  (Ī» {refl ā†’ id , id})

equal-āŠ¤-ā‰ƒ : propext š“¤
          ā†’ funext š“¤ š“¤
          ā†’ (p : Ī© š“¤) ā†’ (p ļ¼ āŠ¤) ā‰ƒ (p holds)
equal-āŠ¤-ā‰ƒ {š“¤} pe fe p =
 logically-equivalent-props-are-equivalent
  (Ī©-is-set fe pe)
  (holds-is-prop p)
  (equal-āŠ¤-gives-holds p)
  (holds-gives-equal-āŠ¤ pe fe p)

equal-āŠ„-ā‰ƒ : propext š“¤
          ā†’ funext š“¤ š“¤
          ā†’ (p : Ī© š“¤) ā†’ (p ļ¼ āŠ„) ā‰ƒ Ā¬ (p holds)
equal-āŠ„-ā‰ƒ {š“¤} pe fe p =
 logically-equivalent-props-are-equivalent
 (Ī©-is-set fe pe)
 (negations-are-props (lower-funext š“¤ š“¤ fe))
 (equal-āŠ„-gives-fails p)
 (fails-gives-equal-āŠ„ pe fe p)

šŸš-to-Ī© : šŸš ā†’ Ī© š“¤
šŸš-to-Ī© ā‚€ = āŠ„
šŸš-to-Ī© ā‚ = āŠ¤

module _ (fe : funext š“¤ š“¤) (pe : propext š“¤) where

 šŸš-to-Ī©-is-embedding : is-embedding (šŸš-to-Ī© {š“¤})
 šŸš-to-Ī©-is-embedding _ (ā‚€ , p) (ā‚€ , q) = to-Ī£-ļ¼ (refl , Ī©-is-set fe pe p q)
 šŸš-to-Ī©-is-embedding _ (ā‚€ , p) (ā‚ , q) = šŸ˜-elim (āŠ„-is-not-āŠ¤ (p āˆ™ q ā»Ā¹))
 šŸš-to-Ī©-is-embedding _ (ā‚ , p) (ā‚€ , q) = šŸ˜-elim (āŠ„-is-not-āŠ¤ (q āˆ™ p ā»Ā¹))
 šŸš-to-Ī©-is-embedding _ (ā‚ , p) (ā‚ , q) = to-Ī£-ļ¼ (refl , Ī©-is-set fe pe p q)

 šŸš-to-Ī©-fiber : (p : Ī© š“¤) ā†’ fiber šŸš-to-Ī© p ā‰ƒ (Ā¬ (p holds) + p holds)
 šŸš-to-Ī©-fiber p =
  fiber (šŸš-to-Ī© {š“¤}) p           ā‰ƒāŸØ ā‰ƒ-refl _ āŸ©
  (Ī£ n źž‰ šŸš , šŸš-to-Ī© {š“¤} n ļ¼ p ) ā‰ƒāŸØ Iā‚€ āŸ©
  (āŠ„ ļ¼ p) + (āŠ¤ ļ¼ p)            ā‰ƒāŸØ Iā‚ āŸ©
  (Ā¬ (p holds) + p holds)        ā– 
    where
     Iā‚€ = alternative-+
     Iā‚ = +-cong
           (ļ¼-flip ā— equal-āŠ„-ā‰ƒ pe fe p)
           (ļ¼-flip ā— equal-āŠ¤-ā‰ƒ pe fe p)

\end{code}