Impredicativity

宿主的宇宙排成一架梯子，而梯子反复抛出同一个问题：住在高一层的东西，在低层有没有替身？对命题而言，这个问题正是非直谓性的标志：真值的世界拒绝随宇宙一起膨胀。本章铸下这套词汇：单个命题「是小的」是什么意思，一揽子断言小性的两个接口，以及它们的打包。此处无所假设、亦无所证明；这些是接口。下一章将用排中律把它们全部赎回，第三部则恰以这种货币为具体的模型字段标价。

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

module Base.Impredicativity where

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

何谓小

高一层的命题是小的，指它与某个低一层的命题等价。定义随身携带见证：手握 isSmall P 的居民，就是手握小替身连同那份等价。第三部的小性一章将把传递这种见证做成一整套体操，逐原子地挣得实例，不花任何公理。

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

两个接口

命题降层是一揽子断言：高一层的每个命题都是小的。这正是经典集合论从不操心命题住在哪个宇宙的确切原因。与 LEM 同款，逐层级陈述。

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

第二个接口谈的不是单个命题，而是它们的总体：真值类型本住在高一层宇宙，却等价于一个小类型。HPropSmallness ℓ 索要一个与 hProp ℓ 等价的小类型，即命题的小分类器。

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

打包

两件器具共有一种品格，各自以各自的口吻说着「命题拒绝随宇宙膨胀」这一句话；它们也共享消费者，于是打包成一个接口，逐层级陈述。打包依据是共同消费而非相互蕴含：两件器具谁也推不出谁 (它们分别源自 Voevodsky 两条分立的 resizing 公理)。这个接口不谈任何特定结构，是纯粹的宇宙层级政策。

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

小结

命题的小性即与低层替身的等价 (isSmall)；Resizing 将它断言于每个命题，HPropSmallness 断言于它们的总体，Impredicativity 把两者打包。以上全是词汇，无一被假设。下一章：本书唯一诉诸的经典原理，以及用它对本章的整体赎回。