Martin Escardo

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

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

\begin{code}

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

module UF.Subsingletons where

open import MLTT.Plus-Properties
open import MLTT.Spartan
open import MLTT.Unit-Properties
open import UF.Base

is-prop : ๐ค ฬ โ ๐ค ฬ
is-prop X = (x y : X) โ x ๏ผ y

is-prop-valued-family : {X : ๐ค ฬ } โ (X โ ๐ฅ ฬ ) โ ๐ค โ ๐ฅ ฬ
is-prop-valued-family A = โ x โ is-prop (A x)

\end{code}

And of course we could adopt a terminology borrowed from topos logic:

\begin{code}

is-truth-value is-subsingleton : ๐ค ฬ โ ๐ค ฬ
is-truth-value  = is-prop
is-subsingleton = is-prop

ฮฃ-is-prop : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
โ is-prop X
โ ((x : X) โ is-prop (A x))
โ is-prop (ฮฃ A)
ฮฃ-is-prop {๐ค} {๐ฅ} {X} {A} i j (x , a) (y , b) =
to-ฮฃ-๏ผ (i x y , j y (transport A (i x y) a) b)

\end{code}

Next we define singleton (or contractible types). The terminology
"contractible" is due to Voevodsky. I currently prefer the terminology
"singleton type", because it makes more sense when we consider
univalent type theory as interesting on its own right independently of
its homotopical (originally motivating) models. Also it emphasizes
that we don't require homotopy theory as a prerequisite to understand
univalent type theory.

\begin{code}

is-central : (X : ๐ค ฬ ) โ X โ ๐ค ฬ
is-central X c = (x : X) โ c ๏ผ x

is-singleton : ๐ค ฬ โ ๐ค ฬ
is-singleton X = ฮฃ c ๊ X , is-central X c

center : {X : ๐ค ฬ } โ is-singleton X โ X
center = prโ

centrality : {X : ๐ค ฬ } (i : is-singleton X) โ is-central X (center i)
centrality = prโ

\end{code}

For compatibility with the homotopical terminology:

\begin{code}

is-center-of-contraction-of : (X : ๐ค ฬ ) โ X โ ๐ค ฬ
is-center-of-contraction-of = is-central

is-contr : ๐ค ฬ โ ๐ค ฬ
is-contr = is-singleton

๐-is-singleton : is-singleton (๐ {๐ค})
๐-is-singleton = โ , (ฮป (x : ๐) โ (๐-all-โ x)โปยน)

singletons-are-props : {X : ๐ค ฬ } โ is-singleton X โ is-prop X
singletons-are-props (c , ฯ) x y = x ๏ผโจ (ฯ x) โปยน โฉ
c ๏ผโจ ฯ y โฉ
y โ

prop-criterion' : {X : ๐ค ฬ }
โ (X โ is-singleton X)
โ is-prop X
prop-criterion' ฯ x = singletons-are-props (ฯ x) x

prop-criterion : {X : ๐ค ฬ } โ (X โ is-prop X) โ is-prop X
prop-criterion ฯ x = ฯ x x

pointed-props-are-singletons : {X : ๐ค ฬ }
โ X
โ is-prop X
โ is-singleton X
pointed-props-are-singletons x h = x , h x

\end{code}

The two prototypical propositions:

\begin{code}

๐-is-prop : is-prop (๐ {๐ค})
๐-is-prop {๐ค} x y = unique-from-๐ {๐ค} {๐ค} x

๐-is-prop : is-prop (๐ {๐ค})
๐-is-prop {๐ค} โ โ = refl {๐ค}

singleton-type : {X : ๐ค ฬ } (x : X) โ ๐ค ฬ
singleton-type x = ฮฃ y ๊ type-of x , x ๏ผ y

singleton-center : {X : ๐ค ฬ } (x : X) โ singleton-type x
singleton-center x = (x , refl)

