Martin Escardo

In univalent logic, as opposed to Curry-Howard logic, a proposition is
a prop or a type such that any two of its elements are
identified.

https://www.newton.ac.uk/files/seminar/20170711100011001-1009756.pdf
https://unimath.github.io/bham2017/uf.pdf

About (sub)singletons using function extensionality.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module UF.Subsingletons-FunExt where

open import MLTT.Spartan

open import UF.Base
open import UF.Subsingletons renaming (⊤Ω to ⊤ ; ⊥Ω to ⊥)
open import UF.FunExt
open import UF.Lower-FunExt
open import UF.LeftCancellable
open import UF.Retracts

Π-is-prop : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
→ ((x : X) → is-prop (A x))
→ is-prop (Π A)
Π-is-prop fe i f g = dfunext fe (λ x → i x (f x) (g x))

Π-is-prop' : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
→ ((x : X) → is-prop (A x))
→ is-prop ({x : X} → A x)
Π-is-prop' fe {X} {A} i = retract-of-prop retr (Π-is-prop fe i)
where
retr : retract ({x : X} → A x) of Π A
retr = (λ f {x} → f x) , (λ g x → g {x}) , (λ x → refl)

Π-is-singleton : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
→ ((x : X) → is-singleton (A x))
→ is-singleton (Π A)
Π-is-singleton fe i = (λ x → pr₁ (i x)) ,
(λ f → dfunext fe (λ x → pr₂ (i x) (f x)))

being-prop-is-prop : {X : 𝓤 ̇ }
→ funext 𝓤 𝓤
→ is-prop (is-prop X)
being-prop-is-prop {𝓤} {X} fe f g = c₁
where
l : is-set X
l = props-are-sets f

c : (x y : X) → f x y ＝ g x y
c x y = l (f x y) (g x y)

c₀ : (x : X) → f x ＝ g x
c₀ x = dfunext fe (c x)

c₁ : f ＝ g
c₁  = dfunext fe c₀

⇔-is-prop : {X : 𝓤 ̇  } {Y : 𝓥 ̇  }
→ funext 𝓤 𝓥
→ funext 𝓥 𝓤
→ is-prop X
→ is-prop Y
→ is-prop (X ⇔ Y)
⇔-is-prop fe fe' X-is-prop Y-is-prop = ×-is-prop
(Π-is-prop fe  (λ _ → Y-is-prop))
(Π-is-prop fe' (λ _ → X-is-prop))

\end{code}

The following means that propositions are h-isolated elements of type
universes:

\begin{code}

identifications-with-props-are-props : propext 𝓤
→ funext 𝓤 𝓤
→ (P : 𝓤 ̇ )
→ is-prop P
→ (X : 𝓤 ̇ ) → is-prop (X ＝ P)
identifications-with-props-are-props {𝓤} pe fe P i = γ
where
f : (X : 𝓤 ̇ ) → X ＝ P → is-prop X × (X ⇔ P)
f X refl = i , (id , id)

g : (X : 𝓤 ̇ ) → is-prop X × (X ⇔ P) → X ＝ P
g X (l , φ , γ) = pe l i φ γ

j : (X : 𝓤 ̇ ) → is-prop (is-prop X × (X ⇔ P))
j X = ×-prop-criterion ( (λ _ → being-prop-is-prop fe)
, (λ l → ⇔-is-prop fe fe l i))

k : (X : 𝓤 ̇ ) → wconstant (g X ∘ f X)
k X p q = ap (g X) (j X (f X p) (f X q))

γ : (X : 𝓤 ̇ ) → is-prop (X ＝ P)
γ = local-hedberg' P (λ X → g X ∘ f X , k X)

being-singleton-is-prop : funext 𝓤 𝓤 → {X : 𝓤 ̇ } → is-prop (is-singleton X)
being-singleton-is-prop fe {X} (x , φ) (y , γ) = δ
where
isp : is-prop X
isp = singletons-are-props (y , γ)

iss : is-set X
iss = props-are-sets isp

δ : x , φ ＝ y , γ
δ = to-Σ-＝ (φ y , dfunext fe λ z → iss {y} {z} _ _)

∃!-is-prop : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
→ funext (𝓤 ⊔ 𝓥) (𝓤 ⊔ 𝓥)
→ is-prop (∃! A)
∃!-is-prop fe = being-singleton-is-prop fe

Π-is-set : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
→ ((x : X) → is-set (A x))
→ is-set (Π A)
Π-is-set {𝓤} {𝓥} fe {X} {A} isa {f} {g} = b
where
a : is-prop (f ∼ g)
a p q = dfunext fe λ x → isa x (p x) (q x)

b : is-prop (f ＝ g)
b = left-cancellable-reflects-is-prop
happly
(section-lc happly (pr₂ (fe f g)))
a

\end{code}

The crucial lemma of the following proof is being-set-is-prop'. The
rest of the code is to deal with implicit arguments in conjunction
with function extensionality. The solution is not ideal. Ideally,
functions with implicit parameters should be the same as their
versions with explicit parameters.

\begin{code}

being-set-is-prop : funext 𝓤 𝓤 → {X : 𝓤 ̇ } → is-prop (is-set X)
being-set-is-prop {𝓤} fe {X} = h
where
is-set' : 𝓤 ̇ → 𝓤 ̇
is-set' X = (x y : X) → is-prop (x ＝ y)

being-set-is-prop' : {X : 𝓤 ̇ } → funext 𝓤 𝓤 → is-prop (is-set' X)
being-set-is-prop' fe = Π-is-prop fe
(λ x → Π-is-prop fe
(λ y → being-prop-is-prop fe))

