---
title: "非直谓性"
module: Base.Impredicativity
lang: zh
site: "Bedrock"
description: "非直谓性"
stage: "基础"
reading_order: 3
canonical: https://bedrock.institute/zh/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/en/Base.Impredicativity.md, https://bedrock.institute/ja/Base.Impredicativity.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 非直谓性

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

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

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

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

module Base.Impredicativity where

open import Base.Prelude
```

## 跨越宇宙层级的比较

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

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

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

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

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

<div class="single-line-code"><code>Σ (a : A) (f a ≡ b)</code></div>

纤维的一个元素由两部分组成：第一分量是一个候选原像 `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` 本身降入低层宇宙，而是为它给出一个低层代表；不同见证也可能选出不同的代表。

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

## 两个接口

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

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

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

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

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

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

## 合并两项原理

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

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

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

## 小结

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