经典逻辑的边界

在带宇宙层级的类型论中，命题引出两个不同的小性问题。第一，固定命题 P : hProp (ℓ-suc ℓ)，能否找到低一层宇宙中与之等价的命题？这就是命题降级：它逐个命题发言。第二，全体 ℓ 层命题的类型 hProp ℓ 本身住在 Type (ℓ-suc ℓ) 中；能否用一个小类型呈现整个总体？这就是小分类器。两项断言形状不同，本章由一条显式假设同时证明二者。

这条假设是排中律：给定层级的每个命题要么真要么假。Cubical 类型论并不预设它，因此这里的每个经典证明都把它作为显式参数接收，每项结果也准确记录所用的是哪个层级的实例。构造性定义与经典步骤全程分开：构造自身不作任何判定，假设只在消耗判定之处进入。

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

module Base.Classical where

两个小性问题已在「非直谓性」一章获得精确形状，本章原样使用那套词汇。对单个命题，isSmall P 由一个低层命题 Q : hProp ℓ 与底层类型间的等价 ⟨ P ⟩ ≃ ⟨ Q ⟩ 组成。两个统一陈述的区别在于量化的对象：Resizing ℓ 要求每个 P : hProp (ℓ-suc ℓ) 都带有这样的数据，而 HPropSmallness ℓ 要求一个与整个 hProp ℓ 同时等价的类型 Ω' : Type ℓ。前者是逐命题见证的族，后者是呈现总体的单一载体；本章从排中律分别导出二者，并且不断言二者之间有蕴含关系。

open import Base.Prelude
open import Base.Impredicativity
  using ( isSmall; Resizing; HPropSmallness; Impredicativity )

判定一个命题意味着什么，必须先于一切证明固定下来。判定 P，就是给出 ⟨ P ⟩ 的一个证明，或给出从 ⟨ P ⟩ 到空类型的映射：后者把任何证明都变成荒谬，从而反驳 P。余积 _⊎_ 及其两个构造子承载的正是这种二选一，而且这个析取是真实的数据：元素知道自己来自哪一支，因此判定能够逐情形使用。布尔值 Bool 与 true、false 将为两种结果贴标签，tt* 则是「真」命题底层单元类型的唯一元素。

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Bool using ( Bool; true; false )
open import Cubical.Data.Unit using ( tt* )

小性通过「相同」来比较命题，下文会出现两种形式的相同。在两个命题之间，双向的一对映射既能经命题外延性 ⇔toPath 给出 hProp 值之间的路径，也能经 propBiimpl→Equiv 给出底层类型间的等价。同构 iso 把两个映射与两条逆律一并记录，isoToEquiv 把它读作等价。分类器要等同命题，所以构造 hProp 的路径；命题降级要交付底层类型间的等价。

open import Cubical.Foundations.Equiv using ( propBiimpl→Equiv )
open import Cubical.Foundations.Isomorphism using ( iso; isoToEquiv )
open import Cubical.Functions.Logic using ( ⇔toPath )

陈述

在证明任何东西之前，必须先把假设连同其宇宙层级陈述清楚。层级指标不是装饰：它说明在哪个宇宙上要求统一判定，后续每个定理都在向读者交代它需要哪个经典实例。

对每个宇宙层级 ℓ，LEM ℓ 是一个函数：取命题 P : hProp ℓ，返回 ⟨ P ⟩ 的证明，或一个反驳，即从 ⟨ P ⟩ 映入空类型的映射。由于它量化了 hProp ℓ 的所有命题，其类型位于高一层宇宙 Type (ℓ-suc ℓ)。因此这个陈述本身是大的，尽管它产出的每个判定都只是一小段数据；而且 LEM ℓ 是逐层陈述的，不是同时对所有层级断言。注意这种形状给出的强度：判定是数据而非命题，所以从排中律假设出发，可以在证明与反驳两种情形之间作分支推理，而不只是断言二者之一存在。

LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)

应用需要在不止一个层级上的排中律，而证明拿到的往往只有高层实例 LEM (ℓ-suc ℓ)。一条下降引理补上这个缺口。它是恰好一步的结果，即 LEM (ℓ-suc ℓ) → LEM ℓ：要判定 P : hProp ℓ，在上一层宇宙判定 P 的抬升副本，再把裁决带回。这里不声称判定可以一次跨越任意多层下降。

