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

\begin{code}

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

module UF.Subsingletons-FunExt where

open import MLTT.Spartan
open import UF.Base
open import UF.FunExt
open import UF.Hedberg
open import UF.Retracts
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-Properties

ฮ -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

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)
i
(negations-are-props feโ)
(ฮป p u โ u p)

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

holds-gives-equal-๐ : propext ๐ค โ (P : ๐ค ฬ ) โ is-prop P โ P โ P ๏ผ ๐
holds-gives-equal-๐ pe P i p = pe i ๐-is-prop unique-to-๐ (ฮป _ โ p)

equal-๐-gives-holds : (P : ๐ค ฬ ) โ P ๏ผ ๐ โ P
equal-๐-gives-holds P r = Idtofun (r โปยน) โ

not-๐-is-๐ : funext ๐ค ๐คโ
โ propext ๐ค
โ (ยฌ ๐) ๏ผ ๐
not-๐-is-๐ fe pe = pe (negations-are-props fe)
๐-is-prop
(ฮป _ โ โ)
(ฮป _ z โ ๐-elim z)

\end{code}

In the above and in the following, ๐-elim is used to coerce from ๐ {๐ค}
to ๐ {๐คโ} as this is where negations take values in.

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}