---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module Base.Impredicativity where
```
# Impredicativity
```agda
open import Base.Prelude
```
A predicative foundation does not allow quantification within a definition over a totality that already contains the object 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. All 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 `ℓ`.
For example, suppose we define a proposition `R` by saying that every `Q : hProp ℓ` implies itself, and also demand that `R` belong to `hProp ℓ`. Then the quantifier over every `Q` also ranges over `R`: the totality being quantified over already includes the proposition being defined. The claim that `Q` implies itself is elementary; the difficulty is the demand that this quantification produce a proposition at the same level. In Cubical Agda the quantification instead lives one universe higher. User code cannot rewrite Agda's universe-level rules, but an explicit assumption can connect the higher proposition to a lower representative with the same truth content.
We express this connection using the type equivalence `A ≃ B` introduced in the foundational vocabulary. It can relate types in different universes while preserving their elements and paths. There are two distinct size requirements: finding a representative for each proposition, and finding one type that represents an entire proposition universe.
## Propositional resizing
Given `P : hProp ℓ₁`, Agda does not let us change the level at which `P` lives. What we can ask for is another proposition `Q : hProp ℓ₂` whose underlying type is connected to that of `P` by a type equivalence.
**Definition** (`hasSize`) We read `hasSize ℓ₂ P` as saying that `P` has size `ℓ₂`, and define it as the dependent pair below. Its first component chooses `Q`, and its second component gives the type equivalence showing that `Q` has exactly the truth content of `P`.
```agda
hasSize : ∀ {ℓ₁} (ℓ₂ : Level) → hProp ℓ₁ → Type (ℓ-max ℓ₁ (ℓ-suc ℓ₂))
hasSize ℓ₂ P = Σ[ Q ∶ hProp ℓ₂ ] (⟨ P ⟩ ≃ ⟨ Q ⟩)
```
Neither level has to be larger than the other. In the applications below `ℓ₁` is usually the model's truth-value level and `ℓ₂` its indexing level, but the definition itself allows any two levels. The name "propositional resizing" refers to replacing a proposition by a type-equivalent representative at the chosen target level, rather than changing the universe annotation of the original proposition.
**Definition** (`Resizing`) We read `Resizing ℓ₁ ℓ₂` as saying that propositions at level `ℓ₁` can be resized to level `ℓ₂`, and define it as the dependent function below. For each `P : hProp ℓ₁`, it returns a witness that `P` has size `ℓ₂`.
```agda
Resizing : ∀ ℓ₁ ℓ₂ → Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂))
Resizing ℓ₁ ℓ₂ = (P : hProp ℓ₁) → hasSize ℓ₂ P
```
## Ω-resizing
**Definition** (`ΩResizing`) We read `ΩResizing ℓ₁ ℓ₂` as saying that the proposition universe `hProp ℓ₁` has size `ℓ₂`, and define it as the dependent pair below. Its first component chooses a type `Ω : Type ℓ₂`; its second gives a type equivalence `hProp ℓ₁ ≃ Ω`. Thus every proposition at `ℓ₁` has a code in `Ω`, and every element of `Ω` decodes to such a proposition.
```agda
ΩResizing : ∀ ℓ₁ ℓ₂ → Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂))
ΩResizing ℓ₁ ℓ₂ = Σ[ Ω ∶ Type ℓ₂ ] (hProp ℓ₁ ≃ Ω)
```
propositional resizing
Propositional resizing replaces each proposition by a type-equivalent representative at a chosen universe level.
$$r : \operatorname{Resizing}\,\ell_1\,\ell_2$$
$$P_i : \operatorname{hProp}\,\ell_1$$
$$Q_i : \operatorname{hProp}\,\ell_2$$
$$\langle P_1\rangle$$
$$\overset{e_1}{\simeq}$$
$$\langle Q_1\rangle$$
$$\langle P_2\rangle$$
$$\overset{e_2}{\simeq}$$
$$\langle Q_2\rangle$$
$$\vdots$$
$$\vdots$$
$$r(P_i) = (Q_i,e_i)$$
Ω-resizing
Ω-resizing presents an entire proposition universe by a type in a chosen universe level.
$$c_i = \operatorname{equivFun}\,e\,P_i : \Omega$$
Resizing each proposition and resizing the whole proposition universe ask for different data
Next we prove that Ω-resizing implies propositional resizing. Suppose we are given `Ω : Type ℓ₂` and an equivalence `e : hProp ℓ₁ ≃ Ω`. This equivalence gives each proposition a code in `Ω`; we still need to turn that code into a proposition at level `ℓ₂` and prove it equivalent to the original.
In an ordinary mathematical proof, we might fix `Ω` and `e` for the argument and carry out several constructions under these shared assumptions. Agda expresses the same arrangement with the parameterized submodule `CodedTruth`: its declaration lists the common data, which its definitions can use without repeating the parameters. When the main theorem receives a particular `(Ω , e)`, it uses those constructions. `private` only makes the module an internal proof aid; it adds no mathematical assumption.
```agda
private module CodedTruth {ℓ₁ ℓ₂} (Ω : Type ℓ₂) (e : hProp ℓ₁ ≃ Ω) where
```
Name the forward map of `e` by `c`. Then `c P` is the code of `P` in `Ω`.
```agda
c : hProp ℓ₁ → Ω
c = equivFun e
```
**Construction** (`codedTruth`) The code `c P` is a point of `Ω`. To obtain a proposition, ask whether it equals the code of truth: `c ⊤ ≡ c P`. This path type lies at level `ℓ₂`. It is a proposition because `e` transfers the h-set structure of `hProp ℓ₁` to `Ω`. We take it as the representative of `P`; the isomorphism below verifies that it has the same truth content.
```agda
codedTruth : hProp ℓ₁ → hProp ℓ₂
codedTruth P = (c ⊤ ≡ c P) , isOfHLevelRespectEquiv 2 e isSetHProp _ _
```
The band in `Ω` depicts paths with endpoints `c(⊤)` and `c(P)`. Click it to unfold the path family into the second type space, with whole paths represented as points. The illustrated `q` and `r` presuppose that `P` has a proof; the equivalence with `⟨ P ⟩` holds without this assumption.
A point in `⟨ codedTruth P ⟩` is a whole path in `Ω`: `⟨ codedTruth P ⟩ = (c(⊤) ≡ c(P))`. The two proof types are equivalent, at levels `ℓ₁` and `ℓ₂` respectively
**Lemma** (`codedTruthIso`) The underlying type of `P` is isomorphic to the underlying type of `codedTruth P`. Thus the representative constructed above really has the same truth content as `P`.
```agda
codedTruthIso : (P : hProp ℓ₁) → Iso ⟨ P ⟩ ⟨ codedTruth P ⟩
```
**Proof** We construct the two maps `to` and `from`, then assemble them with `iso`. The source `⟨ P ⟩` and target `⟨ codedTruth P ⟩` are both propositions, so their propositionhood proves the two round-trip laws once the maps have been given. Where a map must return an inhabitant of truth, we write its unique inhabitant `tt*` explicitly.
```agda
codedTruthIso P = iso to from (λ q → ⟨ codedTruth P ⟩isProp _ q) (λ p → ⟨ P ⟩isProp _ p)
where
```
It remains to construct the two maps.
- For `to`, a proof `p : ⟨ P ⟩` makes `⊤` and `P` logically equivalent. Propositional extensionality gives `⊤ ≡ P`; applying `cong c` yields `c ⊤ ≡ c P`, a proof of `codedTruth P`.
```agda
to : ⟨ P ⟩ → ⟨ codedTruth P ⟩
to p = cong c (⇔toPath (λ _ → p) (λ _ → tt*))
```
- For `from`, start with `q : c ⊤ ≡ c P`. The equivalence `congEquiv e` identifies paths between propositions with paths between their codes. Its inverse `invEq (congEquiv e)` recovers `⊤ ≡ P`; transporting `tt*` along this path with `subst ⟨_⟩` gives a proof of `P`.
```agda
from : ⟨ codedTruth P ⟩ → ⟨ P ⟩
from q = subst ⟨_⟩ (invEq (congEquiv e) q) tt*
```
**Theorem** (`ΩResizing→Resizing`) Ω-resizing implies propositional resizing.
**Proof** Given `(Ω , e)`, the preceding module supplies `codedTruth P` at level `ℓ₂` for each `P`. Convert `codedTruthIso P` to an equivalence with `isoToEquiv`; the pair is precisely `hasSize ℓ₂ P`.
```agda
ΩResizing→Resizing : ∀ {ℓ₁ ℓ₂} → ΩResizing ℓ₁ ℓ₂ → Resizing ℓ₁ ℓ₂
ΩResizing→Resizing (Ω , e) P = codedTruth P , isoToEquiv (codedTruthIso P)
where open CodedTruth Ω e
```
## 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; propositional resizing supplies such representatives pointwise, while Ω-resizing presents a proposition universe all at once. No inhabitant has been constructed here. The classical chapter derives both principles from excluded middle.