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 #-}

module UF-Subsingletons-FunExt where

open import SpartanMLTT

open import UF-Base
open import UF-Subsingletons
open import UF-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-a-prop-is-a-prop : {X : ๐“ค ฬ‡ } โ†’ funext ๐“ค ๐“ค โ†’ is-prop (is-prop X)
being-a-prop-is-a-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โ‚€

identifications-of-props-are-props : propext ๐“ค โ†’ funext ๐“ค ๐“ค
                                   โ†’ (P : ๐“ค ฬ‡ ) โ†’ is-prop P
                                   โ†’ (X : ๐“ค ฬ‡ ) โ†’ is-prop (X โ‰ก P)
identifications-of-props-are-props {๐“ค} pe fe P i = local-hedberg' P (ฮป X โ†’ g X โˆ˜ f X , k X)
 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-a-prop-is-a-prop fe) ,
                          (ฮป l โ†’ ร—-is-prop (ฮ -is-prop fe (ฮป x โ†’ i))
                                            (ฮ -is-prop fe (ฮป p โ†’ l))))
  k : (X : ๐“ค ฬ‡ ) โ†’ constant (g X โˆ˜ f X)
  k X p q = ap (g X) (j X (f X p) (f X q))

being-a-singleton-is-a-prop : funext ๐“ค ๐“ค โ†’ {X : ๐“ค ฬ‡ } โ†’ is-prop(is-singleton X)
being-a-singleton-is-a-prop fe {X} (x , ฯ†) (y , ฮณ) = to-ฮฃ-โ‰ก (ฯ† y , dfunext fe ฮป z โ†’ iss {y} {z} _ _)
 where
  isp : is-prop X
  isp = singletons-are-props (y , ฮณ)
  iss : is-set X
  iss = props-are-sets isp

ฮ -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 meat of the following proof is being-set-is-a-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-a-prop : funext ๐“ค ๐“ค โ†’ {X : ๐“ค ฬ‡ } โ†’ is-prop (is-set X)
being-set-is-a-prop {๐“ค} fe {X} = h
 where
  is-set' : ๐“ค ฬ‡ โ†’ ๐“ค ฬ‡
  is-set' X = (x y : X) โ†’ is-prop(x โ‰ก y)

  being-set-is-a-prop' : {X : ๐“ค ฬ‡ } โ†’ funext ๐“ค ๐“ค โ†’ is-prop (is-set' X)
  being-set-is-a-prop' fe = ฮ -is-prop fe
                              (ฮป x โ†’ ฮ -is-prop fe
                              (ฮป y โ†’ being-a-prop-is-a-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 = subtype-of-prop-is-a-prop g (ap f) (being-set-is-a-prop' fe)

\end{code}

\begin{code}

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
                                      (ฮ -is-prop feโ‚€ ฮป _ โ†’ ๐Ÿ˜-is-prop)
                                      (ฮป p u โ†’ u p)

ฮฉ-ext : funext ๐“ค ๐“ค โ†’ propext ๐“ค โ†’ {p q : ฮฉ ๐“ค}
        โ†’ (p holds โ†’ q holds) โ†’ (q holds โ†’ p holds) โ†’ p โ‰ก q
ฮฉ-ext {๐“ค} fe pe {p} {q} f g =
 to-ฮฃ-โ‰ก ((pe (holds-is-prop p) (holds-is-prop q) f g) , being-a-prop-is-a-prop fe _ _)

ฮฉ-is-a-set : funext ๐“ค ๐“ค โ†’ propext ๐“ค โ†’ is-set (ฮฉ ๐“ค)
ฮฉ-is-a-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 (ฮป X โ†’ X) a
    c : q holds โ†’ p holds
    c = transport (ฮป X โ†’ X) (a โปยน)
  h  : (p q : ฮฉ ๐“ค) โ†’ A p q โ†’ p โ‰ก q
  h p q (u , v) = ฮฉ-ext fe pe u v
  f  : (p q : ฮฉ ๐“ค) โ†’ p โ‰ก q โ†’ p โ‰ก q
  f p q e = h p q (g p q e)
  constant-f : (p q : ฮฉ ๐“ค) (d e : p โ‰ก q) โ†’ f p q d โ‰ก f p q e
  constant-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) โ†’ constant f
  pc {p} {q} = (f p q , constant-f p q)

powersets-are-sets : funext ๐“ค (๐“ฅ โบ) โ†’ funext ๐“ฅ ๐“ฅ โ†’ propext ๐“ฅ
                   โ†’ {A : ๐“ค ฬ‡ } โ†’ is-set (A โ†’ ฮฉ ๐“ฅ)
powersets-are-sets fe fe' pe = ฮ -is-set fe (ฮป x โ†’ ฮฉ-is-a-set fe' pe)

negations-are-props : {X : ๐“ค ฬ‡ } โ†’ funext ๐“ค ๐“คโ‚€ โ†’ is-prop(ยฌ X)
negations-are-props fe = ฮ -is-prop fe (ฮป x โ†’ ๐Ÿ˜-is-prop)

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}

true-is-equal-โŠค : propext ๐“ค โ†’ funext ๐“ค ๐“ค โ†’ (P : ๐“ค ฬ‡ ) (i : is-prop P)
                โ†’ P โ†’ (P , i) โ‰ก โŠค
true-is-equal-โŠค pe fe P i p = to-ฮฃ-โ‰ก (pe i ๐Ÿ™-is-prop unique-to-๐Ÿ™ (ฮป _ โ†’ p) ,
                                      being-a-prop-is-a-prop fe _ _)

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-a-prop-is-a-prop fe _ _)

ฮฉ-ext' : propext ๐“ค โ†’ funext ๐“ค ๐“ค โ†’ {p q : ฮฉ ๐“ค}
      โ†’ (p โ‰ก โŠค โ†’ q โ‰ก โŠค) โ†’ (q โ‰ก โŠค โ†’ p โ‰ก โŠค) โ†’ p โ‰ก q
ฮฉ-ext' pe fe {(P , i)} {(Q , j)} f g = to-ฮฃ-โ‰ก (pe i j I II ,
                                              being-a-prop-is-a-prop fe _ _ )
 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))

\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 = ฮฉ-ext fe pe unique-to-๐Ÿ™ (ฮป _ โ†’ p)
  ฯ† : ยฌยฌ P
  ฯ† u = f l
    where
     l : (P , i) โ‰ก โŠฅ
     l = ฮฉ-ext fe pe (ฮป p โ†’ ๐Ÿ˜-elim (u p)) unique-from-๐Ÿ˜

\end{code}

The above and 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}