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}