L 内部的可构造层级

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

L 内的一阶图记录外部的可构造层级，直至给定序数。表中的值与外部层级逐一对照，被证明具有函数性且精确；随后这些对被收集成一个可构造集合，其元素恰是此前各层。

本章构造内部层级。对层级中的序数 α，hierL 在 α 处是 L 的一个元素，其元素恰是有序对「低于 α 的序数 β 与塔在该处的取值 Lset β」。全章重复同一个模式。表是有序对之集；说它在集合 B 上正确，指它在 B 以下记录的每个取值都是元层面的塔在那里的取值；说它完备，指它在以下的每个实参处都记录了取值。正确且完备的表，恰是图的步进条件所读出的内容，也恰是步进条件据以写下的内容；因此连接步进与塔的那对引理同时服务于消去与引入。

本章在模型自身层级的后继处取一份排中律实例并在其下运行；以下每个构造都陈述于本模块之内，只在公理章传递之处携带这一假设。

这里有两个结构。环境层级贡献其结构 𝒮ᵥ，本章将使用它的成员关系归纳与外延性；可构造结构 𝒮ʟ 贡献载体 S，其元素是层级中的集合连同「其可构造」的证明，故每个载体元素 x 都有底层集合 x .fst。

层级给出全章使用的三件工具：沿成员关系的归纳、集合的外延性，以及有序对 pr 连同找回其分量的单射性。这个对住在层级那一层，而表的被记录条目也住在那里。

可构造一侧给出塔 Lset，它把层级的一个序数送到该处的可构造层；可定义幂集 𝒟ₒ；两条成员关系读式 Lset-in 与 Lset-out；序数性 IsOrd；以及「可构造性沿成员关系传递」这一事实。塔由序数索引，序数是层级的集合；从不由宇宙层级索引，后者是类型的大小指标。

另有三件事实支撑全章：序数的元素是序数；一个层可以呈现为 L 的元素，记作 LsetS，且可构造集合的可定义幂集仍可构造；以及 L 内部可用替换，其形式接受「仅知唯一存在」的取值。

模型贡献它自己的有序对 prʟ，连同识别其第一投影的读式 prʟ-fst，以及定义域子句 domAt-intro。

前一编码章贡献本章要组装的词汇：带见证与三条读式的步进条件，带定义域、取值与步进子句的逼近，有两条读式的塔之图，以及有序对图。

命题机制是常用的那一套：截断的存在、其注入与消去、「第二分量为命题的序对在第一分量相等时即相等」，以及把成员关系的逐点等价转成集合路径的操作。

层级自身以类型的身份出现：其元素正是本章制表的对象，其成员关系是三个条件所谈论的关系，而其 h-集合性使两个被制表集合的相等成为命题。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

在可构造结构内部，S 是载体，⊨ 是满足判断；SetOf 把候选集合与「它实现一个类」的断言配成对，record 的各字段正是以这种形式陈述其公理。

open hPropView 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

满足关系最终在可构造结构处读取：全章的记号 γ ⊨ φ 都是在载体元素的环境处、以取自 L 的常元判断对象语言公式。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

一个私有辅助把变元槽后移两位：当一步要在「先加取值、再加实参」而扩展的环境中判读时，所有旧槽都后移两位。凡从表自身的条目内部判读该表的步进时，它都会出现。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

表记录什么

表是有序对之集，这里总是取层级配对所成的对：一个实参连同一个取值。三个条件刻画表在界集 B 上的样子，它们是互补的条件，而不是同一句陈述的三种读法。Values 要求：在 B 以下记录的每个取值都是塔在那里的取值。Entries 要求：B 以下的每个实参处都记录了正準条目。Domain 要求：B 以外的东西完全没有被记录。

Values : S → V ℓ → Type (ℓ-suc ℓ)
Values h B = (c z : S) → ⟨ c .fst ∈ B ⟩
           → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩ → z .fst ≡ Lset (c .fst)

正确性是关于被记录条目的陈述。若「B 以下的实参 c 与某个 z 组成的对」是表的一条目，则 z 就是塔在 c 处的取值。成员关系 c .fst ∈ B 是层级中的成员关系，因为 B 是层级的集合；表 h 是载体元素，h .fst 是它呈现的那个集合。

