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-1009756.pdf
https://unimath.github.io/bham2017/uf.pdf

\begin{code}

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

module UF-Subsingletons where

open import SpartanMLTT
open import Unit-Properties

open import Plus-Properties
open import UF-Base

is-prop : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-prop X = (x y : X) โ†’ x โ‰ก y

\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

\end{code}

\begin{code}

ฮฃ-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 {๐“ค} {X} (c , ฯ†) x y = x โ‰กโŸจ (ฯ† x) โปยน โŸฉ c โ‰กโŸจ ฯ† y โŸฉ y โˆŽ

prop-criterion' : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ is-singleton X) โ†’ is-prop X
prop-criterion' {๐“ค} {X} ฯ† x = singletons-are-props (ฯ† x) x

prop-criterion : {X : ๐“ค ฬ‡ } โ†’ (X โ†’ is-prop X) โ†’ is-prop X
prop-criterion {๐“ค} {X} ฯ† x y = ฯ† x x y

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 {๐“ค}

\end{code}

A type is a set if all its identity types are subsingletons. In other
words, sets are types for which equality is a proposition (rather than
data or structure).

\begin{code}

is-h-isolated : {X : ๐“ค ฬ‡ } (x : X) โ†’ ๐“ค ฬ‡
is-h-isolated x = โˆ€ {y} โ†’ is-prop (x โ‰ก y)

is-set : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
is-set X = {x : X} โ†’ is-h-isolated x

refl-is-set : (X : ๐“ค ฬ‡ )
            โ†’ ((x : X) (p : x โ‰ก x) โ†’ p โ‰ก refl)
            โ†’ is-set X
refl-is-set X r {x} {.x} p refl = r x p

\end{code}

We now consider some machinery for dealing with the above notions,
using weakly, or wildly, constant maps:

\begin{code}

wconstant : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ (f : X โ†’ Y) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
wconstant f = โˆ€ x y โ†’ f x โ‰ก f y

wconstant-pre-comp : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } (f : X โ†’ Y) (g : Y โ†’ Z)
                   โ†’ wconstant f โ†’ wconstant (g โˆ˜ f)
wconstant-pre-comp f g c x x' = ap g (c x x')

wconstant-post-comp : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {Z : ๐“ฆ ฬ‡ } (f : X โ†’ Y) (g : Y โ†’ Z)
                    โ†’ wconstant g โ†’ wconstant (g โˆ˜ f)
wconstant-post-comp f g c x x' = c (f x) (f x')

collapsible : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
collapsible X = ฮฃ f ๊ž‰ (X โ†’ X) , wconstant f

Id-collapsible : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
Id-collapsible X = {x y : X} โ†’ collapsible(x โ‰ก y)

sets-are-Id-collapsible : {X : ๐“ค ฬ‡ } โ†’ is-set X โ†’ Id-collapsible X
sets-are-Id-collapsible u = (id , u)

local-hedberg : {X : ๐“ค ฬ‡ } (x : X)
              โ†’ ((y : X) โ†’ collapsible (x โ‰ก y))
              โ†’ (y : X) โ†’ is-prop (x โ‰ก y)
local-hedberg {๐“ค} {X} x pc y p q =
 p                    โ‰กโŸจ c y p โŸฉ
 f x refl โปยน โˆ™ f y p  โ‰กโŸจ ap (ฮป - โ†’ (f x refl)โปยน โˆ™ -) (ฮบ y p q) โŸฉ
 f x refl โปยน โˆ™ f y q  โ‰กโŸจ (c y q)โปยน โŸฉ
 q                    โˆŽ
 where
  f : (y : X) โ†’ x โ‰ก y โ†’ x โ‰ก y
  f y = prโ‚ (pc y)
  ฮบ : (y : X) (p q : x โ‰ก y) โ†’ f y p โ‰ก f y q
  ฮบ y = prโ‚‚ (pc y)
  c : (y : X) (r : x โ‰ก y) โ†’ r โ‰ก (f x refl)โปยน โˆ™ f y r
  c _ refl = sym-is-inverse (f x refl)

