非直谓性

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

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

这里的困难来自宇宙层级。底层类型位于 Type ℓ 的命题组成 hProp ℓ，而这个命题宇宙整体属于 Type (ℓ-suc ℓ)。因此，对 hProp ℓ 中所有命题量化所得的命题，不一定仍能放在层级 ℓ。本章要解决的问题，就是如何让高层命题的真值内容仍能由低层对象表示。

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

module Base.Impredicativity where

open import Base.Prelude

跨越宇宙层级的比较

所谓「表示」，并不是把高层命题原封不动地放进低层宇宙，而是为它寻找一个低层命题，使二者表达相同的内容。要把这句话写成精确的数学条件，我们首先需要确定应当用什么关系比较它们。

路径暂时不能直接承担这项工作，因为路径的两端必须属于同一个环境类型，而高层命题与低层命题位于不同的宇宙。逻辑等价可以说明两个命题互相蕴含，却只适用于命题；后面使用的小分类器本身并不是命题。因此，我们需要一种对任意类型都适用的比较方式，这就是类型等价。

对类型 A 与 B，类型等价 A ≃ B 首先包含一个映射 f : A → B。为了判断这个映射能否完整地保存信息，我们逐个考察 b : B 可以怎样从 A 映到。

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

f 在 b 上的纤维，是下面这个依值对类型：

纤维的一个元素由两部分组成：第一分量是一个候选原像 a : A，第二分量是一条路径 f a ≡ b，证明这个 a 的确映到 b。纤维为空，表示 b 没有原像；纤维中若有彼此不能通过路径等同的元素，则表示从 b 返回 A 时存在实质不同的选择。

当每个 b : B 上的纤维都可缩时，每条纤维都有一个中心，纤维中的其他元素都通过路径与它等同。因此，每个 b 都可以从 A 中恢复，而且恢复结果在路径意义下没有歧义。满足这个条件的映射称为等价；逆向映射与两条往返路径都可以由这些纤维的中心导出。

这里的类型等价需要与同构区分。同构显式给出正向映射、选定的逆向映射和两条逆律。同构可以转换为等价，等价也可以表示为同构；区别在于怎样组织同一份数学信息。构造具体例子时，显式列出映射往往使同构更为方便；立方库则以等价作为搬运类型结构的统一接口，因此本章用 _≃_ 表述两项小性原理。

_≃_ 也不只是逻辑等价。两个命题逻辑等价，指的是它们之间具有两个方向的蕴含。若 P 与 Q 的底层类型都满足 isProp，这两个方向便足以确定一个类型等价：命题性使所有证明都不可区分，两个复合因而自动满足逆律。对一般类型，两个方向各有一个映射并不能保证它们互逆，所以逻辑等价并不足够。下面的两种用法体现了这个区别：在 isSmall 中，两端都是命题，逻辑等价可以提升为类型等价；在 HPropSmallness 中，小分类器和 hProp ℓ 本身都不是命题，完整的类型等价不可省略。

这样便可以看清三个概念在本书论证中的分工：证明类型等价时常先构造同构，保存和搬运结构时统一使用类型等价，而当两个对象已经位于同一个环境类型中时，最终的比较往往表述为路径。

何谓小

设 P : hProp (ℓ-suc ℓ)。若存在 Q : hProp ℓ，且它的底层类型与 P 的底层类型等价，那么 P 的真值内容就在层级 ℓ 有了表示。这一对数据就是 P 是小的含义：第一分量选出 Q，第二分量使两边的证书可以双向转换。

完整见证 isSmall P 仍属于 Type (ℓ-suc ℓ)。小性并不把 P 本身降入低层宇宙，而是为它给出一个低层代表；不同见证也可能选出不同的代表。

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

两个接口

小性只涉及一个命题。命题降级把它一致地用于任意命题：对高于 ℓ 一个宇宙的每个命题，它都返回该命题是小的见证。因此，Resizing ℓ 是一个依值函数类型，输入为 P : hProp (ℓ-suc ℓ)，输出为 isSmall P。

由于输入遍历 hProp (ℓ-suc ℓ)，命题降级本身位于 Type (ℓ-suc (ℓ-suc ℓ))。它的元素为每个 P 给出一个代表，但不要求代表唯一，也不要求这些选择之间另有关系。

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

第二条原理针对整个命题宇宙。HPropSmallness ℓ 的见证选取一个类型 Ω' : Type ℓ，并给出等价 Ω' ≃ hProp ℓ。于是，一个小分类器便一次呈现了层级 ℓ 的所有命题。

分类器本身不必是命题，它的元素通过上述等价分类命题。这条陈述位于 Type (ℓ-suc ℓ)，比命题降级低一个宇宙。因此两项原理具有不同的形状，两项定义也都没有声称其中一项蕴含另一项。

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

合并两项原理

累积层级在不同公理中使用这两项原理：命题降级为定义分离子集的每个命题给出低一宇宙中的等价代表，小分类器则为幂集提供所需的尺寸控制。Impredicativity ℓ 因而同时记录两项假设；它的两个字段分别包含 Resizing ℓ 和 HPropSmallness ℓ，二者之间没有相容性条件。

这个 record 位于 Type (ℓ-suc (ℓ-suc ℓ))，即两个分量所在层级中较高的一层。投影可以分别取回任一项原理。record 不增加数学强度，只是把二者的合取表示为数据。

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

小结

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