-- Martin Escardo, 7th August 2015

module propisset where

open import preliminaries
open import prop

Prp-isSet : {i : L}  isSet (Prp i)
Prp-isSet {i} = path-collapsible-isSet pc
 where
  A : (p q : Prp i)  U i
  A p q = (p holds  q holds) × (q holds  p holds) 
  A-isProp : (p q : Prp i)  isProp(A p q)
  A-isProp p q = isProp-closed-under-Σ (isProp-exponential-ideal  _  holdsIsProp q))
                                     _  isProp-exponential-ideal  _  holdsIsProp p))
  g : (p q : Prp i)  p  q  A p q
  g p q e = (b , c)
   where
    a : p holds  q holds
    a = ap _holds e
    b : p holds  q holds
    b = transport  X  X) a
    c : q holds  p holds
    c = transport  X  X) (sym a)
  h  : (p q : Prp i)  A p q  p  q 
  h p q (u , v) = propext u v 
  f  : (p q : Prp i)  p  q  p  q
  f p q e = h p q (g p q e)
  constant-f : (p q : Prp i) (d e : p  q)  f p q d  f p q e 
  constant-f p q d e = ap (h p q) (A-isProp p q (g p q d) (g p q e))
  pc : {p q : Prp i}  Σ \(f : p  q  p  q)  constant f
  pc {p} {q} = (f p q , constant-f p q)