---
title: "最小可构造层的索引"
module: L.Stage
lang: zh
site: "Bedrock"
description: "最小可构造层的索引"
stage: "可构造层与公理"
reading_order: 30
canonical: https://bedrock.institute/zh/L.Stage.html
html: L.Stage.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Stage.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal.Linear]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Stage.md, https://bedrock.institute/ja/L.Stage.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 最小可构造层的索引

每个可构造集合 x 至少属于一个序数 α 所索引的 `Lset α`。本章把这种仅仅存在化为一个典范界：包含 x 的最小层之序数索引。证明先解决更一般的问题。对序数上的任意 hProp 值性质 P，良基下降找出其最小见证，序数三歧则证明所得见证唯一。

下降从任意满足 P 的序数开始。在 α 处，询问是否有更小的 β ∈ α 也满足 P；肯定答案调用 β 处的归纳结果，否定答案则证明 α 最小。成员关系归纳使这一定义保持良基。「存在更小见证」的断言与初始见证都经过命题截断，但 `LeastOrd P` 本身是命题，因此每处截断都可以消去到这个完整包。

把 P σ 特化为 x ∈ Lset σ，便得到 `stage x hx`。配套定理说明该索引是序数、其层包含 x，且没有更小的序数层包含 x。证明使用排中律的地方只有判定更小见证是否存在，以及比较两个候选序数。

