Martin Escardo

\begin{code}

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

module UF-PropTrunc where

open import SpartanMLTT

open import Plus-Properties
open import UF-Base
open import UF-Subsingletons
open import UF-FunExt
open import UF-Subsingletons-FunExt
open import UF-Equiv

\end{code}

We use the existence of propositional truncations as an
assumption. The following type collects the data that constitutes this
assumption.

\begin{code}

record propositional-truncations-exist : π€Ο where
field
β₯_β₯ : {π€ : Universe} β π€ Μ β π€ Μ
β₯β₯-is-prop : {π€ : Universe} {X : π€ Μ } β is-prop β₯ X β₯
β£_β£ : {π€ : Universe} {X : π€ Μ } β X β β₯ X β₯
β₯β₯-rec : {π€ π₯ : Universe} {X : π€ Μ } {P : π₯ Μ } β is-prop P β (X β P) β β₯ X β₯ β P
infix 0 β₯_β₯
infix 0 β£_β£

module PropositionalTruncation (pt : propositional-truncations-exist) where

open propositional-truncations-exist pt public

β₯β₯-induction : {X : π€ Μ } {P : β₯ X β₯ β π₯ Μ }
β ((s : β₯ X β₯) β is-prop (P s))
β ((x : X) β P β£ x β£)
β (s : β₯ X β₯) β P s

β₯β₯-induction {π€} {π₯} {X} {P} i f s = Ο' s
where
Ο : X β P s
Ο x = transport P (β₯β₯-is-prop β£ x β£ s) (f x)
Ο' : β₯ X β₯ β P s
Ο' = β₯β₯-rec (i s) Ο

is-singleton'-is-prop : {X : π€ Μ } β funext π€ π€ β is-prop (is-prop X Γ β₯ X β₯)
is-singleton'-is-prop fe = Ξ£-is-prop (being-prop-is-prop fe) (Ξ» _ β β₯β₯-is-prop)

the-singletons-are-the-inhabited-propositions : {X : π€ Μ } β is-singleton X β is-prop X Γ β₯ X β₯
the-singletons-are-the-inhabited-propositions {π€} {X} = f , g
where
f : is-singleton X β is-prop X Γ β₯ X β₯
f (x , Ο) = singletons-are-props (x , Ο) , β£ x β£

g : is-prop X Γ β₯ X β₯ β is-singleton X
g (i , s) = β₯β₯-rec i id s , i (β₯β₯-rec i id s)

β₯β₯-functor : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β β₯ X β₯ β β₯ Y β₯
β₯β₯-functor f = β₯β₯-rec β₯β₯-is-prop (Ξ» x β β£ f x β£)

β₯β₯-recβ : {π€ π₯ : Universe} {X : π€ Μ } {Y : π₯ Μ } {P : π¦ Μ }
β is-prop P β (X β Y β P) β β₯ X β₯ β β₯ Y β₯ β P
β₯β₯-recβ i f s t = β₯β₯-rec i (Ξ» x β β₯β₯-rec i (f x) t) s

β₯β₯-functorβ : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ }
β (X β Y β Z) β β₯ X β₯ β β₯ Y β₯ β β₯ Z β₯
β₯β₯-functorβ f s t = β₯β₯-rec β₯β₯-is-prop (Ξ» x β β₯β₯-functor (f x) t) s

β : {X : π€ Μ } (Y : X β π₯ Μ ) β π€ β π₯ Μ
β Y = β₯ Ξ£ Y β₯

β-is-prop : {X : π€ Μ } {Y : X β π₯ Μ } β is-prop (β Y)
β-is-prop = β₯β₯-is-prop

Exists : {π€ π₯ : Universe} (X : π€ Μ ) (Y : X β π₯ Μ ) β π€ β π₯ Μ
Exists X Y = β Y

syntax Exists A (Ξ» x β b) = β x κ A , b

infixr -1 Exists

_β¨_  : π€ Μ β π₯ Μ β π€ β π₯ Μ
P β¨ Q = β₯ P + Q β₯

β¨-is-prop  : {P : π€ Μ } {Q : π₯ Μ } β is-prop (P β¨ Q)
β¨-is-prop = β₯β₯-is-prop