Id-collapsibles-are-sets : {X : ๐“ค ฬ‡ } โ†’ Id-collapsible X โ†’ is-set X
Id-collapsibles-are-sets pc {x} {y} p q = local-hedberg x (ฮป y โ†’ (prโ‚(pc {x} {y})) , (prโ‚‚(pc {x} {y}))) y p q

\end{code}

Here is an example. Any type that admits a prop-valued, reflexive and
antisymmetric relation is a set.

\begin{code}

type-with-prop-valued-refl-antisym-rel-is-set : {X : ๐“ค ฬ‡ }
                                              โ†’ (_โ‰ค_ : X โ†’ X โ†’ ๐“ฅ ฬ‡ )
                                              โ†’ ((x y : X) โ†’ is-prop (x โ‰ค y))
                                              โ†’ ((x : X) โ†’ x โ‰ค x)
                                              โ†’ ((x y : X) โ†’ x โ‰ค y โ†’ y โ‰ค x โ†’ x โ‰ก y)
                                              โ†’ is-set X
type-with-prop-valued-refl-antisym-rel-is-set {๐“ค} {๐“ฅ} {X} _โ‰ค_ โ‰ค-prop-valued โ‰ค-refl โ‰ค-anti = ฮณ
 where
  ฮฑ : โˆ€ {x} {y} (l l' : x โ‰ค y) (m m' : y โ‰ค x) โ†’ โ‰ค-anti x y l m โ‰ก โ‰ค-anti x y l' m'
  ฮฑ {x} {y} l l' m m' = apโ‚‚ (โ‰ค-anti x y) (โ‰ค-prop-valued x y l l') (โ‰ค-prop-valued y x m m')

  g : โˆ€ {x y} โ†’ x โ‰ก y โ†’ x โ‰ค y
  g {x} {y} p = transport (x โ‰ค_) p (โ‰ค-refl x)

  h : โˆ€ {x y} โ†’ x โ‰ก y โ†’ y โ‰ค x
  h {x} {y} p = g (p โปยน)

  f : โˆ€ {x y} โ†’ x โ‰ก y โ†’ x โ‰ก y
  f {x} {y} p = โ‰ค-anti x y (g p) (h p)

  ฮบ : โˆ€ {x} {y} p q โ†’ f {x} {y} p โ‰ก f {x} {y} q
  ฮบ {x} {y} p q = ฮฑ (g p) (g q) (h p) (h q)

  ฮณ : is-set X
  ฮณ = Id-collapsibles-are-sets (f , ฮบ)

\end{code}

We also need the following symmetrical version of local Hedberg, which
can be proved by reduction to the above (using the fact that
collapsible types are closed under equivalence), but at this point we
don't have the machinery at our disposal (which is developed in
modules that depend on this one), and hence we prove it directly by
symmetrizing the proof.

\begin{code}

local-hedberg' : {X : ๐“ค ฬ‡ } (x : X)
               โ†’ ((y : X) โ†’ collapsible (y โ‰ก x))
               โ†’ (y : X) โ†’ is-prop (y โ‰ก x)
local-hedberg' {๐“ค} {X} x pc y p q =
  p                     โ‰กโŸจ c y p โŸฉ
  f y p โˆ™ (f x refl)โปยน  โ‰กโŸจ  ap (ฮป - โ†’ - โˆ™ (f x refl)โปยน) (ฮบ y p q) โŸฉ
  f y q โˆ™ (f x refl)โปยน  โ‰กโŸจ (c y q)โปยน โŸฉ
  q                     โˆŽ
 where
  f : (y : X) โ†’ y โ‰ก x โ†’ y โ‰ก x
  f y = prโ‚ (pc y)
  ฮบ : (y : X) (p q : y โ‰ก x) โ†’ f y p โ‰ก f y q
  ฮบ y = prโ‚‚ (pc y)
  c : (y : X) (r : y โ‰ก x) โ†’ r โ‰ก  (f y r) โˆ™ (f x refl)โปยน
  c _ refl = sym-is-inverse' (f x refl)

props-are-Id-collapsible : {X : ๐“ค ฬ‡ } โ†’ is-prop X โ†’ Id-collapsible X
props-are-Id-collapsible h {x} {y} = (ฮป p โ†’ h x y) , (ฮป p q โ†’ refl)

