Martin Escardo

\begin{code}

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

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

 βˆ₯βˆ₯-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

 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)

 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 (βˆ₯βˆ₯-rec i id) ∣_∣

 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}