可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

直谓主义数学基础不允许在一个定义中量化某个已经包含待定义对象的总体。Cubical Agda 建立在这样的基础之上，而本书所要形式化的集合论包含非直谓的构造。为了在直谓式的宿主中准确说明这些构造需要什么，本章专门提出一组接口：它们不改变宿主本身，而是把开展非直谓数学所需的额外条件明确列为假设。

直谓主义数学基础可以容纳这样的非直谓假设，正如直觉主义逻辑可以明确加入经典逻辑原理；反过来却不成立，因为一旦基础本身预先采用了更强的原则，就无法再分辨后续结果究竟依赖哪些额外假设。因此，本书保留 Cubical Agda 的直谓式基础，并在需要非直谓性时，通过本章的接口逐项说明所用的条件。

困难来自宇宙层级。底层类型位于 Type ℓ 的所有命题组成 hProp ℓ，而这个命题宇宙整体属于 Type (ℓ-suc ℓ)。因此，对 hProp ℓ 中所有命题量化所得的命题，不一定仍能放在层级 ℓ。

例如，试图把命题 R 定义为「每个 Q : hProp ℓ 都蕴含自身」，同时要求 R 也属于 hProp ℓ。这样，定义中的「每个 Q」也遍及 R：量化的总体已经包含正在定义的命题。「Q 蕴含自身」虽然显然成立，难点仍是要求这次量化所得的命题留在同一层级。在 Cubical Agda 中，它位于高一层的宇宙。Agda 的用户代码不能改写其宇宙层级规则，但可以通过显式假设，把这个高层命题与真值内容相同的低层代表联系起来。

我们用基础词汇中介绍的类型等价 A ≃ B 表达这种联系。它允许两个类型位于不同宇宙，同时保留其中的元素与路径。接下来要区分两种尺寸要求：逐个为命题寻找代表，以及用一个类型呈现整个命题宇宙。

命题换级

给定 P : hProp ℓ₁，Agda 不允许我们直接改变 P 所在的层级；能够提出的要求，是在目标层级找到另一个命题 Q : hProp ℓ₂，使二者的底层类型类型等价。

定义 (hasSize) 我们把「P 具有尺寸 ℓ₂」记作 hasSize ℓ₂ P，并将其定义为以下依值对：第一分量选出 Q，第二分量给出类型等价，表明 Q 与 P 具有完全相同的真值内容。

hasSize : ∀ {ℓ₁} (ℓ₂ : Level) → hProp ℓ₁ → Type (ℓ-max ℓ₁ (ℓ-suc ℓ₂))
hasSize ℓ₂ P = Σ[ Q ∶ hProp ℓ₂ ] (⟨ P ⟩ ≃ ⟨ Q ⟩)

这里不要求两个层级有大小顺序。在后面的应用中，ℓ₁ 通常是模型真值所在的层级，ℓ₂ 是索引所在的层级；但定义本身允许任意两个层级。「命题换级」是指用目标层级中的类型等价代表替换原命题，而不是修改原命题的宇宙标注。

定义 (Resizing) 我们把「ℓ₁ 层的命题可换级到 ℓ₂ 层」记作 Resizing ℓ₁ ℓ₂，并将其定义为以下依值函数：对每个 P : hProp ℓ₁，它返回「P 具有尺寸 ℓ₂」的见证。

Resizing : ∀ ℓ₁ ℓ₂ → Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂))
Resizing ℓ₁ ℓ₂ = (P : hProp ℓ₁) → hasSize ℓ₂ P

命题宇宙换级

定义 (ΩResizing) 我们把「命题宇宙 hProp ℓ₁ 具有尺寸 ℓ₂」记作 ΩResizing ℓ₁ ℓ₂，并将其定义为以下依值对：第一分量给出类型 Ω : Type ℓ₂，第二分量给出类型等价 hProp ℓ₁ ≃ Ω。因此，ℓ₁ 层的每个命题都在 Ω 中有编码，而 Ω 的每个元素也都解码为该层的命题。

ΩResizing : ∀ ℓ₁ ℓ₂ → Type (ℓ-max (ℓ-suc ℓ₁) (ℓ-suc ℓ₂))
ΩResizing ℓ₁ ℓ₂ = Σ[ Ω ∶ Type ℓ₂ ] (hProp ℓ₁ ≃ Ω)