singleton-types-are-singletons'' : {X : ๐ค ฬ } {x x' : X} (r : x ๏ผ x')
โ singleton-center x ๏ผ (x' , r)
singleton-types-are-singletons'' {๐ค} {X} = J A (ฮป x โ refl)
where
A : (x x' : X) โ x ๏ผ x' โ ๐ค ฬ
A x x' r = singleton-center x ๏ผ[ ฮฃ x' ๊ X , x ๏ผ x' ] (x' , r)

singleton-types-are-singletons : {X : ๐ค ฬ } (xโ : X)
โ is-singleton (singleton-type xโ)
singleton-types-are-singletons xโ = singleton-center xโ , (ฮป t โ singleton-types-are-singletons'' (prโ t))

singleton-types-are-singletons' : {X : ๐ค ฬ } {x : X}
โ is-central (singleton-type x) (x , refl)
singleton-types-are-singletons' {๐ค} {X} (y , refl) = refl

singleton-types-are-props : {X : ๐ค ฬ } (x : X) โ is-prop (singleton-type x)
singleton-types-are-props x = singletons-are-props (singleton-types-are-singletons x)

singleton-type' : {X : ๐ค ฬ } โ X โ ๐ค ฬ
singleton-type' x = ฮฃ y ๊ type-of x , y ๏ผ x

singleton'-center : {X : ๐ค ฬ } (x : X) โ singleton-type' x
singleton'-center x = (x , refl)

ร-prop-criterion-necessity : {X : ๐ค ฬ } {Y : ๐ฅ ฬ }
โ is-prop (X ร Y) โ (Y โ is-prop X) ร (X โ is-prop Y)
ร-prop-criterion-necessity i = (ฮป y x x' โ ap prโ (i (x , y) (x' , y ))) ,
(ฮป x y y' โ ap prโ (i (x , y) (x  , y')))