props-are-sets : {X : ๐“ค ฬ‡ } โ†’ is-prop X โ†’ is-set X
props-are-sets h = Id-collapsibles-are-sets(props-are-Id-collapsible h)

๐Ÿ˜-is-collapsible : collapsible (๐Ÿ˜ {๐“ค})
๐Ÿ˜-is-collapsible {๐“ค} = id , (ฮป x y โ†’ ๐Ÿ˜-elim y)

pointed-types-are-collapsible : {X : ๐“ค ฬ‡ } โ†’ X โ†’ collapsible X
pointed-types-are-collapsible x = (ฮป y โ†’ x) , (ฮป y y' โ†’ refl)

\end{code}

Under Curry-Howard, the function type X โ†’ ๐Ÿ˜ is understood as the
negation of X when X is viewed as a proposition. But when X is
understood as a mathematical object, inhabiting the type X โ†’ ๐Ÿ˜ amounts
to showing that X is empty. (In fact, assuming univalence, defined
below, the type X โ†’ ๐Ÿ˜ is equivalent to the type X โ‰ก ๐Ÿ˜
(written (X โ†’ ๐Ÿ˜) โ‰ƒ (X โ‰ก ๐Ÿ˜)).)

\begin{code}

empty-types-are-collapsible : {X : ๐“ค ฬ‡ } โ†’ is-empty X โ†’ collapsible X
empty-types-are-collapsible u = (id , (ฮป x x' โ†’ unique-from-๐Ÿ˜(u x)))

๐Ÿ˜-is-collapsible' : collapsible ๐Ÿ˜
๐Ÿ˜-is-collapsible' = empty-types-are-collapsible id

singleton-type : {X : ๐“ค ฬ‡ } (x : X) โ†’ ๐“ค ฬ‡
singleton-type x = ฮฃ y ๊ž‰ type-of x , x โ‰ก y

singleton-inclusion : {X : ๐“ค ฬ‡ } (x : X) โ†’ singleton-type x
singleton-inclusion x = (x , refl)

singleton-types-are-singletons'' : {X : ๐“ค ฬ‡ } {x x' : X} (r : x โ‰ก x') โ†’ singleton-inclusion x โ‰ก (x' , r)
singleton-types-are-singletons'' {๐“ค} {X} = J A (ฮป x โ†’ refl)
 where
  A : (x x' : X) โ†’ x โ‰ก x' โ†’ ๐“ค ฬ‡
  A x x' r = _โ‰ก_ {_} {ฮฃ x' ๊ž‰ X , x โ‰ก x'} (singleton-inclusion x) (x' , r)

singleton-types-are-singletons : {X : ๐“ค ฬ‡ } (xโ‚€ : X) โ†’ is-singleton(singleton-type xโ‚€)
singleton-types-are-singletons xโ‚€ = singleton-inclusion 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

ร—-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 : ๐“ค ฬ‡ } {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)

subtype-of-prop-is-prop : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (m : X โ†’ Y)
                          โ†’ left-cancellable m โ†’ is-prop Y โ†’ is-prop X
subtype-of-prop-is-prop {๐“ค} {๐“ฅ} {X} m lc i x x' = lc (i (m x) (m x'))

subtypes-of-sets-are-sets : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } (m : X โ†’ Y)
                          โ†’ left-cancellable m โ†’ is-set Y โ†’ is-set X