命题换级

命题换级为每个命题在指定宇宙层级选取一个类型等价的代表。

$$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)$$

命题宇宙换级

命题宇宙换级用指定宇宙层级中的一个类型呈现整个命题宇宙。

$$(\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$$

逐个命题换级与整个命题宇宙换级，要求的是不同的数据

接下来证明：命题宇宙换级蕴含命题换级。假设给定 Ω : Type ℓ₂ 和等价 e : hProp ℓ₁ ≃ Ω。等价使每个命题都有 Ω 中的编码；我们还需要从这个编码构造 ℓ₂ 层的命题，并证明它与原命题等价。

通常的数学证明会先说「以下固定 Ω 和 e」，再在这两个共同前提下完成一系列构造。Agda 用带参数的子模块 CodedTruth 表达同样的安排：模块声明列出共同前提，里面的定义都可以直接使用它们，不必反复写出参数。证明最后收到具体的 (Ω , e) 时，再取用这一组构造。private 只表示这个模块是本章内部的辅助工具，并未增加数学假设。

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

把 e 的正向映射命名为 c。于是 c P 是 P 在 Ω 中的编码。

c : hProp ℓ₁ → Ω
c = equivFun e

构造 (codedTruth) 编码 c P 是 Ω 中的一个点。要得到命题，就问它是否等于真命题的编码：c ⊤ ≡ c P。这个路径类型位于 ℓ₂ 层；e 把 hProp ℓ₁ 的 h-集合结构搬运到 Ω，保证它是命题。我们取它作为 P 的代表，下面的同构将证明二者具有相同的真值内容。

codedTruth : hProp ℓ₁ → hProp ℓ₂
codedTruth P = (c ⊤ ≡ c P) , isOfHLevelRespectEquiv 2 e isSetHProp _ _

Ω 中的带状区域示意端点为 c(⊤)、c(P) 的路径族。点击它，路径族展开成第二个类型空间，整条路径改画成其中的点。图中的 q、r 以 P 有证明为前提；与 ⟨ P ⟩ 的类型等价本身不需要这个假设。

$$\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)$

⟨ codedTruth P ⟩ 中的一个点，就是 Ω 中的一整条路径：⟨ codedTruth P ⟩ = (c(⊤) ≡ c(P))。两个证明类型分别位于 ℓ₁ 和 ℓ₂ 层，彼此类型等价

引理 (codedTruthIso) P 的底层类型与 codedTruth P 的底层类型同构。因此，上面构造的代表确实与 P 具有相同的真值内容。

codedTruthIso : (P : hProp ℓ₁) → Iso ⟨ P ⟩ ⟨ codedTruth P ⟩

证明 我们构造两个方向的映射 to 和 from，再用 iso 把它们组装起来。源 ⟨ P ⟩ 和目标 ⟨ codedTruth P ⟩ 都是命题，因此给出两个映射之后，两端的命题性便可直接证明两条往返律。映射需要返回真命题的元素时，我们显式写出其唯一元素 tt*。

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

现在构造两个方向的映射。

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

  from : ⟨ codedTruth P ⟩ → ⟨ P ⟩
  from q = subst ⟨_⟩ (invEq (congEquiv e) q) tt*

定理 (ΩResizing→Resizing) 命题宇宙换级蕴含命题换级。

证明 给定 (Ω , e)，前面的模块为每个 P 提供位于 ℓ₂ 层的 codedTruth P。再用 isoToEquiv 将 codedTruthIso P 转成等价，所得依值对正是 hasSize ℓ₂ P。

ΩResizing→Resizing : ∀ {ℓ₁ ℓ₂} → ΩResizing ℓ₁ ℓ₂ → Resizing ℓ₁ ℓ₂
ΩResizing→Resizing (Ω , e) P = codedTruth P , isoToEquiv (codedTruthIso P)
  where open CodedTruth Ω e

小结

这些定义分离出了直谓式宇宙层级不会自动提供的尺寸信息。借助类型等价，高层命题获得具有相同真值内容的低层代表；命题换级逐点给出这类代表，命题宇宙换级则一次呈现整个命题宇宙。本章尚未构造这些原理的见证。「经典逻辑的边界」将从排中律导出二者。