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