Martin Escardo & Chuangjie Xu, 2015.

We postulate the propositional truncation.

\begin{code}

module Continuity.PropositionalTruncation where

open import Preliminaries.SetsAndFunctions

postulate
  ∥_∥       : Set → Set
  ∥-∥-hprop : ∀{X : Set} → hprop ∥ X ∥
  ∣_∣       : {X : Set} → X → ∥ X ∥
  ∥-∥-elim  : ∀{X P : Set} → hprop P → (X → P) → ∥ X ∥ → P

\end{code}

Notice that this is a weaker form of truncation than that of the HoTT
book, because we don't assume f' ∣ x ∣ = f x definitionally. 

   ∣-∣
X ----> ∥ X ∥
 \        | 
  \       |
   \      |
    \     | 
  f  \    | f'  defined using elim and f
      \   |
       \  |
        v v
          P     a proposition

With the stronger version of the HoTT book, one gets function
extensionality, but this is not expected with the weaker version
considered here (although this is open at the time of writing).