可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

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

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

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

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

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

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

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

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

open hPropView 𝒮ᵥ

满足性质的最小序数

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

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

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

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

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

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

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

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

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

  decide (inl α∈α')       = ⊥₀-rec (leastα' α ordα pα α∈α')
  decide (inr (inl e))    = e
  decide (inr (inr α'∈α)) = ⊥₀-rec (leastα α' ordα' pα' α'∈α)
  α≡α' : α ≡ α'
  α≡α' = decide (ord-tri α ordα α' ordα')

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

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

下降到最小序数

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

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

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

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

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

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

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

    decide (yes ∃β) = rec₁ isPropLeastOrd
      (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β
    decide (no ¬∃β) = α , ordα , pα , leastProof
      where
      leastProof : isLeastOrd α

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

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

leastOrd : ∥ (Σ[ α ∶ S ] (IsOrd α × ⟨ P α ⟩)) ∥₁ → LeastOrd
leastOrd = 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 应用于这条性质。因此，可构造性恰好提供了取得最小层索引所需的截断存在前提。

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 投影出该索引，并保持其递归构造不透明，使后续论证使用序数性、层成员关系与极小性。它以可构造集合及其见证为输入并返回序数；它既不是宇宙层级，也不是秩函数。

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 恰是章首承诺的那个最小索引，只是经由投影、而非重新打开递归而得到。

  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 精确陈述这些事实。后续论证因而可以比较或约束这些序数索引，再使用对应的可构造层。