f : {X : 𝓤 ̇ } → is-set' X → is-set X
f s {x} {y} = s x y

g : {X : 𝓤 ̇ } → is-set X → is-set' X
g s x y = s {x} {y}

h : is-prop (is-set X)
h = subtypes-of-props-are-props' g (ap f) (being-set-is-prop' fe)

negations-are-props : {X : 𝓤 ̇ } → funext 𝓤 𝓤₀ → is-prop (¬ X)
negations-are-props fe = Π-is-prop fe (λ x → 𝟘-is-prop)

decidability-of-prop-is-prop : funext 𝓤 𝓤₀
→ {P : 𝓤 ̇ }
→ is-prop P
→ is-prop (P + ¬ P)
decidability-of-prop-is-prop fe₀ i = sum-of-contradictory-props
i
(negations-are-props fe₀)
(λ p u → u p)

Ω-extensionality : funext 𝓤 𝓤
→ propext 𝓤
→ {p q : Ω 𝓤}
→ (p holds → q holds)
→ (q holds → p holds)
→ p ＝ q
Ω-extensionality {𝓤} fe pe {p} {q} f g =
to-Σ-＝
(pe (holds-is-prop p) (holds-is-prop q) f g ,
being-prop-is-prop fe _ _)

Ω-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 fe pe 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)

powersets-are-sets'' : funext 𝓤 (𝓥 ⁺)
→ funext 𝓥 𝓥
→ propext 𝓥
→ {A : 𝓤 ̇ } → is-set (A → Ω 𝓥)
powersets-are-sets'' fe fe' pe = Π-is-set fe (λ x → Ω-is-set fe' pe)

powersets-are-sets : funext 𝓥 (𝓥 ⁺)
→ propext 𝓥
→ {A : 𝓥 ̇ } → is-set (A → Ω 𝓥)
powersets-are-sets {𝓥} fe = powersets-are-sets'' fe (lower-funext 𝓥 (𝓥 ⁺) fe)

empty-types-are-props : {X : 𝓤 ̇ } → ¬ X → is-prop X
empty-types-are-props f x = 𝟘-elim (f x)

equal-𝟘-is-empty : {X : 𝓤 ̇ } → X ＝ 𝟘 → ¬ X
equal-𝟘-is-empty e x = 𝟘-elim (transport id e x)

empty-types-are-＝-𝟘 : funext 𝓤 𝓤₀ → propext 𝓤 → {X : 𝓤 ̇ } → ¬ X → X ＝ 𝟘
empty-types-are-＝-𝟘 fe pe f = pe (empty-types-are-props f)
𝟘-is-prop
(λ x → 𝟘-elim (f x))
𝟘-elim

not : funext 𝓤 𝓤₀ → Ω 𝓤 → Ω 𝓤
not fe (P , i) = (¬ P , negations-are-props fe)