Entries : S → V ℓ → Type (ℓ-suc ℓ)
Entries h B = (c : S) → ⟨ c .fst ∈ B ⟩ → ⟨ pr (c .fst) (Lset (c .fst)) ∈ h .fst ⟩

完备性是关于覆盖范围的镜像要求：在 B 以下的每个实参 c 处，典范条目，即 c 与塔值 Lset c 组成的对，都被记录。两个条件合起来，正确且完备的表在 B 以下记录的恰是那些典范条目，没有任何走样。

Domain : S → V ℓ → Type (ℓ-suc ℓ)
Domain h B = (c z : S) → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩ → ⟨ c .fst ∈ B ⟩

这些条件分开保留，因为各应用所需的子集不同。对逼近的归纳只用前两条，且用不了第三条：逼近的诸条目落在它自己的定义域以下，而不落在归纳所处的那个实参以下。内部层级将三条全有，因为它就是按「恰好是那些对的集合」构造的。还要注意 B 是什么：它是底层界集，层级中的一个集合。在语义应用中，它经由环境的某个槽位到来，是载体元素的底层部分，而该载体元素另外携带可构造性；B 的序数性是一条独立的假设，不由这些条件供给。此处制表的层是层级的集合、由序数索引；宿主的宇宙层级从不进入制表。

与外部层级对照的步骤

本节把上一章的步进条件与塔连接起来。实参 b 处的步进，沿 b 以下的诸实参 c 与在其处记录的诸取值 w，收集 w 的可定义幂集的元素。塔在 b 处收集的元素与之相同，只是把被记录的 w 换成 Lset c。三个私有事实为对照做准备：ok 解除旁条件 PowOK，below 把塔的一次分解变成步进见证，above 把步进见证变成塔的元素。

module _ {n : ℕ} (v b f : Fin n) (γ : Vec S n) where

private

  ok : IsOrd ((lookup b γ) .fst) → Values (lookup f γ) ((lookup b γ) .fst)
     → PowOK b f γ

  ok ob vals c z rec = subst (λ u → ⟨ isL (𝒟ₒ u) ⟩)
    (sym (vals c z (rec .fst) (rec .snd)))
    (isL-𝒟ₒ (c .fst) (mem-ord {A = (lookup b γ) .fst} ob (c .fst) (rec .fst)))

  below : IsOrd ((lookup b γ) .fst) → Entries (lookup f γ) ((lookup b γ) .fst)
        → (z : S)
        → Σ[ δ ∶ V ℓ ] (⟨ δ ∈ (lookup b γ) .fst ⟩ × ⟨ z .fst ∈ 𝒟ₒ (Lset δ) ⟩)
        → StepOf b f γ z

  below ob ents z (δ , (δ∈ , hz)) =
    d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz))

    where
    oδ : IsOrd δ
    oδ = mem-ord {A = (lookup b γ) .fst} ob δ δ∈
    d : S
    d = δ , isL-trans {x = (lookup b γ) .fst} {y = δ} δ∈ (lookup b γ .snd)

  above : Values (lookup f γ) ((lookup b γ) .fst) → (z : S) → StepOf b f γ z
        → ⟨ z .fst ∈ Lset ((lookup b γ) .fst) ⟩

  above vals z (c , (w , (rec , hz))) =
    Lset-in ((lookup b γ) .fst) (c .fst) (z .fst) (rec .fst)
      (subst (λ u → ⟨ z .fst ∈ 𝒟ₒ u ⟩) (vals c w (rec .fst) (rec .snd)) hz)

step-Lset : ⟨ γ ⊨ StepAt v b f ⟩ → IsOrd ((lookup b γ) .fst)
          → Values (lookup f γ) ((lookup b γ) .fst)
          → Entries (lookup f γ) ((lookup b γ) .fst)
          → (lookup v γ) .fst ≡ Lset ((lookup b γ) .fst)

