### Contents

{-# 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 γ
where
γ : 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
where
dfe : dfunext ℓ ℓ'
dfe = hfunext→dfunext hfe

i : isSet' (Π A P)
i f g = j
where
open ≃-lemmas

k : isProp (f ~ g)
k p q = dfe p q γ
where
γ : (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.

### 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 γ
where
γ : f ~ g
γ a = dfe (f a) (g a) γ₁
where
γ₁ : 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 γ
where
γ : f ~ g
γ (a₁ , a₂) = dfe (f (a₁ , a₂)) (g (a₁ , a₂)) γ₁
where
γ₁ : 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)))



### 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₂ γ
where
γ : i₁ ~ i₂
γ y = isProp-is-Prop dfe' (i₁ y) (i₂ y)


### Subtypes

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
where
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 =  γ
where
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 ≃⁻¹)


### 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
where
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
where
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
where
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
where
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
where
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
where
φ : (x : A) → isProp (a ≡ x)
φ x = i
where
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)
where
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
where
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
where

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

γ : (P Q : Ω ℓ) → isProp (leq P Q)
γ P Q = Σ-type-isprop ipq (λ _ → iqp)
where
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
where
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



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

p̂ : ∀ {ℓ} → Ω̂ ℓ → Ω ℓ
p̂ = π₁ {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 p̂ 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) →
p̂ ∘′ (embedding→univ-prop f) ≡ (embedding→powerset f) ∘′ (π₁ f)
diagram-univ-prop-commutes dfe f = dfe ((p̂ ∘′ χ̂)) ((χ ∘′ (π₁ f))) γ
where
χ = embedding→powerset f
χ̂ = embedding→univ-prop f

γ : (p̂ ∘′ χ̂) ~ (χ ∘′ (π₁ 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 ≡ p̂ 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
where
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) ≃⁻¹
where
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 ≃⁻¹)
where
open ≃-lemmas
Â : Set (ℓ ⊔ ℓ')
Â = pullback-univ-prop' {ℓ'} (embedding→powerset (f , i))

lemma1 : Â ≃ Σ[ 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.

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


#### Smallness

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 γ
where
γ : 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
where
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 φ (ψ , (ε , η))))
where
φ : Ω ℓ → Ω ℓ'
φ (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
where
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
where
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⁺
pe⁺
dfe
pe
rez
( λ 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
pe
dfe₀
pe₀
rez
λ 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
where
𝟙' : 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 *)
where
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'
where
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 *)



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↩︎