equal-⊤-is-true : (P : 𝓤 ̇ ) (i : is-prop P) → (P , i) ＝ ⊤ → P
equal-⊤-is-true P hp r = f ⋆
where
s : 𝟙 ＝ P
s = (ap pr₁ r)⁻¹

f : 𝟙 → P
f = transport id s

\end{code}

TODO. In the following, rather than using a P and i, use a p = (P , i) in Ω 𝓤.

\begin{code}

holds-gives-equal-𝟙 : propext 𝓤 → (P : 𝓤 ̇ ) → is-prop P → P → P ＝ 𝟙
holds-gives-equal-𝟙 pe P i p = pe i 𝟙-is-prop unique-to-𝟙 (λ _ → p)

true-is-equal-⊤ : propext 𝓤
→ funext 𝓤 𝓤
→ (P : 𝓤 ̇ ) (i : is-prop P)
→ P → (P , i) ＝ ⊤
true-is-equal-⊤ pe fe P i p = to-Σ-＝ (holds-gives-equal-𝟙 pe P i p ,
being-prop-is-prop fe _ _)

holds-gives-equal-⊤ : propext 𝓤 → funext 𝓤 𝓤 → (p : Ω 𝓤) → p holds → p ＝ ⊤
holds-gives-equal-⊤ pe fe (P , i) = true-is-equal-⊤ pe fe P i

equal-𝟙-gives-holds : (P : 𝓤 ̇ ) → P ＝ 𝟙 → P
equal-𝟙-gives-holds P r = Idtofun (r ⁻¹) ⋆

equal-⊤-gives-holds : (p : Ω 𝓤) → p ＝ ⊤ → p holds
equal-⊤-gives-holds p r = equal-𝟙-gives-holds (p holds) (ap pr₁ r)

not-𝟘-is-𝟙 : funext 𝓤 𝓤₀
→ propext 𝓤
→ (¬ 𝟘) ＝ 𝟙
not-𝟘-is-𝟙 fe pe = pe (negations-are-props fe)
𝟙-is-prop
(λ _ → ⋆)
(λ _ z → 𝟘-elim z)

equal-⊥-gives-not-equal-⊤ : (fe : Fun-Ext)
(pe : propext 𝓤)
(p : Ω 𝓤)
→ p ＝ ⊥
→ not fe p ＝ ⊤
equal-⊥-gives-not-equal-⊤ fe pe p r = γ
where
s : p holds ＝ 𝟘
s = ap _holds r

t : ¬ (p holds) ＝ 𝟙
t = ap ¬_ s ∙ not-𝟘-is-𝟙 fe pe

γ : not fe p ＝ ⊤
γ = to-subtype-＝ (λ _ → being-prop-is-prop fe) t

false-is-equal-⊥ : propext 𝓤
→ funext 𝓤 𝓤
→ (P : 𝓤 ̇ ) (i : is-prop P)
→ ¬ P → (P , i) ＝ ⊥
false-is-equal-⊥ pe fe P i f =
to-Σ-＝
(pe i 𝟘-is-prop (λ p → 𝟘-elim (f p)) 𝟘-elim ,
being-prop-is-prop fe _ _)

not-equal-⊤-gives-equal-⊥ : (fe : Fun-Ext)
(pe : propext 𝓤)
(p : Ω 𝓤)
→ not fe p ＝ ⊤
→ p ＝ ⊥
not-equal-⊤-gives-equal-⊥ fe pe p r = γ
where
f : (not fe p) holds
f = Idtofun (ap _holds r ⁻¹) ⋆

t : p holds ＝ 𝟘
t = empty-types-are-＝-𝟘 fe pe f

γ : p ＝ ⊥
γ = to-subtype-＝ (λ _ → being-prop-is-prop fe) t

Ω-ext : propext 𝓤
→ funext 𝓤 𝓤
→ {p q : Ω 𝓤}
→ (p ＝ ⊤ → q ＝ ⊤)
→ (q ＝ ⊤ → p ＝ ⊤)
→ p ＝ q

Ω-ext pe fe {P , i} {Q , j} f g = III
where
I : P → Q
I x = equal-⊤-is-true Q j (f (true-is-equal-⊤ pe fe P i x))

II : Q → P
II y = equal-⊤-is-true P i (g (true-is-equal-⊤ pe fe Q j y))