step-Lset h ob vals ents =
  extensionalV {a = (lookup v γ) .fst} {b = Lset ((lookup b γ) .fst)} pt
  where

  fwd : (x : V ℓ) → ⟨ x ∈ (lookup v γ) .fst ⟩
      → ⟨ x ∈ Lset ((lookup b γ) .fst) ⟩
  fwd x hx = rec₁ ((x ∈ Lset ((lookup b γ) .fst)) .snd) (above vals z)
    (StepAt-out v b f γ h (ok ob vals) z hx)

    where
    z : S
    z = x , isL-trans {x = (lookup v γ) .fst} {y = x} hx (lookup v γ .snd)

  bwd : (x : V ℓ) → ⟨ x ∈ Lset ((lookup b γ) .fst) ⟩
      → ⟨ x ∈ (lookup v γ) .fst ⟩
  bwd x hx = rec₁ ((x ∈ (lookup v γ) .fst) .snd) put
    (Lset-out ((lookup b γ) .fst) x hx)

    where
    z : S
    z = x , isL-trans {x = Lset ((lookup b γ) .fst)} {y = x} hx
              (LsetS ((lookup b γ) .fst) ob .snd)

    put : Σ[ δ ∶ V ℓ ] (⟨ δ ∈ (lookup b γ) .fst ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
        → ⟨ x ∈ (lookup v γ) .fst ⟩
    put s = StepAt-back v b f γ h (ok ob vals) z (below ob ents z s)

  pt : (x : V ℓ) → (x ∈ (lookup v γ) .fst) ≡ (x ∈ Lset ((lookup b γ) .fst))
  pt x = ⇔toPath (fwd x) (bwd x)

step-table : IsOrd ((lookup b γ) .fst)
           → Values (lookup f γ) ((lookup b γ) .fst)
           → Entries (lookup f γ) ((lookup b γ) .fst)
           → (lookup v γ) .fst ≡ Lset ((lookup b γ) .fst)
           → ⟨ γ ⊨ StepAt v b f ⟩

step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back
  where

  into : (z : S) → ⟨ z .fst ∈ (lookup v γ) .fst ⟩ → ∥ StepOf b f γ z ∥₁
  into z hz = map₁ (below ob ents z)
    (Lset-out ((lookup b γ) .fst) (z .fst)
      (subst (λ u → ⟨ z .fst ∈ u ⟩) q hz))

  back : (z : S) → StepOf b f γ z → ⟨ z .fst ∈ (lookup v γ) .fst ⟩
  back z s = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym q) (above vals z s)

反过来，见证经 above 把 z 放进塔里，而运输沿 q 反向进行。

逼近所记录的每个值

一次归纳，在实参上，在元语言中，逼近与它的定义域保持固定。动机说：逼近在这个实参处所记录的任何取值，都是元层面的塔在那里的取值。动机对一切被记录的取值作量化，而这正是单值性在任何地方都不作为假设的原因。在同一个实参处记录的两个取值都被钉在同一个塔值上，故两者相等；被记录取值的唯一性由归纳读出，而非假设。

归纳的步进就是 step-Lset 施于被记录的那个取值。实参以下的正确性就是归纳假设，一字不差。实参以下的完备性则是逼近的取值子句被花掉之处：比这个实参更低的实参落在逼近的定义域以下，因为定义域是序数、而序数传递；逼近于是在那里有取值；而归纳假设把它与塔的取值认同。那个取值只是「仅仅」被拿出来的，而这已经够了，因为要对它证的是一条成员关系。

module _ {n : ℕ} (f a : Fin n) (γ : Vec S n) where

private
  Value : V ℓ → Type (ℓ-suc ℓ)
  Value u = ⟨ isL u ⟩ → (z : S)
          → ⟨ pr u (z .fst) ∈ (lookup f γ) .fst ⟩ → z .fst ≡ Lset u

approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd ((lookup a γ) .fst)
           → (x z : S) → ⟨ pr (x .fst) (z .fst) ∈ (lookup f γ) .fst ⟩
           → z .fst ≡ Lset (x .fst)
