-- Martin Escardo, 13 September 2017, based on earlier ideas and Agda files.

-- Propositional truncation, by resizing the large propositional
-- truncation, rather than using Voevodsky's resizing of all
-- propositions.

{-# OPTIONS --without-K #-}
{-# OPTIONS --rewriting #-} -- Needed because we import resize which relies on that.
                            -- Only this module in this development should use rewriting
                            -- (and the general purpose module resize.lagda used here).
module proptrunc where

open import preliminaries
open import prop
open import resize          -- Only this module in this development should use resize.

-- Large propositional truncation first:

βˆ₯_βˆ₯' : {i : 𝕃} β†’ U i β†’ U(lsuc i)
βˆ₯ X βˆ₯' = (p : Prp) β†’ (X β†’ p holds) β†’ p holds

∣_∣' : {i : 𝕃} {X : U i} β†’ X β†’ βˆ₯ X βˆ₯'
∣ x ∣' = Ξ» _ f β†’ f x

βˆ₯βˆ₯'-rec : {i : 𝕃} {X : U i} {P : U i} β†’ isProp P β†’ (X β†’ P) β†’ βˆ₯ X βˆ₯' β†’ P
βˆ₯βˆ₯'-rec {i} {X} {P} isp Ο† s = s ( P , isp ) Ο†

βˆ₯βˆ₯'-rec-comp : {i : 𝕃} {X : U i} {P : U i}
            β†’ {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 : 𝕃} {X : U i} β†’ isProp βˆ₯ X βˆ₯'
βˆ₯βˆ₯'-isProp {i} {X} s t = lemmaβ‚€
 where
  open import funext
  lemmaβ‚€ : s ≑ t
  lemmaβ‚€ = funext (Ξ» p β†’ funext (Ξ» f β†’ holdsIsProp p (s p f) (t p f)))

-- Then we resize it to make it small:

βˆ₯_βˆ₯ : {i : 𝕃} β†’ U i β†’ U i
βˆ₯ X βˆ₯ = resize βˆ₯ X βˆ₯'

private increase' : {i : 𝕃} {X : U i} β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ X βˆ₯'
increase' = resize-in

private decrease' : {i : 𝕃} {X : U i} β†’ βˆ₯ X βˆ₯' β†’ βˆ₯ X βˆ₯
decrease' = resize-out

decrease-increase' : {i : 𝕃} {X : U i} (s : βˆ₯ X βˆ₯)
                  β†’ decrease'(increase' s) ≑ s
decrease-increase' = refl

increase-decrease' : {i : 𝕃} {X : U i} (s' : βˆ₯ X βˆ₯')
                  β†’ increase'(decrease' s') ≑ s'
increase-decrease' = refl

∣_∣ : {i : 𝕃} {X : U i} β†’ X β†’ βˆ₯ X βˆ₯
∣ x ∣ = decrease' ∣ x ∣'

βˆ₯βˆ₯-rec : {i : 𝕃} {X : U i} {P : U i} β†’ isProp P β†’ (X β†’ P) β†’ βˆ₯ X βˆ₯ β†’ P
βˆ₯βˆ₯-rec {i} {X} {P} isp Ο† s = βˆ₯βˆ₯'-rec {i} {X} {P} isp Ο† (increase' s)

-- The computation rule is definitional:

βˆ₯βˆ₯-rec-comp : {i : 𝕃} {X : U i} {P : U i} {isp : isProp P} (Ο† : X β†’ P) (x : X)
            β†’  βˆ₯βˆ₯-rec isp Ο† ∣ x ∣ ≑ Ο† x
βˆ₯βˆ₯-rec-comp {i} {X} {P} {isp} Ο† x = refl (Ο† x)

βˆ₯βˆ₯-isProp : {i : 𝕃} {X : U i} β†’ isProp βˆ₯ X βˆ₯
βˆ₯βˆ₯-isProp {i} {X} s t = ap decrease' lemma
 where
  open import funext
  lemma : increase' s ≑ increase' t
  lemma = βˆ₯βˆ₯'-isProp (increase' s) (increase' t)

-- We don't need increase' and decrease' now that we have βˆ₯βˆ₯-rec and
-- βˆ₯βˆ₯-isProp defined from them:

increase : {i : 𝕃} {X : U i}  β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ X βˆ₯'
increase s p f = βˆ₯βˆ₯-rec (holdsIsProp p) f s

decrease : {i : 𝕃} {X : U i}  β†’ βˆ₯ X βˆ₯' β†’ βˆ₯ X βˆ₯
decrease = βˆ₯βˆ₯'-rec βˆ₯βˆ₯-isProp ∣_∣

-- But then of course we don't get the following as definitional
-- equalities, as we do with increase' and decrease':

decrease-increase : {i : 𝕃} {X : U i} (s : βˆ₯ X βˆ₯)
                  β†’ decrease(increase s) ≑ s
decrease-increase s = βˆ₯βˆ₯-isProp (decrease (increase s)) s

increase-decrease : {i : 𝕃} {X : U i} (s' : βˆ₯ X βˆ₯')
                  β†’ increase(decrease s') ≑ s'
increase-decrease s' = βˆ₯βˆ₯'-isProp (increase (decrease s')) s'

-- Induction on βˆ₯ X βˆ₯ follows from recursion, as usual:

βˆ₯βˆ₯-ind : {i : 𝕃} {X : U i} {P : βˆ₯ X βˆ₯ β†’ U i} β†’ ((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 : 𝕃} {X : U i} {P : βˆ₯ X βˆ₯ β†’ U i}
              (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)