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)

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}