Propositions, Sets and Logic—Ⅱ
Contents
- Cartesian products of propositions and sets
- To be a proposition or a set is a proposition
- Type embeddings
- Subtypes
- The types of Propositions and Sets
- Propositional extensionality
- The powerset
- Propositional resizing
{-# 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 thatf : 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 → Ω ℓ'
Ω ℓ' 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) = PNote 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-embeddingThe 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 → Ω ℓ'.
χ : 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 , reflThe 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 eFor 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  : 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.
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 oflift, 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 *)