-- Martin Escardo, 3rd August 2015.

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

module prop where

open import preliminaries
open import isprop public

-- The type of small propositions is large:
Prop : {i : 𝕃}  U(lsuc i)
Prop{i} = Σ \(P : U i)  isProp P

-- Destructors:

_holds : {i : 𝕃}  Prop{i}  U i
_holds = pr₁

holdsIsProp : {i : 𝕃} (p : Prop{i})  isProp(p holds)
holdsIsProp = pr₂

-- The idea of the terminology is that we cannot assert a point of the
-- type Prop, as it is a pair, but we can assert that it holds, meaning
-- that we assert that its first component has an inhabitant, as it is
-- a truth-value (a type P with the asserted side-condition isProp P).

-- We have the following judgemental equalities:
-- 
--    (β₁)   ( P , isp ) holds = P,
--    (β₂)   holdsIsProp ( P , isp ) = isp,
--    (η)    p = ( p holds , holdsIsProp p ).

-- NB. holdsIsProp shows that _holds is an embedding in the sense of
-- the HoTT book https://homotopytypetheory.org/book/.

Prop-≡ : {i : 𝕃} {p q : Prop{i}}  p holds  q holds  p  q
Prop-≡ {i} {p} {q} e = e'
 where 
   e' : p  q
   e' = Σ-≡ e (isProp-isProp (transport isProp e (holdsIsProp p)) (holdsIsProp q))

-- Propositional univalence says that any two (logically) equivalent
-- propositions are equal:

postulate propua : {i : 𝕃} {P Q : U i}  isProp P  isProp Q  (P  Q)  (Q  P)  P  Q

-- It can be formulated as follows:

propext : {i : 𝕃} {p q : Prop{i}}  (p holds  q holds)  (q holds  p holds)  p  q
propext {i} {p} {q} f g = Prop-≡ (propua (holdsIsProp p) (holdsIsProp q) f g)