-- 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))