β¨-elim : {P : π€ Μ } {Q : π₯ Μ } {R : π¦ Μ }
β is-prop R
β (P β R)
β (Q β R)
β P β¨ Q β R
β¨-elim i f g = β₯β₯-rec i (cases f g)

β¨-functor : {P : π€ Μ } {Q : π₯ Μ } {R : π¦ Μ } {S : π£ Μ }
β (P β R)
β (Q β S)
β P β¨ Q β R β¨ S
β¨-functor f g = β₯β₯-functor (+functor f g)

left-fails-gives-right-holds : {P : π€ Μ } {Q : π₯ Μ } β is-prop Q β P β¨ Q β Β¬ P β Q
left-fails-gives-right-holds i d u = β₯β₯-rec i (Ξ» d β Left-fails-gives-right-holds d u) d

right-fails-gives-left-holds : {P : π€ Μ } {Q : π₯ Μ } β is-prop P β P β¨ Q β Β¬ Q β P
right-fails-gives-left-holds i d u = β₯β₯-rec i (Ξ» d β Right-fails-gives-left-holds d u) d

pt-gdn : {X : π€ Μ } β β₯ X β₯ β β {π₯} (P : π₯ Μ ) β is-prop P β (X β P) β P
pt-gdn {π€} {X} s {π₯} P isp u = β₯β₯-rec isp u s

gdn-pt : {X : π€ Μ } β (β {π₯} (P : π₯ Μ ) β is-prop P β (X β P) β P) β β₯ X β₯
gdn-pt {π€} {X} Ο = Ο β₯ X β₯ β₯β₯-is-prop β£_β£

is-inhabited : {X : π€ Μ } β (X β Ξ© π₯) β π€ β π₯ Μ
is-inhabited {π€} {π₯} {X} A = β x κ X , A x holds

being-inhabited-is-prop : {X : π€ Μ } (A : X β Ξ© π₯) β is-prop (is-inhabited A)
being-inhabited-is-prop {π€} {π₯} {X} A = β-is-prop

inhabited-is-nonempty : {X : π€ Μ } β β₯ X β₯ β Β¬Β¬ X
inhabited-is-nonempty s = pt-gdn s π π-is-prop

uninhabited-is-empty : {X : π€ Μ } β Β¬ β₯ X β₯ β Β¬ X
uninhabited-is-empty u x = u β£ x β£

empty-is-uninhabited : {X : π€ Μ } β Β¬ X β Β¬ β₯ X β₯
empty-is-uninhabited v = β₯β₯-rec π-is-prop v

binary-choice : {X : π€ Μ } {Y : π₯ Μ } β β₯ X β₯ β β₯ Y β₯ β β₯ X Γ Y β₯
binary-choice s t = β₯β₯-rec β₯β₯-is-prop (Ξ» x β β₯β₯-rec β₯β₯-is-prop (Ξ» y β β£ x , y β£) t) s

prop-is-equivalent-to-its-truncation : {X : π€ Μ } β is-prop X β β₯ X β₯ β X
prop-is-equivalent-to-its-truncation i =
logically-equivalent-props-are-equivalent β₯β₯-is-prop i (β₯β₯-rec i id) β£_β£

\end{code}

Added 19/12/2019 by Tom de Jong.

The following allows us to use Agda's do-notation with the β₯β₯-monad.

Note that the Kleisli laws hold trivially, because β₯ X β₯ is a proposition for
any type X.

It is quite convenient when dealing with multiple, successive β₯β₯-rec calls.

Agda's do-notation is powerful, because it can be combined with pattern
matching, i.e. if
w κ β₯ fiber f y β₯,
then
x , p β w
is allowed in the do-block.

(Note that in Haskell, you would write "return" for our function β£_β£.)

\begin{code}

_>>=_ : {X : π€ Μ } {Y : π₯ Μ } β β₯ X β₯ β (X β β₯ Y β₯) β β₯ Y β₯
s >>= f = β₯β₯-rec β₯β₯-is-prop f s

\end{code}

\begin{code}

infixr 0 _β¨_

\end{code}