approx-val h oa x = ∈-induction {P = Value} go (x .fst) (x .snd)

  where
  go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
  go u IH hu z p = step-Lset zero (suc zero) (sh2 f) (z ∷ d ∷ γ)
    (ApproxAt-step f a γ h d z p) ou vals ents

    where
    d : S
    d = u , hu
    u∈a : ⟨ u ∈ (lookup a γ) .fst ⟩
    u∈a = ApproxAt-dom f a γ h d z p

    ou : IsOrd u
    ou = mem-ord {A = (lookup a γ) .fst} oa u u∈a

    vals : Values (lookup f γ) u
    vals c y c∈ q = IH (c .fst) c∈ (c .snd) y q

    ents : Entries (lookup f γ) u
    ents c c∈ = rec₁
      ((pr (c .fst) (Lset (c .fst)) ∈ (lookup f γ) .fst) .snd) named
      (ApproxAt-value f a γ h c (oa .fst {x = u} {y = c .fst} c∈ u∈a))

      where
      named : Σ[ y ∶ S ] ⟨ pr (c .fst) (y .fst) ∈ (lookup f γ) .fst ⟩
            → ⟨ pr (c .fst) (Lset (c .fst)) ∈ (lookup f γ) .fst ⟩
      named (y , q) = subst (λ t → ⟨ pr (c .fst) t ∈ (lookup f γ) .fst ⟩)
        (IH (c .fst) c∈ (c .snd) y q) q

那个仅仅给出的被记录取值，由归纳假设同认于塔；运输之后，被记录的恰是典范条目，这正是完备性所要求的。

图只对正确值成立

塔之图说：槽位处的取值就是塔在实参处的取值，而它经由一个逼近这样说：仅存在一个逼近，其在该实参处的步进正是那个取值。展开之后，所需的材料全部就位。实参以下的正确性来自刚完成的归纳；实参以下的完备性来自逼近的取值子句，经同一场归纳运输；最后再应用一次 step-Lset，就把被记录取值同认于塔。因此图确定它的取值：凡在某个序数处满足它的对象，都是元层面的塔在该处的取值。

这条读式以变元槽形式陈述，这并非装饰。它的各处实例化住在不同的具体环境中；若在某一处陈述，就得通过一个内部装着整条塔描述的满足关系，把它运到另一处。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

Lset-only : ⟨ γ ⊨ LsetGraphAt w b ⟩ → IsOrd ((lookup b γ) .fst)
          → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)

Lset-only h ob = rec₁
  (setIsSet ((lookup w γ) .fst) (Lset ((lookup b γ) .fst))) read
  (LsetGraph-out w b γ h)
  where

  read : GraphOf w b γ → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)
  read (f , (ha , hs)) =
    step-Lset (suc w) (suc b) zero (f ∷ γ) hs ob vals ents

    where
    vals : Values f ((lookup b γ) .fst)
    vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p

    ents : Entries f ((lookup b γ) .fst)
    ents c c∈ = rec₁ ((pr (c .fst) (Lset (c .fst)) ∈ f .fst) .snd) named
      (ApproxAt-value zero (suc b) (f ∷ γ) ha c c∈)

      where
      named : Σ[ y ∶ S ] ⟨ pr (c .fst) (y .fst) ∈ f .fst ⟩
            → ⟨ pr (c .fst) (Lset (c .fst)) ∈ f .fst ⟩
      named (y , q) = subst (λ t → ⟨ pr (c .fst) t ∈ f .fst ⟩)
        (approx-val zero (suc b) (f ∷ γ) ha ob c y q) q

那个仅仅给出的被记录取值，由同一场归纳再次同认于塔；运输之后，被记录的恰是典范条目。

表就是逼近

反方向需要一个见证，而一张正确且完备的表就是。graph-table 把这样一张表变成对塔之图的满足，办法是填上上一章的诸子句，此外什么也不做。

逼近的定义域合取项是「实参在定义域中」的两种说法之间的等价，Domain 与 Entries 分别证明其两个方向：在 c 处记录的条目把 c 放到界以下；而只要 c 低于界，c 处的正準条目就被记录。某条被记录的对 (c, y) 处的步进合取项，是施于 c 的 step-table；序数的传递性把表的正确性与完备性限制到 c 以下的实参，那正是步进引理在该处所消费的。图所问的取值是整个实参处的步进，这同样是 step-table，取「被记录取值同认于塔」的等式为输入。

陈述取表 h、实参的序数性、表在实参上的三个条件，以及「被记录取值就是塔」的断言。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

graph-table : (h : S) → IsOrd ((lookup b γ) .fst)
            → Values h ((lookup b γ) .fst) → Entries h ((lookup b γ) .fst)
            → Domain h ((lookup b γ) .fst)
            → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)

            → ⟨ γ ⊨ LsetGraphAt w b ⟩
