-- Martin Escardo, 3rd August 2015, modified 9 May to add the rewriting option only.

-- Propositional truncation.

{-# OPTIONS --without-K #-}
{-# OPTIONS --rewriting #-} -- Needed because we import prop which now relies on that.

module proptrunc where

open import preliminaries
open import prop

-- Propositional truncation first:

∥_∥ : {i : Level} → U i → U i
∥ X ∥ = (p : Prop) → (X → p holds) → p holds

-- Here ∥ X ∥ is ranged over by s and t.

∣_∣ : {i : Level} {X : U i} → X → ∥ X ∥
∣ x ∣ = λ _ f → f x

∥∥-rec : {i : Level} {X : U i} {P : U₀} → isProp P → (X → P) → ∥ X ∥ → P
∥∥-rec {i} {X} {P} isp φ s = s ₍ P , isp ₎ φ

∥∥-rec-comp : {i : Level} {X : U i} {P : U₀}
            → {isp : isProp P} (φ : X → P) (x : X) →  ∥∥-rec isp φ ∣ x ∣ ≡ φ x
∥∥-rec-comp φ x = refl(φ x)

-- To have that ∥ X ∥ is a proposition we need function extensionality. 
-- In fact, assuming that ∥ X ∥ is a proposition gives function extensionality 
-- (proof omitted here).

∥∥-isProp : {i : Level} {X : U i} → isProp ∥ X ∥
∥∥-isProp s t = lemma
 where
  open import funext
  lemma : s ≡ t
  lemma = funext (λ p → funext (λ f → holdsIsProp p (s p f) (t p f)))

-- Induction on ∥ X ∥ follows from recursion:

∥∥-ind : {i : Level} {X : U i} {P : ∥ X ∥ → U₀} → ((s : ∥ X ∥) → isProp(P s))
       → ((x : X) → P ∣ x ∣) →  (s : ∥ X ∥) → P s
∥∥-ind {i} {X} {P} isp φ s = ∥∥-rec (isp s) ψ s
 where
  ψ : X → P s
  ψ x = transport P (∥∥-isProp ∣ x ∣ s) (φ x)

-- There should be a way of defining ∥∥-ind so that its computation
-- rule holds definitionally (using the ideas of the file hsetfunext
-- elsewhere). For the above definition, it only holds
-- propositionally:

∥∥-ind-comp : {i : Level} {X : U i} {P : ∥ X ∥ → U₀}
              (isp : (s : ∥ X ∥) → isProp(P s)) (φ : (x : X) → P ∣ x ∣)
            → (x : X) → ∥∥-ind isp φ ∣ x ∣ ≡ φ x
∥∥-ind-comp isp φ x = isp ∣ x ∣ (∥∥-ind isp φ ∣ x ∣) (φ x)