给定 lem : LEM (ℓ-suc ℓ) 与命题 P : hProp ℓ，计划不是把 lem 用在 P 本身上，而是用在住在 ℓ-suc ℓ 层、因而假设可适用的 P 的抬升副本上，然后再把关于副本的裁决翻译回关于 P 的裁决。

lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ
lowerLEM {ℓ} lem P = fromLifted (lem lifted)

抬升后的命题底层类型为 Lift ⟨ P ⟩，其元素就是高一层宇宙中的 ⟨ P ⟩ 元素，而且它是命题：对元素 x 与 y，先用 lower 把二者降到 ⟨ P ⟩，用 P 的命题性 P .snd 得到降像之间的路径，再用 cong lift 把该路径抬回上层。于是 lifted 是 lem 的合法输入。

  where
  lifted : hProp (ℓ-suc ℓ)
  lifted = Lift ⟨ P ⟩ , λ x y → cong lift (P .snd (lower x) (lower y))

翻译裁决只需要 lift 与 lower，而它们的方向恰好合适。Lift ⟨ P ⟩ 的证明经 lower 降为 ⟨ P ⟩ 的证明；Lift ⟨ P ⟩ 的反驳与 lift 复合后成为 ⟨ P ⟩ 的反驳，因为它在抬升之后适用于 ⟨ P ⟩ 的任何证明。两种情形都是判定的纯粹搬运，自身不含经典推理；经典的步骤是判定那个抬升后的命题。

  fromLifted : ⟨ lifted ⟩ ⊎ (⟨ lifted ⟩ → Empty.⊥) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
  fromLifted (inl p)  = inl (lower p)
  fromLifted (inr np) = inr (λ p → np (lift p))

由排中律得到小分类器

在经典观点下，固定层级的每个命题只有两种可能：真或假。这提示了一个两点的分类器。小代表取 Lift Bool，其中 true 代表命题「真」，false 代表命题「假」。有两点提醒使图景保持准确。布尔值只是标签；它所代表的命题是另一个 hProp 值，分类器只按 hProp 值之间的路径把它们等同，绝不按语法上的同一。并且两端大小不同：Lift Bool 住在 Type ℓ，而 hProp ℓ 住在 Type (ℓ-suc ℓ)；等价可以联系不同层级的类型，这个大小差正是所要建立的小性。

构造分成干净的两步。解码把每个布尔值送到它代表的命题。编码则需要知道给定的 P 属于哪种情形，因此把 P 的判定作为显式参数；两条逆律随后针对这份数据证明。排中律只在最后出现，用于一致地供给这些判定。

两个代表命题是《基础词汇》逻辑运算中典范的顶命题 ⊤ 与底命题 ⊥。后者按定义就是对 (⊥* , isProp⊥*)，因此其底层类型是空类型 ⊥*。二者在任意层级 ℓ 都可用，这正是它们能在 hProp ℓ 内部充任代表的原因；下面的布尔标签指称的恰是这两个命题。

private
  decodeB : ∀ {ℓ} → Lift {ℓ-zero} {ℓ} Bool → hProp ℓ

解码读取布尔标签，返回它所代表的命题：lift true 给出 ⊤，lift false 给出 ⊥。定义域是提升 Lift {ℓ-zero} {ℓ} Bool 而非 Bool 本身：Bool 住在 Type ℓ-zero，其提升是 Type ℓ 中的类型，这正是分类器陈述所要求的。注意，单独的解码只是一个指派代表的函数；这个指派在两个方向上都忠实，是下面两条逆律的内容。

  decodeB (lift true)  = ⊤
  decodeB (lift false) = ⊥

编码是相反方向的指派：给定 P 与 P 的一个判定，返回获胜情形的标签。判定是显式参数而非编码器自己产出的，所以这一步不使用排中律。一般而言，为 P 选代表是两步的事：先判定 P，再读出标签。两条逆律将表明这两趟往返各自是恒等，一趟在命题上，一趟在标签上。