graph-table h ob vals ents dom q = LsetGraph-in w b γ h approx
  (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents q)
  where

  onDom : (c : S)
        → (⟨ ∃[ y ∶ S ] pr (c .fst) (y .fst) ∈ h .fst ⟩
           → ⟨ c .fst ∈ (lookup b γ) .fst ⟩)
        × (⟨ c .fst ∈ (lookup b γ) .fst ⟩
           → ⟨ ∃[ y ∶ S ] pr (c .fst) (y .fst) ∈ h .fst ⟩)

  onDom c = (λ hy → rec₁ ((c .fst ∈ (lookup b γ) .fst) .snd) named hy)
          , (λ c∈ → ∣ LsetS (c .fst) (mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈)
                   , ents c c∈ ∣₁)

    where
    named : Σ[ y ∶ S ] ⟨ pr (c .fst) (y .fst) ∈ h .fst ⟩
          → ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    named (y , p) = dom c y p

  onStep : (c y : S) → ⟨ pr (c .fst) (y .fst) ∈ h .fst ⟩
         → ⟨ (y ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
  onStep c y p = step-table zero (suc zero) (suc (suc zero)) (y ∷ c ∷ h ∷ γ)
    oc vals' ents' (vals c y c∈ p)

    where
    c∈ : ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    c∈ = dom c y p
    oc : IsOrd (c .fst)
    oc = mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈

    vals' : Values h (c .fst)
    vals' e t _ r = vals e t (dom e t r) r
    ents' : Entries h (c .fst)
    ents' e e∈ = ents e (ob .fst {x = c .fst} {y = e .fst} e∈ c∈)

  approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
  approx = ApproxAt-in zero (suc b) (h ∷ γ)
    (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep

把两个合取项装配起来，表本身就是逼近：其定义域子句是刚才证明的等价，其步进子句是之前的那个。所谓「正确且完备的表包含实参以下层级的记录」，其含义就在于此。

有序对图

表必须被构造出来，而 L 内部可用的建造者只有替换，替换需要一个图。替换在函数性图的描述之后收集这张表：表的一条目是实参 c 与取值 z 的有序对；当 z 满足塔在 c 处的图时，图对该条目成立，而塔所遍及的载体被钉在某个常元上。一个存在量词绑定塔的取值，对读式把条目与「实参和被绑定取值」组成的对等同起来，塔之图则说明被绑定的取值是正确的。

它的两种读法把那个句子取作参数，并把该句子自己的等式取作假设，本章的调用处是 refl。该框架对句子保持通用：无论传入什么公式，读法都在「它拼出有序对图」的假设下谈论它。等式随句子同行，因此读法的施用无需更多论证。

内部层级

Recorded 为内部层级在 α 处要收集的类命名：底层集合低于 α 的实参 c，连同塔在 c 处的取值组成的对，此外别无他物。IsHier 说模型的某个集合逐元素地实现这个类：对每个载体元素 z，属于该集合恰当 z 呈现为这样的对。这条陈述的两个方向都有使用。HierOf 把实现集合连同其规格收为一对；构造所建造的是这个形式，两条读式所消费的也是这个形式。

两条读式都针对一个由其规格抵达的变元实现集合，这样即将到来的构造就可以把它们应用于自己正在建造的集合。向外读取时，对某个元素应用层级配对的单射性：实现集合的一条目指名低于 B 的实参与塔在该处的取值。向内写入时，把正準对呈现为模型的元素，这由模型自身的配对给出；它还需要实参的序数性，否则根本无法指称塔在该处的取值。

然后是构造，在序数上作一次沿元素的归纳。在 α 处，成对的那个图在以下的每个实参上都是函数性的：归纳假设给出直到那个实参为止的层级，graph-table 把它变成对塔之图的满足，而 Lset-only 说别的东西都不满足它。替换把这些对收集成模型的一个集合。每个实参的序数性取自 mem-ord；函数性要求由 mereFunct 满足，因为某个实参处的取值是一个构造。

Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Recorded B z = ∃[ c ∶ S ] (c .fst ∈ B)
  ⊓ ((z ≡ pr (c .fst) (Lset (c .fst))) , setIsSet z (pr (c .fst) (Lset (c .fst))))

Recorded B z 是一个命题，它说：存在某个载体元素 c，其底层集合低于 B，使得 z 的底层集合是 c .fst 与塔在 c 处取值的有序对。两个 h-集合的相等本身就是命题，因此这是一个命题上的析取聚合。

IsHier : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
IsHier B h = (z : S) → (z .fst ∈ h .fst) ≡ Recorded B (z .fst)

IsHier B h 说 h 所呈现的集合逐元素地实现被记录的类：在每个 z 处，属于该集合与被记录是同一命题。两个方向都不丢弃，因为各有其用：只有成员关系而无被记录，会放进陌生者；只有被记录而无成员关系，会漏掉应有的对。

HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
HierOf B = Σ[ h ∶ S ] IsHier B h

HierOf B 把实现集合连同其规格收集为一对。这对正是归纳要在每个序数处构造的东西；它的两个分量分别回答对任何构造都要问的两个问题：它是什么，以及它为何合格。

module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where

hier-out : (c z : S) → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩
         → ⟨ c .fst ∈ B ⟩ × (z .fst ≡ Lset (c .fst))

hier-out c z p = rec₁
  (isProp× ((c .fst ∈ B) .snd) (setIsSet (z .fst) (Lset (c .fst)))) read
  (subst ⟨_⟩ (sp k) p)
  where

  k : S
  k = pr (c .fst) (z .fst)
    , isL-trans {x = h .fst} {y = pr (c .fst) (z .fst)} p (h .snd)

  read : Σ[ d ∶ S ] (⟨ d .fst ∈ B ⟩
           × (pr (c .fst) (z .fst) ≡ pr (d .fst) (Lset (d .fst))))
       → ⟨ c .fst ∈ B ⟩ × (z .fst ≡ Lset (c .fst))
  read (d , (d∈ , eq)) =
      subst (λ t → ⟨ t ∈ B ⟩) (sym (pr-inj eq .fst)) d∈

    , (pr-inj eq .snd ∙ cong Lset (sym (pr-inj eq .fst)))

hier-in : (c : S) → ⟨ c .fst ∈ B ⟩ → ⟨ pr (c .fst) (Lset (c .fst)) ∈ h .fst ⟩
hier-in c c∈ = subst (λ t → ⟨ t ∈ h .fst ⟩) (prʟ-fst c (LsetS (c .fst) oc))
  (subst ⟨_⟩ (sym (sp k)) ∣ c , (c∈ , prʟ-fst c (LsetS (c .fst) oc)) ∣₁)

  where
  oc : IsOrd (c .fst)
  oc = mem-ord {A = B} oB (c .fst) c∈
  k : S
  k = prʟ c (LsetS (c .fst) oc)

c 的序数性来自 B 的序数性；有了它，塔在 c 处的取值才能呈现为 L 的元素，而这正是模型的配对所需要的第二分量。

opaque
  hierAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → HierOf α
  hierAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → HierOf α}
    (build (PairGraphAt zero (suc zero)) refl)
    where

归纳的步进函数把成对的那个图保持为随身携带自己等式的变元句子，而不写出它将被实例化成的闭句子。等式随句子同行，因此下面的每条读式都在调用处以 refl 施用。

    build : (φ : Formula S ) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ)
          → ⟨ isL α ⟩ → IsOrd α → HierOf α

