-- Martin Escardo, 3rd August 2015, originally using type-in-type.
-- 9 May 2016, now using rewriting rather than type-in-type.

{-

 Users of this module need to use the option "rewriting" like this:
 {-# OPTIONS --rewriting #-}

 We use Abel and Cockx's rewriting feature for Agda to get
 impredicativity à la Voevodsky (propositional resizing) in Agda.

 See the module resize.agda.

-}

{-# OPTIONS --without-K #-} 
{-# OPTIONS --rewriting #-} -- Needed for the import resize.agda to work.

module prop where

open import preliminaries
open import isprop public
open import resize -- Don't make public, as it is inconsistent in general.

-- The type of small propositions is large:
PropLarge : U₁
PropLarge = Σ \(P : U₀)  isProp P

-- We make it small:
Prop : U₀
Prop = resize PropLarge

-- The above corresponds to Voevodsky's resizing rule RR2.  
-- Notational convention:
--
--   Upper case P, Q, R : U₀,  when we have isProp P, isProp Q, isProp R.
--   Lower case p, q, r : Prop.

-- Constructor:

₍_,_₎ : (P : U₀)  isProp P  Prop
 P , isp  = resize-in(P , isp)

-- Destructors:

_holds : Prop  U₀
p holds = pr₁(resize-out p) 

holdsIsProp : (p : Prop)  isProp(p holds)
holdsIsProp p = pr₂(resize-out p)

-- 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/.

-- The following corresponds the Voevodky's resizing rule RR1:

resize₁ : {i : Level} (P : U i)  isProp {i} P  U₀
resize₁ P isp = resize P

-- We also need the following to make the above work:

resize₁-in : {i : Level} {P : U i} (isp : isProp {i} P)  P  resize₁ P isp
resize₁-in isp = resize-in

resize₁-out : {i : Level} {P : U i} (isp : isProp {i} P)  resize₁ P isp  P
resize₁-out isp = resize-out

-- The functions (resize₁-in isp) and (resize₁-out isp) form a judgemental
-- isomorphism.  Here is a typical example where the above two
-- functions are needed:

resize₁-isProp : {i : Level} {P : U i}  (isp : isProp {i} P)  isProp (resize₁ {i} P isp) 
resize₁-isProp {i} {P} isp p q = ap (resize₁-in isp) (isp (resize₁-out isp p) (resize₁-out isp q))

-- We also need the following judgemental isomorphism:

Prop-out : Prop  PropLarge
Prop-out = resize-out

Prop-in : PropLarge  Prop
Prop-in = resize-in

-- Here is a typical example where these functions are needed (because
-- the equality in the premise, being of two types in U₀, is in U₁,
-- whereas that of the conclusion, being of the type Prop, is in U₀) :

Prop-≡ : {p q : Prop}  p holds  q holds  p  q
Prop-≡ {p} {q} e = ap Prop-in e'
 where 
   e' : Prop-out p  Prop-out 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 : Level} {P Q : U i}  isProp P  isProp Q  (P  Q)  (Q  P)  P  Q

-- It can be formulated as follows:

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