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}