Martin Escardo

\begin{code}

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

module UF.PropTrunc where

open import MLTT.Plus-Properties
open import MLTT.Spartan
open import MLTT.Two-Properties
open import UF.Base
open import UF.Equiv
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

\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

exit-β₯β₯ : {P : π€ Μ } β is-prop P β β₯ P β₯ β P
exit-β₯β₯ i = β₯β₯-rec i id

β₯β₯-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) = exit-β₯β₯ i s , i (exit-β₯β₯ i 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

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

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

infixr -1 Exists
infixr -1 Β¬Exists

remove-truncation-inside-β : {X : π€ Μ } {Y : X β π₯ Μ }
β (β x κ X , β₯ Y x β₯)
β (β x κ X , Y x )
remove-truncation-inside-β =
β₯β₯-rec β-is-prop
(Ξ» (x , s) β β₯β₯-rec β-is-prop
(Ξ» y β β£ x , y β£) s)

Natβ : {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ } β Nat A B β β A β β B
Natβ ΞΆ = β₯β₯-functor (NatΞ£ ΞΆ)

_β¨_  : π€ Μ β π₯ Μ β π€ β π₯ Μ
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)

β¨-flip : {P : π€ Μ } {Q : π₯ Μ }
β P β¨ Q β Q β¨ P
β¨-flip = β₯β₯-functor (cases inr inl)

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 β£_β£

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 (exit-β₯β₯ i) β£_β£

equiv-to-own-truncation-implies-prop : {X : π€  Μ} β X β β₯ X β₯  β is-prop X
equiv-to-own-truncation-implies-prop {π€} {X} e = equiv-to-prop e β₯β₯-is-prop

not-existsβ-implies-forallβ : {X : π€ Μ } (p : X β π)
β Β¬ (β x κ X , p x οΌ β)
β β (x : X) β p x οΌ β
not-existsβ-implies-forallβ p u x =
different-from-β-equal-β (not-Ξ£-implies-Ξ -not (u β β£_β£) x)

forallβ-implies-not-existsβ : {X : π€ Μ } (p : X β π)
β (β (x : X) β p x οΌ β)
β Β¬ (β x κ X , p x οΌ β)
forallβ-implies-not-existsβ {π€} {X} p Ξ± = β₯β₯-rec π-is-prop h
where
h : (Ξ£ x κ X , p x οΌ β) β π
h (x , r) = zero-is-not-one (r β»ΒΉ β Ξ± x)

forallβ-implies-not-existsβ : {X : π€ Μ } (p : X β π)
β (β (x : X) β p x οΌ β)
β Β¬ (β x κ X , p x οΌ β)
forallβ-implies-not-existsβ {π€} {X} p Ξ± = β₯β₯-rec π-is-prop h
where
h : (Ξ£ x κ X , p x οΌ β) β π
h (x , r) = one-is-not-zero (r β»ΒΉ β Ξ± x)

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