匹配对象是判定而非 P：左支的元素给出 lift true，右支的元素给出 lift false。证明或反驳本身被丢弃，因为标签只记录出现的是哪种情形，而不是见证。结果类型是 Lift {ℓ-zero} {ℓ} Bool，与 decodeB 的定义域严格相配。

  encodeB : ∀ {ℓ} (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → Lift {ℓ-zero} {ℓ} Bool
  encodeB P (inl _) = lift true
  encodeB P (inr _) = lift false

第一条逆律说，经由判定选出的代表与 P 有相同的真值。具体地，secB 证明 decodeB (encodeB P d) ≡ P，这是 hProp 值之间的一条路径。两种情形的证明策略相同：给出双向的映射，再由命题外延性 ⇔toPath 组装出路径。

若判定是证明 p，目标是 ⊤ ≡ P。从 ⊤ 到 ⟨ P ⟩ 的映射就是判定所得的见证 p；反方向上，所有输入都映到 ⊤ 的唯一元素 tt*。若判定是反驳 np，目标是 ⊥ ≡ P。从 ⊥* 出发没有构造子可匹配，荒谬模式 λ () 表达的正是这一点；⟨ P ⟩ 的每个证明 p 都交给 np 并由 Empty.rec 消去。两个分支中，所选代表都与 P 路径相等，于是编码的往返不丢失任何真值。

  secB : ∀ {ℓ} (P : hProp ℓ) (d : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥))
       → decodeB (encodeB P d) ≡ P
  secB P (inl p)  = ⇔toPath (λ _ → p) (λ _ → tt*)
  secB P (inr np) = ⇔toPath (λ ()) (λ p → Empty.rec (np p))

第二条逆律把代表读回来：encodeB (decodeB b) d ≡ b。这里有个关键细节。在组装好的分类器中，判定 d 将由排中律产生，而任何东西都不保证那个判定如何计算。所以 retrB 必须对每一个判定 d 成立，而不是只对某个特定证明会供给的判定成立。证明因此分成四种情形：两个相容的分支计算为 refl，两个不相容的分支作为不可能而消去；这也表明两个代表不会被混淆，因为 ⊤ 有元素而 ⊥ 为空。

当 b = lift true 时，解码得 ⊤。配以证明编码返回 lift true，目标按定义就是 refl。所谓反驳的分支不可能出现：把它用于 ⊤ 的元素 tt* 会得到空类型的元素，Empty.rec 便由这一矛盾结案。

  retrB : ∀ {ℓ} (b : Lift {ℓ-zero} {ℓ} Bool)
          (d : ⟨ decodeB b ⟩ ⊎ (⟨ decodeB b ⟩ → Empty.⊥))
        → encodeB (decodeB b) d ≡ b
  retrB (lift true)  (inl _)  = refl
  retrB (lift true)  (inr n⊤) = Empty.rec (n⊤ tt*)

当 b = lift false 时，解码得 ⊥，其底层类型为 ⊥*。它的所谓证明将是空类型的项，荒谬模式 () 立即结束该分支；配以反驳编码返回 lift false，同样由 refl 完成。纵观四种情形，无论供给哪种判定，返回的标签总等于出发时的标签。

  retrB (lift false) (inl ())
  retrB (lift false) (inr _)  = refl

现在各部分组装成 HPropSmallness ℓ 所承诺的分类器：一个 Type ℓ 中的、与 hProp ℓ 等价的类型。小类型是 Lift Bool；等价来自这样的同构：正向映射是 decodeB，反向映射判定 P 后编码。两条逆律正是 secB 与 retrB，各自用来自 lem 的判定实例化。排中律在本节的作用就在此处：它一致地供给那些构造性部分作为输入所需的判定。

对子 (Lift Bool , ...) 是 HPropSmallness ℓ 的见证：第一分量类型为 Type ℓ，第二分量是等价 Lift Bool ≃ hProp ℓ。层级安排正是要点：Lift Bool : Type ℓ 而 hProp ℓ : Type (ℓ-suc ℓ)，于是高一宇宙的类型获得了一个小代表。这是关于宇宙层级的尺寸陈述，不是声称两端共享同一个宇宙；而且等价本身依赖两条逆律，因此布尔标签与其命题只是在 secB 与 retrB 所认证的路径之下被等同。

lem→hPropSmallness : ∀ {ℓ} → LEM ℓ → HPropSmallness ℓ
lem→hPropSmallness lem = Lift Bool , isoToEquiv (iso decodeB
  (λ P → encodeB P (lem P))
  (λ P → secB P (lem P))
  (λ b → retrB b (lem (decodeB b))))

由排中律得到命题降级

第二个小性问题是逐命题的。固定 P : hProp (ℓ-suc ℓ)，命题降级产出命题 Q : hProp ℓ 以及底层类型间的等价 ⟨ P ⟩ ≃ ⟨ Q ⟩。同样的两个代表再次可用：若 P 为真取 ⊤，若为假取 ⊥，二者都在 ℓ 层。注意结果的形状：它是底层类型间的等价，而不是打包命题 P 与 Q 之间的路径。