III : P , i ＝ Q , j
III = to-Σ-＝ (pe i j I II , being-prop-is-prop fe _ _ )

Ω-discrete-gives-EM : funext 𝓤 𝓤
→ propext 𝓤
→ ((p q : Ω 𝓤) → is-decidable (p ＝ q))
→ (P : 𝓤 ̇ ) → is-prop P → P + ¬ P
Ω-discrete-gives-EM {𝓤} fe pe δ P i = f (δ p q)
where
p q : Ω 𝓤
p = (P , i)
q = (𝟙 , 𝟙-is-prop)

f : is-decidable (p ＝ q) → P + ¬ P
f (inl e) = inl (equal-𝟙-gives-holds P (ap pr₁ e))
f (inr ν) = inr (λ (x : P) → ν (to-subtype-＝
(λ _ → being-prop-is-prop fe)
(holds-gives-equal-𝟙 pe P i x)))
\end{code}

Without excluded middle, we have that:

\begin{code}

no-truth-values-other-than-⊥-or-⊤ : funext 𝓤 𝓤
→ propext 𝓤
→ ¬ (Σ p ꞉ Ω 𝓤 , (p ≠ ⊥) × (p ≠ ⊤))
no-truth-values-other-than-⊥-or-⊤ fe pe ((P , i) , (f , g)) = φ u
where
u : ¬ P
u p = g l
where
l : (P , i) ＝ ⊤
l = Ω-extensionality fe pe unique-to-𝟙 (λ _ → p)

φ : ¬¬ P
φ u = f l
where
l : (P , i) ＝ ⊥
l = Ω-extensionality fe pe (λ p → 𝟘-elim (u p)) unique-from-𝟘

no-three-distinct-propositions : funext 𝓤 𝓤
→ propext 𝓤
→ ¬ has-three-distinct-points (Ω 𝓤)
no-three-distinct-propositions fe pe ((p , q , r) , u , v , w) = XI
where
I : p ≠ ⊥
I a = no-truth-values-other-than-⊥-or-⊤ fe pe (q , II , III)
where
II : q ≠ ⊥
II b = u (a ∙ b ⁻¹)

III : q ≠ ⊤
III c = no-truth-values-other-than-⊥-or-⊤ fe pe (r , IV , V)
where
IV : r ≠ ⊥
IV d = w (d ∙ a ⁻¹)

V : r ≠ ⊤
V e = v (c ∙ e ⁻¹)

VI : p ≠ ⊤
VI a = no-truth-values-other-than-⊥-or-⊤ fe pe (q , VII , X)
where
VII : q ≠ ⊥
VII b = no-truth-values-other-than-⊥-or-⊤ fe pe (r , VIII , IX)
where
VIII : r ≠ ⊥
VIII c = v (b ∙ c ⁻¹)

IX : r ≠ ⊤
IX d = w (d ∙ a ⁻¹)

X : q ≠ ⊤
X e = u (a ∙ e ⁻¹)

XI : 𝟘
XI = no-truth-values-other-than-⊥-or-⊤ fe pe (p , I , VI)

\end{code}

The above function was added 19th March 2021.

The above implies that if Fin n is embedded in Ω 𝓤, then n ≤ 2. That
is, every finite subset of Ω has at most two elements. See the module
Fin.lagda.

In the above and in the following, 𝟘-elim is used to coerce from 𝟘 {𝓤}
to 𝟘 {𝓤₀} as this is where negations take values in.

\begin{code}

⊥-is-not-⊤ : ⊥ {𝓤} ≠ ⊤ {𝓤}
⊥-is-not-⊤ b = 𝟘-elim (𝟘-is-not-𝟙 (ap _holds b))

\end{code}

Sometimes it is convenient to work with the type of true propositions,
which is a singleton and hence a subsingleton. But we will leave this
type nameless:

\begin{code}

𝟙-is-true-props-center : funext 𝓤 𝓤
→ propext 𝓤
→ (σ : Σ P ꞉ 𝓤 ̇ , is-prop P × P) → (𝟙 , 𝟙-is-prop , ⋆) ＝ σ
𝟙-is-true-props-center fe pe = γ
where
φ : ∀ P → is-prop (is-prop P × P)
φ P (i , p) = ×-is-prop (being-prop-is-prop fe) i (i , p)

