-- Martin Escardo, 5th August 2015. Modified 9 May to add rewriting to conform with prop.agda.

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

module propisset where

open import preliminaries
open import prop

Prop-isSet : isSet Prop
Prop-isSet = path-collapsible-isSet pc
 where
  A : (p q : Prop)  U₀
  A p q = (p holds  q holds) × (q holds  p holds) 
  A-isProp : (p q : Prop)  isProp(A p q)
  A-isProp p q = isProp-closed-under-Σ (isProp-exponential-ideal  _  holdsIsProp q))
                                        _  isProp-exponential-ideal  _  holdsIsProp p))
  g : (p q : Prop)  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 : Prop)  A p q  p  q 
  h p q (u , v) = propext u v 
  f  : (p q : Prop)  p  q  p  q
  f p q e = h p q (g p q e)
  constant-f : (p q : Prop) (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 : Prop}  Σ \(f : p  q  p  q)  constant f
  pc {p} {q} = (f p q , constant-f p q)