Prelude

本书的每一章都是文学化 Agda：解说的文稿与它所解说的经机器检查的代码同住一个文件，解说先行，代码紧随其后。这开篇一章负责摆桌子：先立下一条决定本书读法的纪律 (任何名字都可溯源)；再从 cubical 标准库转出全书立足的一小套宿主语言词汇。本章不证明任何东西；现在可以速览，之后遇到陌生符号再回来查。

名字可溯源

有一条由机器执法的纪律须在开篇言明，因为它改变本书的读法：每条 import 都精确列出所取的名字。一章的 import 块因此兼作它的先修清单，「这个名字从哪来」在页面上总有答案。有意设置的例外是全书指定的两个枢纽，即本章与下一章：它们被整体打开，凡未见于任何 import 清单的名字都来自枢纽。

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

module Base.Prelude where

宿主词汇

以下逐条转出，一段说明领一条 import：它带来什么，本书要它做什么。

宿主把类型组织成一座塔斯基式宇宙塔，层级显式。Level 是层级本身的类型，配有层级算术 ℓ-zero、ℓ-suc、ℓ-max；Type ℓ 是第 ℓ 层宇宙，它自身又是高一层的类型，住在 Type (ℓ-suc ℓ) 里。本书凡检视某个总体 (「所有集合」「所有命题」)，都由这套层级记账精确说明检视的总体有多大。

open import Cubical.Foundations.Prelude public
  using ( Type; Level; ℓ-zero; ℓ-suc; ℓ-max )

_≡_ 是路径类型，即宿主的相等，随行的是它的日常工具：refl (自反)、sym (对称)、_∙_ (路径复合)、cong 与 cong₂ (任何函数都尊重相等)、transport 与 subst (沿路径搬运居民)，以及 funExt (逐点相等的函数相等)。

open import Cubical.Foundations.Prelude public
  using ( _≡_; refl; sym; _∙_; cong; cong₂; transport; subst; funExt )

h-层级谓词按「相等结构的多少」为类型分级：isProp (任意两个居民相等)、isSet (相等本身是命题)、isContr (恰有一个居民，在路径意义下)，以及把它们串起来的 isProp→isSet。isContr 就是本书表述唯一存在的方式，这一承重决策在纲领中有完整论述。

open import Cubical.Foundations.Prelude public
  using ( isProp; isSet; isContr; isProp→isSet )

Lift 把一个类型复制到更高的宇宙层级：当某个东西住得低了一层，这就是标准补丁。lift 与 lower 在原类型与其副本之间搬运元素，两者互逆；不对称发生在类型层面，那里是单行道：类型总能向上复制，却一般没有办法把一个类型搬下来。(例外是命题：经典边界一章将看到，排中律恰好买得到这个向下方向。)

open import Cubical.Foundations.Prelude public
  using ( Lift; lift; lower )

hProp 把一个类型与其命题性证明打包：它就是本书经典侧的真值类型。随行的两条事实值得说清。isSetHProp 说的是 hProp 自身是集合：由 univalence，两个命题之间的路径就是它们之间的双向蕴含，而双向蕴含本身是命题，所以命题之间的相等除真假之外不携带任何额外结构。正是这条事实使 hProp 有资格在下一章充当真值类型 (isSetΩ 字段要求的恰是它)。isPropΠ 说的是命题在 Π 类型下封闭：若对每个 x，B x 都是命题，则 (x : A) → B x 也是命题。这就是全称量化的真值仍是真值的原因。

open import Cubical.Foundations.HLevels public
  using ( hProp; isSetHProp; isPropΠ )

⟨_⟩ (读作「延展」) 把底层类型从 hProp 中投影出来；对 P : hProp ℓ，其命题性证明就是 P .snd，本书不为它另设名字。

open import Cubical.Foundations.Structure public
  using ( ⟨_⟩ )

随行的还有一个派生记号。载体 A 上的类是命题值谓词 A → hProp ℓ，而 x ∈ᶜ M (读作「x 属于类 M」) 恰是 ⟨ M x ⟩：库的幂集成员关系，换上带标记的名字。上标 ᶜ 说的就是类，把这个记号与后文诸对象层成员关系区分开，后者指称集合，而非宿主层的谓词。

open import Cubical.Foundations.Powerset public
  using () renaming ( _∈_ to _∈ᶜ_ )

依值对：Σ 及其糖衣 Σ-syntax、普通的积 _×_、配对 _,_，以及投影 fst 与 snd。Σ 类型是本书「把东西与它的性质捆在一起」的方式。

open import Cubical.Data.Sigma public
  using ( Σ; Σ-syntax; _×_; _,_; fst; snd )

自然数 ℕ，构造子 zero 与 suc。一切有限事物都由它们索引，首先就是公式的自由变量个数。

open import Cubical.Data.Nat public
  using ( ℕ; zero; suc )

向量：Vec A n 是恰含 n 个 A 元素的表，由 [] 与 _∷_ 构造，用 lookup 查询。向量是变量环境的原材料，将在第一部登场。

open import Cubical.Data.Vec public
  using ( Vec; []; _∷_; lookup )

Fin n 是恰有 n 个元素的类型；它将充当 n 元公式的变量类型。其构造子与自然数同名 zero、suc，由类型检查器消歧。

open import Cubical.Data.FinData public
  using ( Fin; zero; suc )

最后是层级多态的空类型 ⊥*，连同 isProp⊥*。注意星号：这是宿主层的类型，层级随需而定，不是下一章的真值 ⊥。

open import Cubical.Data.Empty public
  using ( ⊥*; isProp⊥* )

本章以唯一一个自家定义收尾，而且是能想象的最小的一个：层级多态的恒等函数。它凭一个身份落户枢纽：本书的典范常量解释。常量就代表它指名的那个集合，说的恰是 id。

id : ∀ {ℓ} {A : Type ℓ} → A → A
id x = x

小结

自此进入作用域的有：宇宙、路径、h-层级、hProp 与 ⟨_⟩ 及类隶属 ∈ᶜ、对与积、ℕ、Vec、Fin、⊥*，以及恒等 id。本章不证明任何东西，自家定义仅 id 一个，逻辑符号也刻意缺席：本书的每个概念都在它初次派上用场的章节引入，而逻辑随下一章的真值代数登场。