γ : ∀ σ → (𝟙 , 𝟙-is-prop , ⋆) ＝ σ
γ (P , i , p) = to-subtype-＝ φ s
where
s : 𝟙 ＝ P
s = pe 𝟙-is-prop i (λ _ → p) (λ _ → ⋆)

the-true-props-form-a-singleton-type : funext 𝓤 𝓤
→ propext 𝓤
→ is-singleton (Σ P ꞉ 𝓤 ̇ , is-prop P × P)
the-true-props-form-a-singleton-type fe pe = (𝟙 , 𝟙-is-prop , ⋆) ,
𝟙-is-true-props-center fe pe

the-true-props-form-a-prop : funext 𝓤 𝓤
→ propext 𝓤
→ is-prop (Σ P ꞉ 𝓤 ̇ , is-prop P × P)
the-true-props-form-a-prop fe pe =
singletons-are-props (the-true-props-form-a-singleton-type fe pe)

\end{code}

Added 16th June 2020. (Should have added this ages ago to avoid
boiler-plate code.)

\begin{code}

Π₂-is-prop : Fun-Ext
→ {X : 𝓤 ̇ }
{Y : X → 𝓥 ̇ }
{Z : (x : X) → Y x → 𝓦 ̇ }
→ ((x : X) (y : Y x) → is-prop (Z x y))
→ is-prop ((x : X) (y : Y x) → Z x y)
Π₂-is-prop fe i = Π-is-prop fe (λ x → Π-is-prop fe (i x))

Π₃-is-prop : Fun-Ext
→ {X : 𝓤 ̇ }
{Y : X → 𝓥 ̇ }
{Z : (x : X) → Y x → 𝓦 ̇ }
{T : (x : X) (y : Y x) → Z x y → 𝓣 ̇ }
→ ((x : X) (y : Y x) (z : Z x y) → is-prop (T x y z))
→ is-prop ((x : X) (y : Y x) (z : Z x y) → T x y z)
Π₃-is-prop fe i = Π-is-prop fe (λ x → Π₂-is-prop fe (i x))

Π₄-is-prop : Fun-Ext
→ {𝓥₀ 𝓥₁ 𝓥₂ 𝓥₃ : Universe}
{A : 𝓤 ̇ }
{B : A → 𝓥₀ ̇ }
{C : (a : A) → B a → 𝓥₁ ̇ }
{D : (a : A) (b : B a) → C a b → 𝓥₂ ̇ }
{E : (a : A) (b : B a) (c : C a b) → D a b c → 𝓥₃ ̇ }
→ ((a : A) (b : B a) (c : C a b) (d : D a b c) → is-prop (E a b c d))
→ is-prop ((a : A) (b : B a) (c : C a b) (d : D a b c) → E a b c d)
Π₄-is-prop fe i = Π-is-prop fe (λ x → Π₃-is-prop fe (i x))

Π₅-is-prop : Fun-Ext
→ {𝓥₀ 𝓥₁ 𝓥₂ 𝓥₃ 𝓥₄ : Universe}
{A : 𝓤 ̇ }
{B : A → 𝓥₀ ̇ }
{C : (a : A) → B a → 𝓥₁ ̇ }
{D : (a : A) (b : B a) → C a b → 𝓥₂ ̇ }
{E : (a : A) (b : B a) (c : C a b) → D a b c → 𝓥₃ ̇ }
{F : (a : A) (b : B a) (c : C a b) (d : D a b c) → E a b c d → 𝓥₄ ̇ }
→ ((a : A) (b : B a) (c : C a b) (d : D a b c) (e : E a b c d) → is-prop (F a b c d e))
→ is-prop ((a : A) (b : B a) (c : C a b) (d : D a b c) (e : E a b c d) → F a b c d e)
Π₅-is-prop fe i = Π-is-prop fe (λ x → Π₄-is-prop fe (i x))

Π₂-is-prop' : Fun-Ext
→ {X : 𝓤 ̇ }
{Y : X → 𝓥 ̇ }
{Z : (x : X) → Y x → 𝓦 ̇ }
→ ((x : X) (y : Y x) → is-prop (Z x y))
→ is-prop ({x : X} {y : Y x} → Z x y)
Π₂-is-prop' fe i = Π-is-prop' fe (λ x → Π-is-prop' fe (i x))

\end{code}