1. Cartesian products of propositions and sets
  2. To be a proposition or a set is a proposition
  3. Type embeddings
  4. Subtypes
  5. The types of Propositions and Sets
  6. Propositional extensionality
  7. The powerset
    1. Universal family
    2. A universal proposition
    3. The powerset classifies type embeddings
  8. Propositional resizing
    1. Resizing is a proposition
    2. Smallness
    3. Excluded Middle implies Propositional Resizing
    4. Propositional impredicativity

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

module more-logic where 

open import mltt
open import twocatconstructions
open import basichomotopy
open import sets-logic
open import univalence-base
open import funext-equiv
open import univalence-funext

open ≡-Reasoning
open ◾-lemmas

Cartesian products of propositions and sets

We have seen that one way to express function extensionality is to say that the Cartesian product of singletons is a singleton, as expressed by the vfunext axiom. What about propositions?

The corresponding statement holds as a consequence of function extensionality:

Π-prop-is-prop :  { ℓ'} (dfe : dfunext  ℓ') {A : Set } {P : A  Set ℓ'}  
                 ((x : A)  isProp (P x))  isProp (Π A P)
Π-prop-is-prop dfe is f g =  dfe f g γ
    γ : f ~ g
    γ x = is x (f x) (g x)

A similar statement holds for sets, under the same assumptions (except it is moreconvenient to assume function extensionality in the form of hfunext):

Π-set-is-set :  { ℓ'} (hfe : hfunext  ℓ') {A : Set } {P : A  Set ℓ'}  
               ((x : A)  isSet (P x))  isSet (Π A P)
Π-set-is-set {} {ℓ'} hfe {A} {P} ip = isSet'→isSet (Π A P) i 
    dfe : dfunext  ℓ'
    dfe = hfunext→dfunext hfe

    i : isSet' (Π A P)
    i f g = j
        open ≃-lemmas
        k : isProp (f ~ g)
        k p q = dfe p q γ
            γ : (x : A)  p x   q x
            γ x = ip x (f x , g x) (p x , q x)

        eq : (f ~ g)  (f  g)
        eq = (happly f g , hfe f g) ≃⁻¹
        j : isProp (f  g)
        j = weak-equivalences-preserve-props k eq

Recall that a corresponding stetement concerning Σ-types of proposition holds without assuming any axioms.

top ⇑

To be a proposition or a set is a proposition

Under function extensionality, to be a proposition (i.e. to be path connected), or to be a singleton (i.e. to be contractible) are themselves propositions:

isProp-is-Prop :  {} (dfe : dfunext  ) {A : Set }  isProp (isProp A)
isProp-is-Prop dfe {A} f g =  dfe f g γ
    γ : f ~ g
    γ a = dfe (f a) (g a) γ₁
        γ₁ : f a ~ g a
        γ₁ a' = prop-is-set f ((a , a')) ((f a a') , (g a a'))

-- variant with explicit variable
isProp-is-Prop' :  {} (dfe : dfunext  ) (A : Set )  isProp (isProp A)
isProp-is-Prop' dfe A = isProp-is-Prop dfe {A}

isSet-is-Prop :  {} (dfe : dfunext  ) {A : Set }  isProp (isSet A)
isSet-is-Prop dfe {A} f g = dfe f g γ
    γ : f ~ g
    γ (a₁ , a₂) = dfe (f (a₁ , a₂)) (g (a₁ , a₂)) γ₁
        γ₁ : f (a₁ , a₂) ~ g (a₁ , a₂)
        γ₁ (p , q) = prop-is-set (isSet→isSet' A f a₁ a₂) (p , q) ((f (a₁ , a₂) (p , q)) , (g (a₁ , a₂) (p , q)))

top ⇑

Type embeddings

We say that f : A → B is an embedding if its (homotopy) fibers are mere propositions:
is-embedding :  { ℓ'} {A : Set } {B : Set ℓ'}  (A  B)  Set (  ℓ')
is-embedding f = Π[ b  codomain f ] (isProp (hfib f b))
Given any two types, we can define the type of embeddings as follows
_↪_ :  { ℓ'} (A : Set ) (B : Set ℓ')  Set (  ℓ')
A  B = Σ[ f  (A  B) ] (is-embedding f)
Once again, to be a an embedding is a mere proposition, once we assume function extensionality, which we must assume at two different level pairs:1
is-embedding-is-Prop :  { ℓ'} (dfe : dfunext ℓ' (  ℓ')) (dfe' : dfunext (  ℓ') (  ℓ'))
                       {A : Set } {B : Set ℓ'} (f : A  B)  isProp (is-embedding f)
is-embedding-is-Prop dfe dfe' f i₁ i₂ = dfe i₁ i₂ γ
    γ : i₁ ~ i₂
    γ y = isProp-is-Prop dfe' (i₁ y) (i₂ y)

top ⇑


Givena a dependent type P : A → 𝓤, we may regard each type P x as a proposition, and hence P itself as a predicate on A. Pursuind this idea, one would be led to define an analogue of { x ∈ A ∣ P x } in Type Theory. The obvious choice would be the Σ-type Σ[ x ∈ A ] P x, except that there could be different pairs projecting to the same term x : A: in other words, one might have different proofs of P x. This potential lack of uniqueness hinders the viability of this approach.

The problem is that just picking a dependent type is too generic an approach. This is not the case for mere propositions: if P : A → 𝓤 is a dependent type such that all P x are mere propositions, then for any two pairs u v : Σ A P such that p : π₁ u ≡ π₁ v, it follows that u ≡ v, as indeed we show:

fiber-props-id-base-give-identities :  { ℓ'} {A : Set } {P : A  Set ℓ'}  ((x : A)  isProp (P x)) 
        (u v : Σ A P)  π₁ u  π₁ v  u  v
fiber-props-id-base-give-identities {P = P} isp u v p = PathPair→PathΣ pp
    pp : u  v
    Σ.fst pp = p
    Σ.snd pp = isp (π₁ v) (transport P p (π₂ u)) (π₂ v)
This gives a more solid meaning to { x ∈ A ∣ P x }, which we should refer to as a subtype of A. In fact, we are justified in claiming that P itself is a subtype of A, because the corresponding Σ-type is in fact embedded in A in the sense specified above.
π₁-is-embedding :  { ℓ'} {A : Set } {P : A  Set ℓ'} 
                  ((x : A)  isProp (P x))  is-embedding (π₁ {E = P})
π₁-is-embedding {} {ℓ'} {A} {P} isp x =  γ
    open ≃-lemmas
    p₁ : Σ A P  A
    p₁ = π₁ {E = P}
    w : hfib p₁ x  P x
    w = hfib-of-proj-equiv-fiber x

    γ : isProp (hfib p₁ x)
    γ = weak-equivalences-preserve-props (isp x) (w ≃⁻¹)

top ⇑

The types of Propositions and Sets

In a given universe we can collect the types that “are” propositions and sets by forming the appropriate Σ-types:2

Props :    Set (lsuc )
Props  = Σ[ A  (Set ) ] (isProp A)

Sets :    Set (lsuc )
Sets  = Σ[ A  (Set ) ] (isSet A)

It is customary to use the name Ω for Props, and it is convenient to change the name of Sets to avoid confusion:

Ω 𝓔 :    Set (lsuc )
Ω = Props
𝓔 = Sets

Assuming function extensionality (implied by univalence) we obtain that Propositions and Sets are subtypes of their container universes:

Props-embedding :  {} (dfe : dfunext  )  (is-embedding {lsuc } (π₁ {E = λ A  isProp A}))
Props-embedding {} dfe = π₁-is-embedding is
    is : (A : Set )  isProp (isProp A)
    is A = isProp-is-Prop dfe {A}

Props-is-subtype :  {} (dfe : dfunext  )  Ω   Set 
Props-is-subtype dfe = π₁ {E = λ A  isProp A} , Props-embedding dfe

and similarly for sets:

Sets-embedding :  {} (dfe : dfunext  )  (is-embedding {lsuc } (π₁ {E = λ A  isSet A}))
Sets-embedding {} dfe = π₁-is-embedding is
    is : (A : Set )  isProp (isSet A)
    is A = isSet-is-Prop dfe {A}

Sets-is-subtype :  {} (dfe : dfunext  )  𝓔   Set 
Sets-is-subtype dfe = π₁ {E = λ A  isSet A} , Sets-embedding dfe

Note the level at which we assume function extensionality is ℓ: these propositions can be cleanly implied assuming univalence at the same level.

These propositions have the following important consequence: if, say, we have two “sets”, namely two pairs (A , i) and (B , j) consisting of a type and a proof that it is a set, then an identification p : A ≡ B yields, under univalence, an identification (A , i) ≡ (B , j).

Sets-equality :  {} (dfe : dfunext  ) ((A , i) (B , j) : 𝓔 )  A  B  (A , i)  (B , j)
Sets-equality {} dfe (A , i) (B , j) p = fiber-props-id-base-give-identities isp (A , i) (B , j) p
    isp : (A : Set )  isProp (isSet A)
    isp A = isSet-is-Prop dfe {A}

and, of course, the same holds for propositions:

Props-equality :  {} (dfe : dfunext  ) ((A , i) (B , j) : Ω )  A  B  (A , i)  (B , j)
Props-equality {} dfe (A , i) (B , j) p = fiber-props-id-base-give-identities isp (A , i) (B , j) p
    isp : (A : Set )  isProp (isProp A)
    isp A = isProp-is-Prop dfe {A}

Finally, we use fiber-props-id-base-give-identities to show that being a singleton, i.e. contractible, is again a proposition:

isSingleton-is-Prop :  {} (dfe : dfunext  ) {A : Set } 
                      isProp (isSingleton A)
isSingleton-is-Prop {} dfe {A} (a , γ) (a₁ , γ₁) = p
    ip : isProp A
    ip = singleton→prop A (a , γ)

    is : isSet A
    is = prop-is-set ip

    δ : (a : A)  isProp (Π[ x  A ] (a  x) )
    δ a  f g = Π-prop-is-prop dfe φ f g
        φ : (x : A)  isProp (a  x)
        φ x = i
            i : isProp (a  x)
            i q q₁ = is (a , x) (q , q₁)
    p : (a , γ)  (a₁ , γ₁)
    p = fiber-props-id-base-give-identities δ (a , γ) (a₁ , γ₁) (γ a₁)

Propositional extensionality

We know two logically equivalent propositions are weakly equivalent; more precisely, their underlying types are. Under univalence, their underlying types would be equal and hence the propositions would be equal as propositions. We can extract this as a principle, which is called Propositional extensionality:

propext :    Set (lsuc )
propext  = {A B : Set }  isProp A  isProp B  (A  B)  (B  A)  A  B

As for the other principles (axioms) we can of course formulate a global version:

Propext : Setω
Propext =    propext 

Therefore univalence implies propositional extensionality:

univalence→propext :  {} (ua : is-univalent )  propext 
univalence→propext {} ua ia ib f g = Eq→Id A B (prop-logical-eq-is-eq ia ib f g)
    open U-Rules ua
    A B : Set 
    A = domain f
    B = domain g

and in turn, still assuming univalence, we obtain that logical equivalence implies identity of propositions:

prop-logical-eq-is-id :  {} (ua : is-univalent ) ((A , i) (B , j) : Ω ) 
                        (A  B)  (B  A)  (A , i)  (B , j)
prop-logical-eq-is-id {} ua (A , i) (B , j) f g = Props-equality {} dfe (A , i) (B , j) p
    open U-Rules ua

    dfe : dfunext  
    dfe = univalence→dfunext ua

    p : A  B
    p = univalence→propext ua i j f g

The type of propositions is extensional if the following sense:

Ω-ext :  {}  dfunext    propext   (P Q : Ω ) 
        (π₁ P  π₁ Q)  (π₁ Q  π₁ P)  P  Q
Ω-ext dfe pe P Q f g = fiber-props-id-base-give-identities 
                         (isProp-is-Prop' dfe) P Q (pe (π₂ P) (π₂ Q) f g)

When both the function and propositional extensionality axioms hold, the type Ω ℓ is a set:

Ω-is-set :  {}  dfunext    propext   isSet (Ω )
Ω-is-set {} dfe pe = path-collapsible→isSet pc 

    leq : (P Q : Ω )  Set  
    leq P Q = (π₁ P  π₁ Q) × (π₁ Q  π₁ P)

    γ : (P Q : Ω )  isProp (leq P Q)
    γ P Q = Σ-type-isprop ipq  _  iqp)
        ipq : isProp (π₁ P  π₁ Q)
        ipq = Π-prop-is-prop dfe  _  π₂ Q)
        iqp : isProp (π₁ Q  π₁ P)
        iqp = Π-prop-is-prop dfe  _  π₂ P)

    f : (P Q : Ω )  leq P Q  P  Q
    f P Q (u , v) = Ω-ext dfe pe P Q u v

    g : (P Q : Ω )  P  Q  leq P Q
    g P Q z = u , v
        z' : π₁ P  π₁ Q
        z' = ap π₁ z
        u : π₁ P  π₁ Q
        u = Id→Fun z'
        v : π₁ Q  π₁ P
        v = Id→Fun (z' ⁻¹)
    h : (P Q : Ω )  P  Q  P  Q
    h P Q z = f P Q (g P Q z)

    -- h is constant
    η : (P Q : Ω ) (z w : P  Q)  h P Q z  h P Q w
    η P Q z w = ap  t  f P Q t) (γ P Q (g P Q z) (g P Q w))

    pc : path-coll (Ω )
    pc P Q = h P Q , η P Q

top ⇑

The powerset

For any type A : Set ℓ the function type A → Ω ℓ' ought to be interpreted as the “type of subtypes of A:” this is natural in light of π₁-is-embedding defined in Subtypes. Indeed, a function term p : A → Ω ℓ' unpacks, for each a : A, into a pair π₁ (p a) , π₂ (p a), where π₁ (p a) : Set ℓ' and π₂ (p a) : isProp ( π₁ (p a) ). Comparing with the description in Subtypes, this is precisely a subtype of A.

Conversely, a subtype {x ∈ A ∣ P x} clearly determines a function p : A → Ω ℓ'

Thus Ω ℓ' is a classifier for the subtypes. We refer to the function type A → Ω ℓ' as the powerset of A:
𝓟 :  { ℓ'}  Set   Set (  lsuc ℓ')
𝓟 {} {ℓ'} A = A  Ω ℓ'
Powersets are always sets, even for types that non necessarily are sets:
powerset-is-set :  { ℓ'}  hfunext  (lsuc ℓ')  hfunext ℓ' ℓ'  propext ℓ'  
                  {A : Set }  isSet (𝓟 {} {ℓ'} A)
powerset-is-set {} {ℓ'} hfe hfe' pe = Π-set-is-set hfe  x  Ω-is-set dfe' pe)
    dfe' : dfunext ℓ' ℓ'
    dfe' = hfunext→dfunext hfe'

Universal family

We can introduce the universal family of propositions over Ω ℓ that to any proposition assigns the underlying type:
𝓟rop :  {}  Ω   Set 
𝓟rop (P , i) = P
Note that 𝓟rop is another name for the first projection from Ω ℓ, and we have already proved it is an embedding under function extensionality:
𝓟rop-embedding :  {}  dfunext    is-embedding {lsuc } 𝓟rop
𝓟rop-embedding = Props-embedding
The second projection is a tautological proof that each term of the universal family is a proposition:
𝓘ₚ :  {}  (P : Ω )  isProp (𝓟rop P)
𝓘ₚ (P , i) = i

Using the notions of universal proposition and its proof we can show (using function extensionality) that the powerset of A is equivalent to the type of propositions parametrized by A (i.e. dependent types that fiberwise propositions).

powerset→fiberwise-prop :  { ℓ'} {A : Set }  𝓟 {} {ℓ'} A  
                          Σ[ P  (A  Set ℓ') ] ( (x : A)  isProp (P x) )
powerset→fiberwise-prop f = (𝓟rop ∘′ f) , (𝓘ₚ  f)

fiberwise-prop→powerset :  { ℓ'} {A : Set }  Σ[ P  (A  Set ℓ') ] ( (x : A)  isProp (P x) )  
                          𝓟 {} {ℓ'} A
fiberwise-prop→powerset (P , i) = λ x  P x , i x

powerset≃fiberwise-prop :  { ℓ'} (dfe : dfunext  (lsuc ℓ')) {A : Set }  
                          Σ[ P  (A  Set ℓ') ] ( (x : A)  isProp (P x) )  𝓟 {} {ℓ'} A
powerset≃fiberwise-prop {} {ℓ'} dfe {A} = e
    open Univ-Cart-Prod
    e : Σ[ P  (A  Set ℓ') ] ( (x : A)  isProp (P x) )  𝓟 {} {ℓ'} A
    e = ΣΠ-univ-is-equiv {A = A} dfe

A universal proposition

To continue the construction of our universal object, consider the global Σ-type:
Ω̂ :    Set (lsuc )
Ω̂  = Σ (Ω ) 𝓟rop

 :  {}  Ω̂   Ω 
 = π₁ {E = 𝓟rop}

A term of Ω̂ ℓ is a triple P , i , u, where P , i is a proposition and u : P. The type Ω̂ ℓ is “universally” and “tautologically” embedded in Ω ℓ, because is an embedding by virtue of 𝓟rop-embedding.

The powerset classifies type embeddings

The upshot is that the powerset classifies embeddings by pulling back the universal object p̂ : Ω̂ ℓ → Ω ℓ, in the sense that any embedding f : A → B, where A : Set ℓ and B : Set ℓ', arises from a diagram of the form

\[ \begin{array}{ccc} A & \longrightarrow & \hat Ω ℓ' \\ \downarrow & & \downarrow \\ B & \longrightarrow & Ω ℓ' \end{array} \]

i.e. pulling back p̂ : Ω̂ ℓ → Ω ℓ along a term of the powerset 𝓟 B = B → Ω ℓ'.

First, starting from an embedding, let us construct the diagram. We just need to build a couple of functions: χ : B → Ω' and χ̂ : A → Ω̂.
embedding→powerset :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B)  (B  Ω (  ℓ'))
embedding→powerset (f , i) = λ x  (hfib f x) , (i x)
whereas the function to the total space is
embedding→univ-prop :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B)  (A  Ω̂ (  ℓ'))
embedding→univ-prop (f , i) = λ x  (hfib f (f x) , i (f x)) , x , refl
The diagram commutes:
diagram-univ-prop-commutes :  { ℓ'} (dfe : dfunext  (lsuc   lsuc ℓ')) {A : Set } {B : Set ℓ'} (f : A  B) 
                              ∘′ (embedding→univ-prop f)  (embedding→powerset f) ∘′ (π₁ f)
diagram-univ-prop-commutes dfe f = dfe (( ∘′ χ̂)) ((χ ∘′ (π₁ f))) γ
    χ = embedding→powerset f
    χ̂ = embedding→univ-prop f

    γ : ( ∘′ χ̂) ~ (χ ∘′ (π₁ f))
    γ x = refl

In the opposite direction, given a term in the powerset of B we should be able to reconstruct a type A and embedding f : A → B. The first step is to pull back the universal proposition to B. We can write two possible definitions: one by writing an ad hoc fiber product, the other by pulling back the dependent type, as we have done in the past. (Note they belong to different universes.3)

pullback-univ-prop :  {ℓ' ℓ''} {B : Set ℓ'} (χ : B  Ω  ℓ'')  Set (ℓ'  (lsuc ℓ''))
pullback-univ-prop {ℓ'} {ℓ''} {B} χ = Σ (B × Ω̂  ℓ'')  (b , u)  χ b   u)

pullback-univ-prop' :  {ℓ' ℓ''} {B : Set ℓ'} (χ : B  Ω ℓ'')  Set (ℓ'  ℓ'')
pullback-univ-prop' {ℓ'} {ℓ''} {B} χ = Σ[ b  B ] ( 𝓟rop (χ b) )
We can prove this is an embedding into B:
pullback-univ-prop-is-embedding :  {ℓ' ℓ''} {B : Set ℓ'} (χ : B  Ω (ℓ'')) 
                                  pullback-univ-prop' {ℓ'} χ  B
Σ.fst (pullback-univ-prop-is-embedding {ℓ'} χ) = λ u  π₁ u
Σ.snd (pullback-univ-prop-is-embedding {ℓ'} χ) b = k
    j : isProp (𝓟rop (χ b))
    j = π₂ (χ b)

    B : Set ℓ'
    B = domain χ
    p : pullback-univ-prop' {ℓ'} χ  B
    p = π₁

    e : 𝓟rop (χ b)  hfib p b
    e = (hfib-of-proj-equiv-fiber b) ≃⁻¹
        open ≃-lemmas

    k : isProp (hfib p b)
    k = weak-equivalences-preserve-props j e 
For this to be meaningful, the two processes must be inverses of one another. At lease we should be able to recover the embedding from the classifying map, which is what we do. We prove that if we have an embedding f : A → B, then A must be equivalent to the pullback of the universal proposition.
classifying-prop-is-equiv :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B) 
                            A  pullback-univ-prop' {ℓ'} (embedding→powerset f)
classifying-prop-is-equiv {} {ℓ'} {A} {B} (f , i) = lemma2 ≃◾≃ (lemma1 ≃⁻¹)
    open ≃-lemmas 
     : Set (  ℓ')
     = pullback-univ-prop' {ℓ'} (embedding→powerset (f , i))
    lemma1 :   Σ[ b  B ] (hfib f b)
    Σ.fst lemma1 = λ { (b , u)  b , u}
    Σ.fst (Σ.snd lemma1) = id , λ _  refl
    Σ.snd (Σ.snd lemma1) = id , λ _  refl

    lemma2 : A  Σ[ b  B ] (hfib f b)
    lemma2 = domain-is-Σ f

In the opposite direction, we should check what happens if we start from a term of 𝓟 B, i.e. a function χ : B → Ω ℓ', pull pack the universal proposition along it, and the compute a new term of 𝓟 B out of it. However, we obtain a powerset at a differnt level:

powerset→univ-prop→powerset :  {ℓ' ℓ''} {B : Set ℓ'} (χ : B  Ω ℓ'')  B  Ω (ℓ'  ℓ'')
powerset→univ-prop→powerset χ = embedding→powerset (pullback-univ-prop-is-embedding χ )

so this cannot be directly compared with χ : B → Ω ℓ'', unless of course, there was a way to relate all the proposition classifiers at different levels. This is what the axiom of propositional resizing aims to do.

top ⇑

Propositional resizing4

Propositional resizing was introduced by Voevodsky to ensure certain quotients belong to the same universe as their original types.

Here we just mention a few things. In the HoTT book, §3.5.5 the axiom states that the map Ω ℓ → Ω ℓ’ is a weak equivalence, if ℓ’ is “higher” than ℓ. This presumes universe cumulativity, which we are not assuming, so our formulation will be slightly different.

We follow the treatment at the end of MHE: in words, the axiom of propositional resizing states that propositions can be “resized,” that is, they are equivalent to propositions in a different (usually lower, properly defined) universe.

The idea, similar to that of lift, is that a type at level ℓ has “size” ℓ’ if it is equivalent to a type in that universe:
_has-size_ :  {}  Set   (ℓ' : Level)  Set (  lsuc ℓ')
A has-size ℓ' = Σ[ B  Set ℓ' ] (A  B)
The principle says that for every pair of levels, every proposition in a universe at level ℓ, that is, each term of type Ω ℓ, has size ℓ’:
propositional-resizing : ( ℓ' : Level)  Set (lsuc (  ℓ'))
propositional-resizing  ℓ' = ((P , i) : Ω )  P has-size ℓ'
Like other principles we can formulate a global version of it:
Propositional-Resizing : Setω
Propositional-Resizing =   ℓ'  propositional-resizing  ℓ'
One can always upward resize to a higher universe:
upper-resizing :  {} (A : Set ) (ℓ' : Level)  A has-size (  ℓ')
upper-resizing A ℓ' = (Lift ℓ' A) , ≃id-lift A
    open yoga-lift using (≃id-lift)
and size is upper closed in the following sense:
has-size-is-upper-closed :  { ℓ' ℓ''} (A : Set )  A has-size ℓ'  A has-size (ℓ'  ℓ'')
has-size-is-upper-closed {} {ℓ'} {ℓ''} A (B , e) = C , f
    open yoga-lift using (≃id-lift)
    open ≃-lemmas

    C : Set (ℓ'  ℓ'')
    C = Lift ℓ'' B

    f : A  C
    f = e ≃◾≃ (≃id-lift B)

upper-propositional-resizing :  { ℓ'}  propositional-resizing  (  ℓ')
upper-propositional-resizing {} {ℓ'} (P , i) = upper-resizing P ℓ' 

Resizing is a proposition

We tautologically observe that the underlying type of a resized proposition is indeed a proposition. First, we extract the underlying type:
resize :  { ℓ'}  propositional-resizing  ℓ'  ((P , i) : Ω )  Set ℓ'
resize rez (P , i) = π₁ (rez (P , i))
Then we extract the proof that it indeed is a proposition
resize-is-prop :  { ℓ'} (rez : propositional-resizing  ℓ')
                 ((P , i) : Ω )  isProp (resize rez (P , i))
resize-is-prop {} {ℓ'} rez (P , i) = j
    Q : Set ℓ'
    Q = resize rez (P , i)

    j : isProp Q
    j = weak-equivalences-preserve-props i (π₂ (rez (P , i)))
We will also need the actual underlying maps to and from the resized underlying type:
→resize :  { ℓ'} (rez : propositional-resizing  ℓ') ((P , i) : Ω ) 
          P  resize rez (P , i)
→resize rez (P , i) = π₁ (π₂ (rez (P , i)))

resize→ :  { ℓ'} (rez : propositional-resizing  ℓ') ((P , i) : Ω ) 
          resize rez (P , i)  P
resize→ rez (P , i) = π₁ ( iseq→qinv (→resize rez (P , i)) (π₂ (π₂ (rez (P , i)))) )


To be small means to have size in the smaller universe:
is-small :  {}  Set   Set (  1ℓ)
is-small A = A has-size 0ℓ
The ultimate meaning of propositional resizing is that all propositions in all universes are small, as per the following statements:
all-propositions-are-small :    Set (lsuc )
all-propositions-are-small  = ((P , i) : Ω )  is-small P

all-propositions-are-small-is-PR₀ :  {}  all-propositions-are-small   propositional-resizing  0ℓ
all-propositions-are-small-is-PR₀ = refl

all-propositions-are-small→PR :  { ℓ'}  all-propositions-are-small   propositional-resizing  ℓ'
all-propositions-are-small→PR {} {ℓ'} s (P , i) = has-size-is-upper-closed P γ
    γ : is-small P
    γ = s (P , i)

propositional-resizing→all-propositions-are-small :  {}  propositional-resizing  0ℓ  all-propositions-are-small 
propositional-resizing→all-propositions-are-small {} rez (P , i) = rez (P , i)

Excluded Middle implies Propositional Resizing

The axiom of propositional resizing is implied by assuming the Law of Excluded Middle: recall that assuming LEM means that every proposition is decidable (see MHE):
LEM→all-propositions-are-small :  {}  LEM   all-propositions-are-small 
LEM→all-propositions-are-small {} lem (P , i) = (Q (lem P i)) , e
    Q : P + ¬ P  Set₀
    Q (inl _) = 𝟙
    Q (inr _) = 𝟘

    j : (x : P + ¬ P)  isProp (Q x)
    j (inl x) = 𝟙-is-prop
    j (inr x) = 𝟘-is-prop

    f : (x : P + ¬ P)  P  Q x
    f (inl x) = λ _  *
    f (inr ¬x) = λ x  (¬x x)

    g : (x : P + ¬ P)  Q x  P
    g (inl x) = λ _  x
    g (inr x) = !𝟘

    e : P  Q (lem P i)
    e = prop-logical-eq-is-eq i (j (lem P i)) (f (lem P i)) (g (lem P i))
Therefore LEM implies propositional resizing:
LEM→PR :  { ℓ'}  LEM   propositional-resizing  ℓ'
LEM→PR {} {ℓ'} lem = all-propositions-are-small→PR (LEM→all-propositions-are-small lem)

Propositional impredicativity

According to the HoTT book, §3.5, propositional impredicativity is (vaguely) the statement that the types Ω ℓ can be resized. We can give two versions of the type embodying this principle:
impredicativity :   ℓ'  Set (lsuc (  ℓ'))
impredicativity  ℓ' = Ω  has-size ℓ'

is-impredicative :    Set (lsuc )
is-impredicative  = impredicativity  

Recall that Ω ℓ lives in Set (lsuc ℓ). Hence the second statement means that Ω ℓ has a copy of itself (an equivalent type) in the universe Set ℓ. But notice the statement that Set ℓ is impredicative is still in the higher universe.

PR→impredicativity⁺ :  { ℓ'}(dfe : dfunext  ) (pe : propext )
                              (dfe' : dfunext ℓ' ℓ') (pe' : propext ℓ')
                              (rez : propositional-resizing  ℓ')
                              (rez' : propositional-resizing ℓ' ) 
                              impredicativity  (lsuc ℓ')
PR→impredicativity⁺ {} {ℓ'} dfe pe dfe' pe' rez rez' = (Ω ℓ') , (φ , (qinv→iseq φ (ψ , (ε , η))))
    φ : Ω   Ω ℓ'
    φ (P , i) = (resize rez (P , i)) , (resize-is-prop rez (P , i))

    ψ : Ω ℓ'  Ω 
    ψ (Q , j) = (resize rez' (Q , j)) , (resize-is-prop rez' (Q , j))

    ε : (q : Ω ℓ')  φ (ψ q)  q
    ε q = Ω-ext dfe' pe' (φ (ψ q)) q f g
        Q : Set ℓ'
        j : isProp Q
        Q = π₁ q
        j = π₂ q

        P : Set 
        i : isProp P
        P = resize rez' (Q , j)
        i = resize-is-prop rez' (Q , j)

        f : resize rez (P , i)  Q
        f = resize→ rez' (Q , j) ∘′ resize→ rez (P , i)

        g : Q  resize rez (P , i)
        g = →resize rez (P , i) ∘′ →resize rez' (Q , j)

    η : (p : Ω )  ψ (φ p)  p
    η p = Ω-ext dfe pe (ψ (φ p)) p f g
        P : Set 
        i : isProp P
        P = π₁ p
        i = π₂ p
        Q : Set ℓ'
        j : isProp Q
        Q = resize rez (P , i)
        j = resize-is-prop rez (P , i)

        f : resize rez' (Q , j)  P
        f = resize→ rez (P , i) ∘′ resize→ rez' (Q , j)

        g : P  resize rez' (Q , j)
        g = →resize rez' (Q , j) ∘′ →resize rez (P , i)

        q : Ω ℓ'
        q = (Q , j)
Assuming propositional resizing we also obtain that all universes (except the first one) are impredicative
PR→is-impredicative⁺ :  {}  dfunext (lsuc ) (lsuc )  propext (lsuc ) 
                      dfunext    propext  
                      propositional-resizing (lsuc )   
                      is-impredicative (lsuc )
PR→is-impredicative⁺ {} dfe⁺ pe⁺ dfe pe rez =
                     PR→impredicativity⁺ {lsuc } {} dfe⁺
                                                      ( λ p  upper-resizing (π₁ p) (lsuc ) )
And we can also see that all the propositions classifiers Ω ℓ are equivalent to the bottom one Ω 0ℓ, which lives in Set 1ℓ:
PR→impredicativity₁ :  {}  dfunext    propext  
                      dfunext 0ℓ 0ℓ  propext 0ℓ 
                      propositional-resizing  0ℓ  
                      impredicativity  1ℓ
PR→impredicativity₁ {} dfe pe dfe₀ pe₀ rez =
                    PR→impredicativity⁺ dfe
                                        λ p  upper-resizing (π₁ p) 
Conversely, we have that impredicativity implies propositional resizing:
impredicativity→PR :  { ℓ'}  dfunext    propext 
                               impredicativity  ℓ'
                               propositional-resizing  ℓ'
impredicativity→PR {} {ℓ'} dfe pe (Ω' , e) (P , i) = Q , prop-logical-eq-is-eq i j g f
    𝟙' : Set 
    𝟙' = Lift  𝟙

    k : isProp 𝟙'
    k (lift *) (lift *) = refl

    r : Ω   Ω'
    r = π₁ e

    Ω'-is-set : isSet Ω'
    Ω'-is-set = weak-equivalences-preserve-sets (Ω-is-set dfe pe) e

    Ω'-is-set' : isSet' Ω'
    Ω'-is-set' = isSet→isSet' Ω' Ω'-is-set

    Q : Set ℓ'
    Q = r (𝟙' , k)  r (P , i)

    j : isProp Q
    j = Ω'-is-set' (r (𝟙' , k))  (r (P , i))

    f : Q  P
    f q = p (lift *)
        q' : 𝟙' , k  P , i
        q' = eq-is-lc r (π₂ e) q

        p : 𝟙'  P
        p = Id→Fun (ap π₁ q')

    g : P  Q
    g p = ap r q'
        q' : 𝟙' , k  P , i
        q' = fiber-props-id-base-give-identities (isProp-is-Prop' dfe) 
                                                 (𝟙' , k)
                                                 (P , i)
                                                 (pe k i  { (lift *)  p}) λ x  lift *)

top ⇑

  1. We could obviate this by simply assuming global function extensionality↩︎

  2. This is one of those situations in which one wishes that universes were not named Set ℓ.↩︎

  3. It is possible to prove they are equivalent.↩︎

  4. In this section we follow (with minor variations) MHE↩︎