步进接收句子及其等式、序数 α、它的两张证书，以及归纳假设：α 的每个元素处的层级均已建成。它须返回 α 处的层级及其规格。

    build φ qφ α IH hα oα = r .fst .fst , spec
      where
      A : S
      A = α , hα

α 处的层级是实现者的第一分量，在替换产出之后一次提取；A 是呈现为载体元素的 α，正是替换消费定义域时所用的形式。

      value : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      value c c∈ = LsetS (c .fst) (mem-ord {A = α} oα (c .fst) c∈)

      entry : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      entry c c∈ = prʟ c (value c c∈)

在 α 以下，两个辅助构造为数据命名。实参 c 处的取值是 c 处的层，由层呈现而成为 L 的元素，c 的序数性取自 α 的序数性。c 处的条目是模型自身的「c 与其取值」的有序对，正是被记录类所要求的形式。

      below : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) (k : S)
            → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      below c c∈ k = graph-table zero (suc (suc zero)) (value c c∈ ∷ k ∷ c ∷ [])
        (hc .fst) oc

塔之图在为 α 的元素 c 所记录的取值处成立。归纳假设正是在此被花掉：它交出 c 处的层级，那是实参 c 上一张正确且完备的表，恰是 graph-table 所要的。环境中载着取值、给图自身量词留的新槽，以及实参。

        (λ d z _ p → hier-out (c .fst) oc (hc .fst) (hc .snd) d z p .snd)
        (hier-in (c .fst) oc (hc .fst) (hc .snd))
        (λ d z p → hier-out (c .fst) oc (hc .fst) (hc .snd) d z p .fst)
        refl

