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