ร-prop-criterion : {X : ๐ค ฬ } {Y : ๐ฅ ฬ }
โ (Y โ is-prop X) ร (X โ is-prop Y) โ is-prop (X ร Y)
ร-prop-criterion (i , j) (x , y) (x' , y') = to-ฮฃ-๏ผ (i y x x' , j x _ _)

ร-๐-is-prop : {X : ๐ค ฬ } โ is-prop (X ร ๐ {๐ฅ})
ร-๐-is-prop (x , z) _ = ๐-elim z

๐-ร-is-prop : {X : ๐ค ฬ } โ is-prop (๐ {๐ฅ} ร X)
๐-ร-is-prop (z , x) _ = ๐-elim z

ร-is-prop : {X : ๐ค ฬ } {Y : ๐ฅ ฬ }
โ is-prop X
โ is-prop Y
โ is-prop (X ร Y)
ร-is-prop i j = ร-prop-criterion ((ฮป _ โ i) , (ฮป _ โ j))

to-subtype-๏ผ : {X : ๐ฆ ฬ } {A : X โ ๐ฅ ฬ }
{x y : X} {a : A x} {b : A y}
โ ((x : X) โ is-prop (A x))
โ x ๏ผ y
โ (x , a) ๏ผ (y , b)
to-subtype-๏ผ {๐ค} {๐ฅ} {X} {A} {x} {y} {a} {b} s p =
to-ฮฃ-๏ผ (p , s y (transport A p a) b)

subtypes-of-props-are-props' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (m : X โ Y)
โ left-cancellable m
โ is-prop Y
โ is-prop X
subtypes-of-props-are-props' m lc i x x' = lc (i (m x) (m x'))

prโ-lc : {X : ๐ค ฬ } {Y : X โ ๐ฅ ฬ }
โ ({x : X} โ is-prop (Y x))
โ left-cancellable (prโ {๐ค} {๐ฅ} {X} {Y})
prโ-lc f p = to-ฮฃ-๏ผ (p , (f _ _))

subsets-of-props-are-props : (X : ๐ค ฬ ) (Y : X โ ๐ฅ ฬ )
โ is-prop X
โ ({x : X} โ is-prop (Y x))
โ is-prop (ฮฃ x ๊ X , Y x)
subsets-of-props-are-props X Y h p = subtypes-of-props-are-props' prโ (prโ-lc p) h

inl-lc-is-section : {X : ๐ค ฬ } {Y : ๐ฅ ฬ }
{x x' : X}
(p : inl {๐ค} {๐ฅ} {X} {Y} x ๏ผ inl x')
โ p ๏ผ ap inl (inl-lc p)
inl-lc-is-section refl = refl

inr-lc-is-section : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {y y' : Y}
(p : inr {๐ค} {๐ฅ} {X} {Y} y ๏ผ inr y')
โ p ๏ผ ap inr (inr-lc p)
inr-lc-is-section refl = refl

\end{code}

Formulation of propositional extensionality:

\begin{code}

propext : โ ๐ค โ ๐ค โบ ฬ
propext ๐ค = {P Q : ๐ค ฬ } โ is-prop P โ is-prop Q โ (P โ Q) โ (Q โ P) โ P ๏ผ Q

PropExt : ๐คฯ
PropExt = โ ๐ค โ propext ๐ค

Prop-Ext : ๐คฯ
Prop-Ext = โ {๐ค} โ propext ๐ค

\end{code}

The following says that, in particular, for any proposition P, we have
that P + ยฌ P is a proposition, or that the decidability of a
proposition is a proposition:

\begin{code}

sum-of-contradictory-props : {P : ๐ค ฬ } {Q : ๐ฅ ฬ }
โ is-prop P
โ is-prop Q
โ (P โ Q โ ๐ {๐ฆ})
โ is-prop (P + Q)
sum-of-contradictory-props {๐ค} {๐ฅ} {๐ฆ} {P} {Q} i j f = ฮณ
where
ฮณ : (x y : P + Q) โ x ๏ผ y
ฮณ (inl p) (inl p') = ap inl (i p p')
ฮณ (inl p) (inr q)  = ๐-elim {๐ค โ ๐ฅ} {๐ฆ} (f p q)
ฮณ (inr q) (inl p)  = ๐-elim (f p q)
ฮณ (inr q) (inr q') = ap inr (j q q')

sum-of-contradictory-props' : {P : ๐ค ฬ } {Q : ๐ฅ ฬ }
โ (is-prop P ร is-prop Q ร (P โ Q โ ๐ {๐ฆ}))
โ is-prop (P + Q)

sum-of-contradictory-props'-converse : {P : ๐ค ฬ } {Q : ๐ฅ ฬ }
โ is-prop (P + Q)
โ (is-prop P ร is-prop Q ร (P โ Q โ ๐ {๐ฆ}))
(ฮป p p' โ inl-lc (k (inl p) (inl p'))) ,
(ฮป q q' โ inr-lc (k (inr q) (inr q'))) ,
(ฮป p q โ ๐-elim (+disjoint (k (inl p) (inr q))))

\end{code}

Without assuming excluded middle, we have that there are no truth
values other than ๐ and ๐:

\begin{code}

no-props-other-than-๐-or-๐ : propext ๐ค โ ยฌ (ฮฃ P ๊ ๐ค ฬ , is-prop P ร (P โ  ๐) ร (P โ  ๐))
no-props-other-than-๐-or-๐ pe (P , i , f , g) = ๐-elim (ฯ u)
where
u : ยฌ P
u p = g l
where
l : P ๏ผ ๐
l = pe i ๐-is-prop unique-to-๐ (ฮป _ โ p)

ฯ : ยฌยฌ P
ฯ u = f l
where
l : P ๏ผ ๐
l = pe i ๐-is-prop (ฮป p โ ๐-elim (u p)) ๐-elim

\end{code}

Notice how we used ๐-elim above to coerce a hypothetical value in ๐
{๐คโ}, arising from negation, to a value in ๐ {๐ค}. Otherwise "u" would
have sufficed in place of "ฮป p โ ๐-elim (u p)". The same technique is
used in the following construction.

\begin{code}

๐-is-not-๐ : ๐ {๐ค} โ  ๐ {๐ค}
๐-is-not-๐ p = ๐-elim (Idtofun (p โปยน) โ)

universe-has-two-distinct-points : has-two-distinct-points (๐ค ฬ )
universe-has-two-distinct-points = ((๐ , ๐) , ๐-is-not-๐)

\end{code}

Unique existence.

\begin{code}

โ! : {X : ๐ค ฬ } (A : X โ ๐ฅ ฬ ) โ ๐ค โ ๐ฅ ฬ
โ! A = is-singleton (ฮฃ A)

existsUnique : (X : ๐ค ฬ ) (A : X โ ๐ฅ ฬ ) โ ๐ค โ ๐ฅ ฬ
existsUnique X A = โ! A

syntax existsUnique X (ฮป x โ b) = โ! x ๊ X , b

witness-uniqueness : {X : ๐ค ฬ } (A : X โ ๐ฅ ฬ )
โ (โ! x ๊ X , A x)
โ (x y : X) โ A x โ A y โ x ๏ผ y
witness-uniqueness A e x y a b = ap prโ (singletons-are-props e (x , a) (y , b))

infixr -1 existsUnique

โ!-intro : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (x : X) (a : A x)
โ ((ฯ : ฮฃ A) โ (x , a) ๏ผ ฯ)
โ โ! A
โ!-intro x a o = (x , a) , o

โ!-witness : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } โ โ! A โ X
โ!-witness ((x , a) , o) = x

โ!-is-witness : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
(u : โ! A)
โ A (โ!-witness u)
โ!-is-witness ((x , a) , o) = a

description : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } โ โ! A โ ฮฃ A
description (ฯ , o) = ฯ

โ!-uniqueness' : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
(u : โ! A)
โ (ฯ : ฮฃ A)
โ description u ๏ผ ฯ
โ!-uniqueness' ((x , a) , o) = o

โ!-uniqueness : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
(u : โ! A)
โ (x : X)
(a : A x)
โ description u ๏ผ (x , a)
โ!-uniqueness u x a = โ!-uniqueness' u (x , a)

โ!-uniqueness'' : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
(u : โ! A)
โ (ฯ ฯ : ฮฃ A)
โ ฯ ๏ผ ฯ
โ!-uniqueness'' u ฯ ฯ = โ!-uniqueness' u ฯ โปยน โ โ!-uniqueness' u ฯ

\end{code}

Added 5 March 2020 by Tom de Jong.

\begin{code}

+-is-prop : {X : ๐ค ฬ } {Y : ๐ฅ ฬ }
โ is-prop X
โ is-prop Y
โ (X โ ยฌ Y)
โ is-prop (X + Y)
+-is-prop i j f (inl x) (inl x') = ap inl (i x x')
+-is-prop i j f (inl x) (inr y) = ๐-induction (f x y)
+-is-prop i j f (inr y) (inl x) = ๐-induction (f x y)
+-is-prop i j f (inr y) (inr y') = ap inr (j y y')

+-is-prop' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ }
โ is-prop X
โ is-prop Y
โ (Y โ ยฌ X)
โ is-prop (X + Y)
+-is-prop' {๐ค} {๐ฅ} {X} {Y} i j f = +-is-prop i j (ฮป y x โ f x y)

\end{code}

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

\begin{code}

รโ-is-prop : {๐ฅโ ๐ฅโ ๐ฅโ : Universe}
{Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ }
โ is-prop Xโ โ is-prop Xโ โ is-prop Xโ โ is-prop (Xโ ร Xโ ร Xโ)
รโ-is-prop iโ iโ iโ = ร-is-prop iโ (ร-is-prop iโ iโ)

รโ-is-prop : {๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ : Universe}
{Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ }
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop (Xโ ร Xโ ร Xโ ร Xโ)
รโ-is-prop iโ iโ iโ iโ = ร-is-prop iโ (รโ-is-prop iโ iโ iโ)

รโ-is-prop : {๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ : Universe}
{Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ }
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop (Xโ ร Xโ ร Xโ ร Xโ ร Xโ)
รโ-is-prop iโ iโ iโ iโ iโ = ร-is-prop iโ (รโ-is-prop iโ iโ iโ iโ)

รโ-is-prop : {๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ : Universe}
{Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ }
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop (Xโ ร Xโ ร Xโ ร Xโ ร Xโ ร Xโ)
รโ-is-prop iโ iโ iโ iโ iโ iโ = ร-is-prop iโ (รโ-is-prop iโ iโ iโ iโ iโ)

รโ-is-prop : {๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ : Universe}
{Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ }
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop (Xโ ร Xโ ร Xโ ร Xโ ร Xโ ร Xโ ร Xโ)
รโ-is-prop iโ iโ iโ iโ iโ iโ iโ = ร-is-prop iโ (รโ-is-prop iโ iโ iโ iโ iโ iโ)

รโ-is-prop : {๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ ๐ฅโ : Universe}
{Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ } {Xโ : ๐ฅโ ฬ }
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ
โ is-prop Xโ โ is-prop (Xโ ร Xโ ร Xโ ร Xโ ร Xโ ร Xโ ร Xโ ร Xโ)
รโ-is-prop iโ iโ iโ iโ iโ iโ iโ iโ = ร-is-prop iโ (รโ-is-prop iโ iโ iโ iโ iโ iโ iโ)

\end{code}