表的三个条件从 c 处层级的规格读出：正确性说每个被记录取值都是塔在那里；完备性说典范条目被记录；定义域条件说此外无他。最后一个参数 refl 是有序对图自己的等式。

        where
        oc : IsOrd (c .fst)
        oc = mem-ord {A = α} oα (c .fst) c∈
        hc : HierOf (c .fst)
        hc = IH (c .fst) c∈ (c .snd) oc

c 的序数性来自 α 的序数性；有了它，归纳假设交付 c 处的层级；可构造集合与规格一并交付。

（holds)每条正準条目都满足有序对图：c 上的纤维被给出，其中包括被绑定的塔值、把条目与模型之对等同的等式，以及塔之图在取值与实参处的满足。见证是纤维的一个元素，即图陈述所断言「仅仅存在」的那个类型的元素。

      holds : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩)
            → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩
      holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ
        (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))

（only)在 c 处满足图的其他任何居留者都等于正準条目。图展开为塔值 z 连同在 (z, c) 处成立的塔之图；塔之图确定其取值，配对的单射性等同两条目，而该等式是这些路径的复合。

      only : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) (k : S)
           → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈
      only c c∈ k h = rec₁ (isSetS k (entry c c∈)) read
        (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)

对的见证拆成塔值 z 与把 k 同认于「c 与 z 之对」的等式 q。一旦底层集合相等，载体元素就相等，Σ≡Prop 把目标化归于此。

        where
        read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
        read (z , (q , hg)) = Σ≡Prop (λ t → (isL t) .snd)
          ( q

(z, c) 处的塔之图确定塔值：由 Lset-only 在「加入取值、典范条目与实参」的扩展环境中施用，得 z 就是塔在 c 处的取值；c 的序数性取自 α 的序数性。

          ∙ cong (pr (c .fst))
              (Lset-only zero (suc (suc zero)) (z ∷ k ∷ c ∷ []) hg
                (mem-ord {A = α} oα (c .fst) c∈))
          ∙ sym (prʟ-fst c (value c c∈)) )

三条路径复合起来，k 就是「c 与塔在 c 处取值」之对，即按其定义读式读出的典范条目。

（fc)c 处的函数性正是替换所要的可缩纤维：正準条目在图中有一席，而每个居留者都等于它。mereFunct 把以「仅仅存在」形式呈现的两半，装配成恰为该可缩纤维的居留。

      fc : (c : S) → ⟨ c ∈ˢ A ⟩
         → isContr (Σ[ k ∶ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩)
      fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁

替换随即收集诸条目：遍及 α 中的实参，每个实参与其唯一确定的取值组成的对构成模型的一个集合，并连同「它恰实现那个对之类」的断言一起呈现。α 处的内部层级作为 L 的集合而存在的时刻，就是此刻。

      r : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ)))
      r = hasReplacementL A φ fc

      spec : IsHier α (r .fst .fst)
      spec z = ⇔toPath toRec fromRec
        where

余下的是验证：收集所得的集合确实实现被记录的类。规格逐元素比较「属于收集集合」与「是被记录的对」；比较的两个方向分别证明，再合并为逐点等价。

        toRec : ⟨ z .fst ∈ (r .fst .fst) .fst ⟩ → ⟨ Recorded α (z .fst) ⟩
        toRec hz = rec₁ squash₁ conv (subst ⟨_⟩ (r .fst .snd z) hz)
          where

