```-- Martin Escardo, 3rd August 2015

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

module isprop where

open import preliminaries

-- A proposition is a type with at most one element:

isProp : {i : π} β Set i β Set i
isProp X = (x y : X) β x β‘ y

-- The two canonical examples:

π-isProp : {i : π} β isProp {i} π
π-isProp () ()

π-isProp : {i : π} β isProp {i} π
π-isProp zero zero = refl zero

isSet : {i : π} β Set i β Set i
isSet X = {x y : X} β isProp(x β‘ y)

constant : {i j : π} {X : Set i} {Y : Set j} β (f : X β Y) β Set(i β j)
constant f = β x y β f x β‘ f y

collapsible : {i : π} β Set i β Set i
collapsible X = Ξ£ \(f : X β X) β constant f

path-collapsible : {i : π} β Set i β Set i
path-collapsible X = {x y : X} β collapsible(x β‘ y)

isSet-is-path-collapsible : {i : π} {X : Set i} β isSet X β path-collapsible X
isSet-is-path-collapsible u = (Ξ» p β p) , u

path-collapsible-isSet : {i : π} {X : Set i} β path-collapsible X β isSet X
path-collapsible-isSet {i} {X} pc {x} {y} p q = claimβ
where
f : {x y : X} β x β‘ y β x β‘ y
f = prβ pc
g : {x y : X} (p q : x β‘ y) β f p β‘ f q
g = prβ pc
claimβ : {x y : X} (r : x β‘ y) β r β‘ trans (sym(f (refl x))) (f r)
claimβ (refl x) = sym-is-inverse (f(refl x))
claimβ : trans (sym (f (refl x))) (f p) β‘ trans (sym(f (refl x))) (f q)
claimβ = ap (Ξ» h β trans (sym(f (refl x))) h) (g p q)
claimβ : p β‘ q
claimβ = trans (trans (claimβ p) claimβ) (sym(claimβ q))

prop-is-path-collapsible : {i : π} {X : Set i} β isProp X β path-collapsible X
prop-is-path-collapsible h {x} {y} = ((Ξ» p β h x y) , (Ξ» p q β refl(h x y)))

prop-is-set : {i : π} {X : Set i} β isProp X β isSet X
prop-is-set h = path-collapsible-isSet(prop-is-path-collapsible h)

isProp-isProp : {i : π} {X : Set i} β isProp(isProp X)
isProp-isProp {i} {X} f g = claimβ
where
open import funext
lemma : isSet X
lemma = prop-is-set f
claim : (x y : X) β f x y β‘ g x y
claim x y = lemma (f x y) (g x y)
claimβ : (x : X) β f x β‘ g x
claimβ x = funext (claim x)
claimβ : f β‘ g
claimβ  = funext claimβ

isProp-closed-under-Ξ£ : {i j : π} {X : Set i} {A : X β Set j}
β isProp X β ((x : X) β isProp(A x)) β isProp(Ξ£ A)
isProp-closed-under-Ξ£ {i} {j} {X} {A} isx isa (x , a) (y , b) =
Ξ£-β‘ (isx x y) (isa y (transport A (isx x y) a) b)

isProp-exponential-ideal : {i j : π} {X : Set i} {A : X β Set j}
β ((x : X) β isProp(A x)) β isProp(Ξ  A)
isProp-exponential-ideal {i} {j} {X} {A} isa = lemma
where
open import funext
lemma : isProp(Ξ  A)
lemma f g = funext (Ξ» x β isa x (f x) (g x))
```