两个构造的差别在于所组装的「相同」是什么。分类器要等同命题，所以它的相同由命题外延性组装为 hProp 值之间的路径。命题降级要交付的则是底层类型间的等价，propBiimpl→Equiv 恰好产出它：输入两侧的命题性证明 P .snd 与 Q .snd 连同两个映射，返回 ⟨ P ⟩ ≃ ⟨ Q ⟩。

给定 P 的一个判定，resizeDec 返回 isSmall P 的见证。真情形的见证是 (⊤ , 等价)：从 ⟨ P ⟩ 到 ⊤ 的映射把所有输入映到 tt*，返回的映射使用判定所得的证明 p。由于两侧都是命题，propBiimpl→Equiv 在收到命题性证明 P .snd 与 ⊤ .snd 后，把这组映射变成底层类型间的等价。

private
  resizeDec : ∀ {ℓ} (P : hProp (ℓ-suc ℓ)) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
            → isSmall P
  resizeDec P (inl p)  = ⊤ , propBiimpl→Equiv (P .snd) (⊤ .snd) (λ _ → tt*) (λ _ → p)
  resizeDec P (inr np) = ⊥ , propBiimpl→Equiv (P .snd) (⊥ .snd)

假情形的见证是 (⊥ , 等价)，映射与 secB 中的相同：从 ⟨ P ⟩ 出发的映射用反驳 np 经 Empty.rec 处理每个证明 p，反向映射则当场荒谬，因为 ⊥* 没有构造子。两个代表 ⊤ 与 ⊥ 都住在比 P 低一层的 ℓ 层，这正是所要认证的小性：Q 取自 hProp ℓ 内部，等价连接 ⟨ P ⟩ 与 ⟨ Q ⟩。

                               (λ p → Empty.rec (np p)) (λ ())

命题降级由此从 ℓ-suc ℓ 层级上排中律的一个实例得到，而这个层级是陈述自身规定的：Resizing ℓ 量化 hProp (ℓ-suc ℓ)，它消耗的判定恰是高一宇宙命题的判定。

lem→resizing 用一行把 LEM (ℓ-suc ℓ) 变为 Resizing ℓ：对每个 P : hProp (ℓ-suc ℓ)，用 lem 判定它，把裁决交给 resizeDec。关键全在层级的方向：ℓ 层的命题降级消耗 ℓ-suc ℓ 层的经典判定，因为获得低层等价代表的命题恰好是高一宇宙中的那些。

lem→resizing : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Resizing ℓ
lem→resizing lem P = resizeDec P (lem P)

合并两项结论

两项尺寸控制现在来自同一条假设。LEM (ℓ-suc ℓ) 的一个实例直接给出命题降级，又经 lowerLEM 下降一步给出小分类器。两条原理仍是不同的陈述：本章从同一假设证明二者，但对其中一条是否蕴含另一条不作断言。

「非直谓性」一章中的记录 Impredicativity ℓ 有两个字段，每条原理各一个，而 lem→impredicativity 用同一个 lem 填满两者。命题降级字段是 lem→resizing lem，在该实例自身的层级上使用它。分类器字段是 lem→hPropSmallness (lowerLEM lem)，先降到 LEM ℓ，再构造 Lift Bool ≃ hProp ℓ。共享是关于这个推导的事实：两项结论都从同一个高层实例可证，而不是宣称两条原理相互蕴含。

lem→impredicativity : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Impredicativity ℓ
lem→impredicativity lem = record
  { resizing       = lem→resizing lem
  ; hPropSmallness = lem→hPropSmallness (lowerLEM lem) }

小结

本章中的排中律只有一件事：在给定层级上判定每个命题的能力，且始终作为显式假设传递。一个 ℓ-suc ℓ 实例供给了全章所需的判定。它为 lowerLEM 判定各个抬升命题，为命题降级判定各个 P : hProp (ℓ-suc ℓ)，又经一步下降，为小分类器判定每个 P : hProp ℓ。两项推论仍是不同的原理，本章未对二者作任何比较；lem→impredicativity 同时持有二者，是因为同一条假设恰好给出了二者。累积层级诸章将接过这一接口，在全分离与 V 的幂集背后需要小性的地方加以使用。