Impredicativity

The host's universes form a ladder, and the ladder poses one recurring question: does a thing living one floor up have a stand-in below? For propositions the question is the hallmark of impredicativity, the world of truth values refusing to grow with the universe. This chapter mints the vocabulary: what it is for one proposition to be small, the two sweeping interfaces that assert smallness wholesale, and their packing. Nothing is assumed and nothing is proven here; these are interfaces. The next chapter redeems them all from excluded middle, and Part 3 prices concrete model fields in exactly this currency.

{-# OPTIONS --cubical --safe --guardedness #-}

module Base.Impredicativity where

open import Base.Prelude
open import Cubical.Foundations.Equiv using ( _≃_ )

Being small

A proposition one universe up is small when it is equivalent to some proposition one universe down. The definition carries the witness: to hold an inhabitant of isSmall P is to hold the small stand-in together with the equivalence. The smallness chapter of Part 3 will make a whole gymnastics of passing such witnesses around, earning instances one atom at a time without any axiom.

isSmall : ∀ {ℓ} → hProp (ℓ-suc ℓ) → Type (ℓ-suc ℓ)
isSmall {ℓ} P = Σ[ Q ∈ hProp ℓ ] (⟨ P ⟩ ≃ ⟨ Q ⟩)

The two interfaces

Propositional resizing is the sweeping claim: every proposition one universe up is small. This is the precise reason classical set theory never worries about which universe a proposition inhabits. Like LEM, it is stated one level at a time.

Resizing : ∀ ℓ → Type (ℓ-suc (ℓ-suc ℓ))
Resizing ℓ = (P : hProp (ℓ-suc ℓ)) → isSmall P

The second interface speaks not of each proposition but of their totality: the type of truth values, which lives one universe up, is equivalent to a small type. HPropSmallness ℓ asks for a small type equivalent to

hProp ℓ, a small classifier of propositions.

HPropSmallness : ∀ ℓ → Type (ℓ-suc ℓ)
HPropSmallness ℓ = Σ[ Ω' ∈ Type ℓ ] (Ω' ≃ hProp ℓ)

The packing

The two instruments share one character, each saying in its own register that propositions refuse to grow with the universe, and they share their consumers, so they are packed into one interface, one level at a time. The packing is by co-consumption, not by implication: neither instrument derives the other (they descend from two of Voevodsky's separate resizing axioms). The interface says nothing about any particular structure; it is pure universe-level policy.

record Impredicativity (ℓ : Level) : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    resizing       : Resizing ℓ
    hPropSmallness : HPropSmallness ℓ

Recap

Smallness of a proposition is an equivalence with a lower stand-in (isSmall); Resizing asserts it of every proposition,

HPropSmallness of their totality, and Impredicativity packs the two. All of it is vocabulary, none of it is assumed. Next: the one classical principle this book ever appeals to, and the redemption of this whole chapter from it.