--- title: "Impredicativity" module: Base.Impredicativity lang: en site: "Bedrock" description: "Impredicativity" stage: "Foundations" reading_order: 3 canonical: https://bedrock.institute/en/Base.Impredicativity.html html: Base.Impredicativity.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Impredicativity.lagda.md prerequisites: [Base.Prelude] routes: [common-foundations] translations: [https://bedrock.institute/zh/Base.Impredicativity.md, https://bedrock.institute/ja/Base.Impredicativity.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Impredicativity A predicative foundation does not allow a definition to range over a totality that already contains what is being defined. Cubical Agda has such a foundation, whereas the set theory formalized in this book contains impredicative constructions. This chapter therefore states the extra conditions needed for those constructions as explicit assumptions, without changing the foundation of the host. A predicative foundation can accommodate impredicative assumptions just as intuitionistic logic can explicitly assume classical principles. The converse does not hold: once the stronger principles are built into the foundation, later results no longer reveal which of them they actually require. We therefore retain Cubical Agda's predicative foundation and name every impredicative condition at the point where it is used. The issue appears in the universe levels. The propositions whose underlying types lie in `Type ℓ` form `hProp ℓ`, but this proposition universe as a whole belongs to `Type (ℓ-suc ℓ)`. A proposition obtained by quantifying over all of `hProp ℓ` need not fit at level `ℓ`. This chapter asks how the truth content of such a higher proposition can nevertheless be represented by an object at the lower level. ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Impredicativity where open import Base.Prelude ``` ## Comparing across universe levels To represent a higher proposition is not to place it unchanged in a lower universe. It is to find a lower proposition with the same content. Before making that statement precise, we must decide what relation should compare the two. A path cannot yet do this job directly, because its endpoints must belong to a common ambient type, while the higher and lower propositions inhabit different universes. Logical equivalence can express mutual implication between propositions, but the small classifier used later is not itself a proposition. We therefore need a comparison that applies to arbitrary types: **type equivalence**. For types `A` and `B`, a type equivalence `A ≃ B` begins with a map `f : A → B`. To determine whether this map preserves all information, consider in turn how each `b : B` can arise from `A`. ```agda open import Cubical.Foundations.Equiv using ( _≃_ ) ``` The **fibre** of `f` over `b` is the following dependent pair type:
Σ (a : A) (f a ≡ b)
An element of the fibre has two components. The first is a candidate preimage `a : A`; the second is a path `f a ≡ b` witnessing that this candidate really maps to `b`. An empty fibre means that `b` has no preimage. Elements of a fibre that cannot be identified by a path represent substantively different ways to return from `b` to `A`. When the fibre over every `b : B` is contractible, each fibre has a centre and all its other elements are path-equal to that centre. Every `b` can therefore be recovered from `A`, and the recovery has no ambiguity up to paths. A map with this property is an equivalence. The inverse map and its two round-trip paths can be derived from the centres of the fibres. This notion should be distinguished from an isomorphism. An isomorphism presents a forward map, a chosen inverse map and the two inverse laws explicitly. It can be converted into an equivalence, and an equivalence can in turn be presented as an isomorphism; the difference is how the same mathematical information is organised. Explicit maps often make an isomorphism convenient when constructing an example. The cubical library uses equivalence as the common interface for transporting type structure, so this chapter records its size principles with `_≃_`. Nor does `_≃_` merely mean logical equivalence. Logical equivalence between propositions supplies implications in both directions. If the underlying types of `P` and `Q` both satisfy `isProp`, those implications do determine an equivalence: propositionhood makes all proofs indistinguishable, so the two composites satisfy the inverse laws automatically. For general types, maps in both directions need not be inverse and are therefore insufficient. This distinction separates the two uses below. In `isSmall`, both sides are propositions, so a logical equivalence can be promoted to a type equivalence. In `HPropSmallness`, the small classifier and `hProp ℓ` are not themselves propositions, so the full type equivalence is essential. The three notions thus serve different parts of an argument in this book. We often construct an isomorphism to prove an equivalence, use equivalences to preserve and transport structure, and state the final comparison as a path once both objects lie in the same ambient type. ## Being small Let `P : hProp (ℓ-suc ℓ)`. Its truth content has a representation at level `ℓ` when there is a `Q : hProp ℓ` whose underlying type is equivalent to that of `P`. This pair of data is what it means for `P` to **be small**: the first component chooses `Q`, and the second converts certificates in both directions. The witness `isSmall P` still belongs to `Type (ℓ-suc ℓ)`. Smallness does not move `P` itself into the lower universe; it supplies a lower representative, and different witnesses may choose different representatives. ```agda isSmall : ∀ {ℓ} → hProp (ℓ-suc ℓ) → Type (ℓ-suc ℓ) isSmall {ℓ} P = Σ[ Q ∈ hProp ℓ ] (⟨ P ⟩ ≃ ⟨ Q ⟩) ``` ## The two interfaces Smallness concerns one proposition. **Propositional resizing** makes it available uniformly: for every proposition one universe above `ℓ`, it returns a witness that this proposition is small. Thus `Resizing ℓ` is a dependent function type whose input is `P : hProp (ℓ-suc ℓ)` and whose output is `isSmall P`. Because the input ranges over `hProp (ℓ-suc ℓ)`, resizing itself lies in `Type (ℓ-suc (ℓ-suc ℓ))`. An inhabitant supplies one representative for each `P`, without requiring uniqueness or any further relation among the choices. ```agda Resizing : ∀ ℓ → Type (ℓ-suc (ℓ-suc ℓ)) Resizing ℓ = (P : hProp (ℓ-suc ℓ)) → isSmall P ``` The second principle concerns the whole proposition universe. A witness of `HPropSmallness ℓ` chooses one type `Ω' : Type ℓ` and an equivalence `Ω' ≃ hProp ℓ`. Thus one small classifier presents all level-`ℓ` propositions at once. The classifier need not itself be a proposition. Its elements classify propositions through the equivalence. This statement lies in `Type (ℓ-suc ℓ)`, one universe below resizing. The two principles therefore have different shapes, and neither definition claims that one implies the other. ```agda HPropSmallness : ∀ ℓ → Type (ℓ-suc ℓ) HPropSmallness ℓ = Σ[ Ω' ∈ Type ℓ ] (Ω' ≃ hProp ℓ) ``` ## Combining the two principles The cumulative hierarchy uses the principles for different axioms: resizing supplies each proposition defining a separated subset with an equivalent representative in the lower universe, while the classifier supplies the size control needed for power set. `Impredicativity ℓ` therefore records both assumptions together. Its two fields contain a `Resizing ℓ` and an `HPropSmallness ℓ`, with no compatibility condition. The record lies in `Type (ℓ-suc (ℓ-suc ℓ))`, the larger of the levels occupied by its components. Projection recovers either principle independently. The record adds no mathematical strength; it expresses their conjunction as data. ```agda record Impredicativity (ℓ : Level) : Type (ℓ-suc (ℓ-suc ℓ)) where field resizing : Resizing ℓ hPropSmallness : HPropSmallness ℓ ``` ## Recap These definitions isolate the size information that predicative universe levels do not provide automatically. Equivalence gives a higher proposition a lower representative with the same truth content; resizing supplies such representatives pointwise, while small classification presents a proposition universe all at once. No inhabitant has been constructed here. The classical chapter derives both principles from excluded middle, after which separation and power set can use them for their distinct purposes.