subtypes-of-sets-are-sets {๐“ค} {๐“ฅ} {X} m i h = Id-collapsibles-are-sets (f , g)
 where
  f : {x x' : X} โ†’ x โ‰ก x' โ†’ x โ‰ก x'
  f r = i (ap m r)
  g : {x x' : X} (r s : x โ‰ก x') โ†’ f r โ‰ก f s
  g r s = ap i (h (ap m r) (ap m s))

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-sets-are-sets : (X : ๐“ค ฬ‡ ) (Y : X โ†’ ๐“ฅ ฬ‡ )
                         โ†’ is-set X
                         โ†’ ({x : X} โ†’ is-prop(Y x))
                         โ†’ is-set(ฮฃ x ๊ž‰ X , Y x)
subsets-of-sets-are-sets X Y h p = subtypes-of-sets-are-sets 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

+-is-set : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ ) โ†’ is-set X โ†’ is-set Y โ†’ is-set (X + Y)
+-is-set X Y i j {inl x} {inl x'} p q = inl-lc-is-section p โˆ™ r โˆ™ (inl-lc-is-section q)โปยน
 where
  r : ap inl (inl-lc p) โ‰ก ap inl (inl-lc q)
  r = ap (ap inl) (i (inl-lc p) (inl-lc q))
+-is-set X Y i j {inl x} {inr y} p q = ๐Ÿ˜-elim (+disjoint  p)
+-is-set X Y i j {inr y} {inl x} p q = ๐Ÿ˜-elim (+disjoint' p)
+-is-set X Y i j {inr y} {inr y'} p q = inr-lc-is-section p โˆ™ r โˆ™ (inr-lc-is-section q)โปยน
 where
  r : ap inr (inr-lc p) โ‰ก ap inr (inr-lc q)
  r = ap (ap inr) (j (inr-lc p) (inr-lc q))

ร—-is-set : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } โ†’ is-set X โ†’ is-set Y โ†’ is-set (X ร— Y)
ร—-is-set i j {(x , y)} {(x' , y')} p q =
 p            โ‰กโŸจ tofrom-ร—-โ‰ก p โŸฉ
 to-ร—-โ‰ก pโ‚€ pโ‚ โ‰กโŸจ apโ‚‚ (ฮป -โ‚€ -โ‚ โ†’ to-ร—-โ‰ก -โ‚€ -โ‚) (i pโ‚€ qโ‚€) (j pโ‚ qโ‚) โŸฉ
 to-ร—-โ‰ก qโ‚€ qโ‚ โ‰กโŸจ (tofrom-ร—-โ‰ก q)โปยน โŸฉ
 q            โˆŽ where
  pโ‚€ : x โ‰ก x'
  pโ‚€ = prโ‚ (from-ร—-โ‰ก' p)
  pโ‚ : y โ‰ก y'
  pโ‚ = prโ‚‚ (from-ร—-โ‰ก' p)
  qโ‚€ : x โ‰ก x'
  qโ‚€ = prโ‚ (from-ร—-โ‰ก' q)
  qโ‚ : y โ‰ก y'
  qโ‚ = prโ‚‚ (from-ร—-โ‰ก' q)

\end{code}

Formulation of the K axiom for a universe U.

\begin{code}

K-axiom : โˆ€ ๐“ค โ†’ ๐“ค โบ ฬ‡
K-axiom ๐“ค = (X : ๐“ค ฬ‡ ) โ†’ is-set X

\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 = go
 where
  go : (x y : P + Q) โ†’ x โ‰ก y
  go (inl p) (inl p') = ap inl (i p p')
  go (inl p) (inr q)  = ๐Ÿ˜-elim {๐“ค โŠ” ๐“ฅ} {๐“ฆ} (f p q)
  go (inr q) (inl p)  = ๐Ÿ˜-elim (f p q)
  go (inr q) (inr q') = ap inr (j q 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 โปยน) *)

\end{code}

Unique existence.

\begin{code}

โˆƒ! : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
โˆƒ! A = is-singleton (ฮฃ A)

existsUnique : (X : ๐“ค ฬ‡ ) (A : X โ†’ ๐“ฅ ฬ‡ ) โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
existsUnique X A = โˆƒ! A

syntax existsUnique A (ฮป x โ†’ b) = โˆƒ! x ๊ž‰ A , 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}

The type of truth values.

\begin{code}

ฮฉ : โˆ€ ๐“ค โ†’ ๐“ค โบ ฬ‡
ฮฉ ๐“ค = ฮฃ P ๊ž‰ ๐“ค ฬ‡ , is-prop P

ฮฉโ‚€ = ฮฉ ๐“คโ‚€

_holds : ฮฉ ๐“ค โ†’ ๐“ค ฬ‡
(P , i) holds = P


holds-is-prop : (p : ฮฉ ๐“ค) โ†’ is-prop (p holds)
holds-is-prop (P , i) = i

โŠฅฮฉ โŠคฮฉ : ฮฉ ๐“ค
โŠฅฮฉ = ๐Ÿ˜ , ๐Ÿ˜-is-prop   -- false
โŠคฮฉ = ๐Ÿ™ , ๐Ÿ™-is-prop   -- true

\end{code}