Read this chapter directly, or use the interactive contents and dependency graph to choose another route.

Interactive contents · Dependency graph

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.

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 ℓ₂.

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.

Ω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.

$$(\Omega,e) : \Omega\operatorname{Resizing}\,\ell_1\,\ell_2$$
$$\operatorname{hProp}\,\ell_1$$
$$P_1$$
$$P_2$$
$$\cdots$$
$$\overset{e}{\simeq}$$
$$\Omega : \operatorname{Type}_{\ell_2}$$
$$c_1$$
$$c_2$$
$$\cdots$$
$$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.

private module CodedTruth {ℓ₁ ℓ₂} (Ω : Type ℓ₂) (e : hProp ℓ₁ ≃ Ω) where

Name the forward map of e by c. Then c P is the code of P in Ω.

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.

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.

$$\langle P\rangle$$
$$: \operatorname{Type}_{\ell_1}$$
$p$
$\simeq$
$$\langle\operatorname{codedTruth}\,P\rangle$$
$$: \operatorname{Type}_{\ell_2}$$
$q$ $r$
$$\Omega$$
$$: \operatorname{Type}_{\ell_2}$$
$q$ $\langle\operatorname{codedTruth}\,P\rangle$ $r$ $c(\top)$ $c(P)$

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.

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.

codedTruthIso P = iso to from (λ q → ⟨ codedTruth P ⟩isProp _ q) (λ p → ⟨ P ⟩isProp _ p)
  where

It remains to construct the two maps.

  to : ⟨ P ⟩ → ⟨ codedTruth P ⟩
  to p = cong c (⇔toPath (λ _ → p) (λ _ → tt*))

  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.

Ω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.