固定宇宙层级 ℓ，并假设层级 ℓ-suc ℓ 上的排中律。这个假设有两种不同的数学用途：`ord-tri` 比较候选序数，而下降过程判定「存在更小候选」这一 hProp。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Stage {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

隶属关系既给出序数上的严格序，也给出其良基归纳原理。可构造性一侧提供谓词 IsOrd、层族 Lset，以及断言 x 出现在某个序数索引层中的 isL x。因此，同一个隶属关系既控制候选索引之间的下降，也在特化后表达 x 属于某一层。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
open import L.Constructible {ℓ} using ( IsOrd; isPropIsOrd; Lset; isL )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
```

「存在更小见证」用命题截断的存在式表示，只记录存在而不暴露选定的 β。消去子 `PT.rec` 只能在目标是命题时使用这份证据；下面的唯一性证明恰好说明 `LeastOrd P` 是命题。积与依赖函数空间保持命题性，这也将说明固定序数索引所附的证据唯一。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
open import Cubical.Data.Sigma using ( Σ≡Prop )
```

性质 P 是到 Ω，即 hProp 类型的映射。因此，`⟨ P α ⟩` 是 P 在 α 处的底层命题，而 `snd (P α)` 证明其任意两个见证相等。当序数索引的相等被提升为完整最小见证包的相等时，正需要这一命题性。

```agda
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )

open hPropStructure 𝒮ᵥ
```

## 满足性质的最小序数

对于序数性质 `P`，`LeastOrd P` 由满足 `P` 的序数 α 和「没有更小序数满足 `P`」的证明组成。这个定义谈的是序数索引本身；直到稍后取 `P σ = (x ∈ Lset σ)`，这样的索引才成为某个可构造层的索引。

唯一性正用到该性质取值于 `hProp` 这一事实：两个候选经三歧比较，每个严格方向都被对方的极小性反驳，而其余分量都是命题，故序数相等即是二者作为整体相等。

极小性被表述为一个反驳：`isLeastOrd α` 断言，对任意集合 γ，γ 不可能是满足 P 的序数且有 γ ∈ α。这里用反证表述极小性是合适的形状，因为序数上的严格序正是经由成员关系读出的；没有「更小序数」这样的值可供返回，只有要导出的不可能局面。整体包 `LeastOrd` 则把序数、其序数性、在该处 P 的证明，以及这条极小性条款捆在一起。

```agda
module _ (P : S → hProp (ℓ-suc ℓ)) where

  isLeastOrd : S → Type (ℓ-suc ℓ)
  isLeastOrd α = (γ : S) → IsOrd γ → ⟨ P γ ⟩ → ⟨ γ ∈ˢ α ⟩ → Empty.⊥

  LeastOrd : Type (ℓ-suc ℓ)
  LeastOrd = Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩ × isLeastOrd α)
```

要证两个这样的包相等，先比较它们的序数索引。三歧给出三种情形：α ∈ α′、α = α′ 或 α′ ∈ α。计划是：用反证消去两个严格情形，保留相等情形；`decide` 就是把这份三歧结果变成路径 α ≡ α′ 的函数。关键在于，这一步只证得索引相等；而包是在索引上的依赖对，故仅有索引相等还得不到包的相等。

```agda
  isPropLeastOrd : isProp LeastOrd
  isPropLeastOrd (α , ordα , pα , leastα) (α' , ordα' , pα' , leastα') =
    Σ≡Prop propRest α≡α'
    where
    decide : (⟨ α ∈ˢ α' ⟩ ⊎ ((α ≡ α') ⊎ ⟨ α' ∈ˢ α ⟩)) → α ≡ α'
```

每个严格情形都与极小性矛盾，但那是与**另一个**候选的极小性矛盾。若 α ∈ α′，则 α 是严格低于 α′ 且满足 P 的序数，`leastα'` 反驳的恰是这一点；α′ ∈ α 的情形对称，用 `leastα`。中间情形就是路径本身。把 `ord-tri` 的裁决送入 `decide`，即得路径 `α≡α'`。注意，到目前为止，除「P 的取值是命题」外，未对 P 使用任何假设。

```agda
    decide (inl α∈α')       = Empty.rec (leastα' α ordα pα α∈α')
    decide (inr (inl e))    = e
    decide (inr (inr α'∈α)) = Empty.rec (leastα α' ordα' pα' α'∈α)
    α≡α' : α ≡ α'
    α≡α' = decide (ord-tri α ordα α' ordα')
```

剩下要把索引的路径提升为包的路径，这里要用到依赖剩余分量的命题性。随索引变化的分量是 `IsOrd β × ⟨ P β ⟩ × isLeastOrd β`：`IsOrd β` 由可构造章知是命题；因 P 取值于 hProp，`⟨ P β ⟩` 是命题；`isLeastOrd β` 是到空类型的函数类型，经 `isPropΠ` 迭代即知是命题。于是 `propRest β` 证明了整个剩余分量的命题性，`Σ≡Prop` 把基础路径变成所需的包的相等：索引一旦一致，依赖的剩余分量便不可能不一致。

```agda
    propRest : (β : S) → isProp (IsOrd β × ⟨ P β ⟩ × isLeastOrd β)
    propRest β = isProp× (isPropIsOrd β)
      (isProp× (snd (P β))
        (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → Empty.isProp⊥))
```

## 下降到最小序数

从任一满足 `P` 的序数出发，`leastOrdBelow` 询问是否有严格更小的序数也满足 `P`，若有便递归下降。成员关系归纳由严格更小序数处的结果定义当前结果，从而得到满足 `P` 的最小序数；此时构造尚未特化到可构造层。

结果既是命题，起始序数便可以截断的形式给出，而这正是各调用方实际具有的形式：它们知道合用的序数存在，却未曾选定一个。

下降按成员关系上的良基归纳来组织，即层级章的原理 `∈-induction`。其步进收到的参数有：序数 α、其序数性、在 α 处的 P 的证明，以及对每个严格更小成员 β 可用的归纳假说：只要 β 又是满足 P 的序数，从 β 开始归纳所得的全局最小 P 见证便已在手。步进唯一的任务，就是在 α 处判定下降该继续还是已经抵达。

```agda
  leastOrdBelow : (α : S) → IsOrd α → ⟨ P α ⟩ → LeastOrd
  leastOrdBelow = ∈-induction step
    where
    step : (α : S) → (∀ β → ⟨ β ∈ˢ α ⟩ → IsOrd β → ⟨ P β ⟩ → LeastOrd)
         → IsOrd α → ⟨ P α ⟩ → LeastOrd
```

要判定的问题是 `Smaller`：是否仅仅存在某个 β，使 β ∈ α、β 是序数且满足 P；诸条件用合取打包成一个 hProp。有两点要紧。其一，这个存在式是截断的：`Smaller` 不携带选定的 β，只声称存在一个。其二，层级 ℓ-suc ℓ 上的排中律经 `lem` 直接判定这个问题，交付截断的一个元素或一个反驳。这正是经典假设进入下降之所在。

```agda
    step α IH ordα pα = decide (lem Smaller)
      where
      Smaller : hProp (ℓ-suc ℓ)
      Smaller = ∃[ β ∶ S ] ((β ∈ˢ α) ⊓ ((IsOrd β , isPropIsOrd β) ⊓ P β))
      decide : (⟨ Smaller ⟩ ⊎ (⟨ Smaller ⟩ → Empty.⊥)) → LeastOrd
```

判定的两个分支都直接构造答案。在肯定分支里，截断的见证不能拆成数据，但 `PT.rec` 可以把它消去到任何命题，而 `LeastOrd` 恰是命题：于是这个见证在被消去而非被选定的意义上，转化为归纳假说在 β 处给出的全局最小包。在否定分支里根本不存在更小的见证，故 α 自身就是最小的。递归只经由 `∈-induction` 受控的归纳假说发生。

```agda
      decide (inl ∃β) = PT.rec isPropLeastOrd
        (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β
      decide (inr ¬∃β) = α , ordα , pα , leastProof
        where
        leastProof : isLeastOrd α
```

否定分支的极小性条款正是反驳发挥作用之处：给定 α 之下任何满足 P 的序数 γ，把见证 `(γ , γ∈α , ordγ , pγ)` 打包进恰好被否认的那个截断 `Smaller`，再对它施加 `¬∃β` 即得所需矛盾。最后，`leastOrd` 处理调用方实际具有的形式：满足 P 的序数仅仅存在。再次地，向 `LeastOrd` 的消去由上一节证明的命题性所许可，于是截断的存在被精炼成典范的最小索引，且没有把截断消去到任意数据类型。

```agda
        leastProof γ ordγ pγ γ∈α = ¬∃β ∣ γ , (γ∈α , (ordγ , pγ)) ∣₁

  leastOrd : ∥ (Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩)) ∥₁ → LeastOrd
  leastOrd = PT.rec isPropLeastOrd
    (λ { (α , (ordα , pα)) → leastOrdBelow α ordα pα })
```

## 层索引函数

取 `P σ = (x ∈ Lset σ)` 后，下降得到最小序数索引 α，使层 `Lset α` 包含 `x`。函数 `stage` 选出 α，`stage-ord` 证明它是序数，`stage-mem` 与 `stage-earliest` 则把这个索引与相应层联系起来。

这个索引通过三条稳定事实给出，而不依赖递归构造本身：它是序数、其层包含 x，并且在具有该性质的序数索引中最小。把 `stage` 声明为 opaque 保持了这一抽象边界。

可构造性证书 `⟨ isL x ⟩` 恰是 `leastOrd` 所期望的输入形式：按可构造章中类的定义，`isL x` 的一个元素仅仅是序数 σ、其序数性、以及隶属 `x ∈ˢ Lset σ` 的一个对。于是性质 `λ σ → x ∈ˢ Lset σ` 满足下降的假设，而 `theEarliest` 把 `leastOrd` 应用于这条性质。因此，可构造性恰好提供了取得最小层索引所需的截断存在前提。

```agda
theEarliest : (x : S) → ⟨ isL x ⟩ → LeastOrd (λ σ → x ∈ˢ Lset σ)
theEarliest x = leastOrd (λ σ → x ∈ˢ Lset σ)

opaque
  stage : (x : S) → ⟨ isL x ⟩ → S
  stage x p = theEarliest x p .fst
```

包 `theEarliest x p` 含有最小索引及其三项证明。函数 `stage` 投影出该索引，并保持其递归构造不透明，使后续论证使用序数性、层隶属与极小性。它以可构造集合及其见证为输入并返回序数；它既不是宇宙层级，也不是秩函数。

```agda
opaque
  unfolding stage
  stage-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (stage x p)
  stage-ord x p = theEarliest x p .snd .fst

  stage-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (stage x p) ⟩
```

这三条定理就是接口，每条都是该包的一个投影。`stage-ord` 说所选索引是序数，因而日后可以与其他索引比较。`stage-mem` 把 `x` 放进层 `Lset (stage x p)`，这正是下降所建立的隶属事实。`stage-earliest` 则取回极小性条款本身：没有更小的序数 σ 使 `x ∈ˢ Lset σ`。合起来，它们说 `stage x p` 恰是章首承诺的那个最小索引，只是经由投影、而非重新打开递归而得到。

```agda
  stage-mem x p = theEarliest x p .snd .snd .fst

  stage-earliest : (x : S) (p : ⟨ isL x ⟩)
                 → isLeastOrd (λ σ → x ∈ˢ Lset σ) (stage x p)
  stage-earliest x p = theEarliest x p .snd .snd .snd
```

## 小结

`leastOrd` 从截断的存在见证中提取满足某条性质的最小序数。其特例 `stage x hx` 返回包含 `x` 的最小 `Lset α` 的序数索引 α；`stage-ord`、`stage-mem` 与 `stage-earliest` 精确陈述这些事实。后续论证因而可以比较或约束这些序数索引，再使用对应的可构造层。