Martin Escardo, Jun 7 2013.

We use Dan Licata's trick 
http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
to implement hpropositional truncation so that the elimination-rule equations hold definitionally.

\begin{code}

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

module hprop-truncation where

open import tiny-library

\end{code}

We implement the hpropositional truncation of ∥ X ∥ as X itself, or
rather its isomorphic copy ∥ X ∥', which is kept private to the
module:

\begin{code}

private
 data ∥_∥' (X : Set) : Set where
   ∣_∣' : X → ∥ X ∥'

∥_∥ : Set → Set
∥_∥ = ∥_∥'

postulate truncation-path : {X : Set} → hprop ∥ X ∥

∣_∣ : {X : Set} → X → ∥ X ∥
∣_∣ = ∣_∣'

truncation-ind : {X : Set} {P : ∥ X ∥ → Set} → ((s : ∥ X ∥) → hprop(P s)) → ((x : X) → P ∣ x ∣)
               → (s : ∥ X ∥) → P s
truncation-ind _ f ∣ x ∣' = f x

truncation-rec : {X P : Set} → hprop P → (X → P) → ∥ X ∥ → P
truncation-rec _ f ∣ x ∣' = f x

\end{code}

The crucial point is that the above two elimination rules hold
definitionally. Because of the postulate, we lose canonicity.