把收集集合的成员关系向外读：替换的规格把它变成 α 的一个元素 c，其取值在 c 处满足有序对图。消去是合法的，因为被记录的类是命题。

          conv : Σ[ c ∶ S ] (⟨ c .fst ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
               → ⟨ Recorded α (z .fst) ⟩
          conv (c , (c∈ , hp)) = ∣ c , (c∈ , cong (λ p → p .fst) (only c c∈ z hp)
                                            ∙ prʟ-fst c (value c c∈)) ∣₁

对见证而言，唯一性说在 c 处记录的取值等于典范条目，而典范条目等于模型的「c 与塔在 c 处取值」之对；底层集合随之而来，这正是「被记录」所要求的。

        fromRec : ⟨ Recorded α (z .fst) ⟩ → ⟨ z .fst ∈ (r .fst .fst) .fst ⟩
        fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (map₁ conv hz)
          where

向内读：一条被记录的对给出低于 α 的实参连同塔在该处的取值；有序对图在该实参的典范条目处成立，而收集集合含有这条条目。

          conv : Σ[ c ∶ S ] (⟨ c .fst ∈ α ⟩
                   × (z .fst ≡ pr (c .fst) (Lset (c .fst))))
               → Σ[ c ∶ S ] (⟨ c .fst ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)

见证从被记录的呈现转换成图的呈现：实参保持不变，而「底层集合等于典范对」的等式变成有序对图在该处的满足。

          conv (c , (c∈ , eq)) = c , (c∈
            , subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩) (sym zeq) (holds c c∈))
            where
            zeq : z ≡ entry c c∈
            zeq = Σ≡Prop (λ t → (isL t) .snd)

该等式说 z 呈现与 c 的典范条目相同的集合；因此两个对元素相等，把 holds 沿这条路径运输，便得有序对图在 z 与 c 处的满足。

              (eq ∙ sym (prʟ-fst c (value c c∈)))

hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
hierL α hα oα = hierAt α hα oα .fst

某个序数处的内部层级，就是归纳所得的实现集合，呈现为 L 的元素。它对每个可构造序数都存在；也就是说：模型如今为它的每个序数准备了一个集合，其元素恰是「低于该序数的序数与塔在该处取值」组成的有序对。

hierL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α)
           → IsHier α (hierL α hα oα)
hierL-spec α hα oα = hierAt α hα oα .snd

规格随构造同行：归纳交付的实现集合，在其序数处于两个方向上满足 IsHier。日后对内部层级的一切使用，都对照这份说明来检验。

外部层级满足该图

内部层级是用 graph-table 与 Lset-only 建造的：在每个序数处，归纳假设供给以下的表，两条引理把它变成成立的图与唯一的取值。最后一条陈述此刻反向而行。规格 hierL-spec 交出实参上的表条件，Lset-defines 把它们喂给 graph-table：塔之图在被记录取值处成立，与之并置的 Lset-only 说别无其他满足者。于是内部之图与元层面的塔在每个可构造序数处、在两个方向上一致。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

Lset-defines : IsOrd ((lookup b γ) .fst)
             → (lookup w γ) .fst ≡ Lset ((lookup b γ) .fst)
             → ⟨ γ ⊨ LsetGraphAt w b ⟩

Lset-defines ob q = graph-table w b γ H ob
  (λ c z _ p → hier-out ((lookup b γ) .fst) ob H sp c z p .snd)
  (hier-in ((lookup b γ) .fst) ob H sp)
  (λ c z p → hier-out ((lookup b γ) .fst) ob H sp c z p .fst)
  q

  where
  H : S
  H = hierL ((lookup b γ) .fst) (lookup b γ .snd) ob
  sp : IsHier ((lookup b γ) .fst) H
  sp = hierL-spec ((lookup b γ) .fst) (lookup b γ .snd) ob

实参处的内部层级之所以存在，是因为实参是可构造序数；其规格恰是归纳所证明的成员关系等价。两件事合起来说：塔在每一个层处都被记录在模型内部，且此外无他。

小结

approx-val 通过对实参作一次沿成员关系归纳，证明逼近记录的每个取值都等于元层面的塔在相应实参处的取值；这里不需要任何单值性假设。在同一个实参处记录的两个取值相等，可由它直接读出。Lset-only 与 Lset-defines 给出图与塔之间的两个方向，而后者用于构造 hierL。hierL 是某个序数处的内部层级，是 L 的一个元素；其元素恰是「低于该序数的序数与塔在该处取值」组成的有序对。其规格是归纳所证明的成员关系等价。

此处制表的层由序数索引，序数是层级的集合；宿主的宇宙层级是类型的大小指标，从不为塔索引。