{-# OPTIONS --without-K #-}
{-# OPTIONS --rewriting #-}
module proptrunc where
open import preliminaries
open import prop
open import resize
β₯_β₯' : {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)
β₯β₯'-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)))
β₯_β₯ : {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)
β₯β₯-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)
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 β£_β£
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'
β₯β₯-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)
β₯β₯-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)