L 中无穷基数的平方律

对 L 中的无穷基数 κ，其成员的有序对所成之集可经 L 内部的编码单射注入 κ 自身。本章构造这个单射。路线经由对上的 Gödel 序：把这条序写成第一阶对象语言的公式，在序数 κ 处读作外部的 Gödel 序，再塌缩到序型，由计数引理与 κ 比较。本章在固定的宇宙层级 ℓ 上工作，使用高一层的排中律，即下文所有序数比较所依赖的唯一经典假设。

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

这一构造并非处处构造性的，其原因在数学而不在形式化。要为序数的有序对排序，就必须对两个序数 a 与 b 判定 a 是否属于 b；本章的每个经典判定都是这同一个问题的实例。模块因此以显式数据接收层级 ℓ-suc ℓ 上的排中律，那正是被判定隶属命题所在的层级。

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

模块参数一次性固定这个实例，本章的每个经典步骤消耗的恰是它。

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

将被内在化的序用一阶对象语言写出：由隶属与相等两种原子经联结词、否定和无界存在量词生成的公式，在外围层级上解释。层级自身还有两条事实伴随其侧，二者都用于收束论证：隶属是良基的，故序数允许沿 ∈ 作归纳；并且没有集合属于自身，故不可能的比较可被直接反驳。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )

读取编码对的坐标并以其计数，依赖三个事实。序数的后继运算是单射的，故相等的后继有相同的前驱。序数的每个成员都由其小呈现的一个索引指名，该命名单射，且可构造集的成员自身可构造。有序对 pr 在两个坐标上都是单射的，故编码对确定其两个分量。

open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj )
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}

在可构造一侧，内层结构 𝒮ʟ 把层级限制到可构造集这个传递类。全章使用的序数事实都是封闭性事实：序数的成员是序数，序数的后继是序数，ω 的成员是序数，且任意两个序数经三歧性可比。与它们并列的，是本章所要内在化的、对上的外部 Gödel 序。

  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord; #∈ω; ω-mem-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
import L.Ordinal.SquareLaw {ℓ} lem as SQ

两个序数的比较被打包成三歧数据而非真值，因为下文的证明必须检查出现了哪种情形：严格小于、相等、或严格大于。空集与 ω 都可作为 L 的元素使用，内部的后继数码则带有对其底层集合的等同，使数码槽位能读作外围自然数。

open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( lt; eq; gt ) renaming ( Tri to TriW )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )

在 L 内部，有序对与图条件由具有内外两种读法的一阶公式表达。配对充分性把编码对等同于其两个分量组成的外围有序对；图的读法则表达单值性、定义域、单射性及取值属于陪域。合在一起，这些条件刻画内部编码单射。

open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt )
open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate )
open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract; module Small )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL; _↪_ )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )

构造由三个数学转换推动。首先，以包含于原序数且在内部与之等势的内部基数代表替代该序数；其次，可定义单射函数给出编码单射；最后，把良基且传递的关系塌缩为序数序型，并由三歧性证明塌缩映射单射。

open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
open import L.InjectionComposition {ℓ} lem
  using ( appC; appC-adequate; ω-limit; finite-excl-ω )

两个编码对的比较携带六个相互依赖的见证：四个坐标及其两个最大值。积保存同时成立的等式与次序条件，不交和保存不同的比较情形。由于证明分量都是命题，它们不会在所得序数据中引入额外选择。

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels
  using ( isProp×; isSetΣSndProp )

编码对的坐标是 κ 底层集合的成员，须借助该集合的小呈现读取。与呈现并列的还有外围隶属、带空虚性证明的空集，以及 ω 与后继运算，坐标的比较与计数正是在这些概念中进行。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )

三种逻辑形式反复出现。良基性表述为每个元素的可及性数据，正是它使塌缩能沿序下降。反驳居住在空类型中。而只断言见证存在的条件在截断之下陈述，这已经足够，因为消费这些条件的目标本身就是命题或截断。

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Induction.WellFounded as WF
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

两个载体被命名并保持区分。外围载体承载层级自身的隶属；内层载体 S 由可构造集组成，每个元素是一个外围集合连同其可构造性证明，其隶属就是在外围集合上读取的外围隶属。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropStructure 𝒮ᵥ using ()
module SL = hPropStructure 𝒮ʟ using (S; _∈ˢ_)
open SL using ( S )

绝对性实例固定在可构造集这个传递类上：有界公式在 L 内外的含义相同，环境经投影读取，内层满足关系被改名为朴素的 _⊨_。

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

内层载体是 h-集合，这使其元素的相等易于处理。其元素是第二分量为命题的对，所以两个元素恰在其底层集合相等时相等；对路径引理则由各分量的等式构造两个对的等式。

isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
opaque
  pair≡ : {A : Type ℓ} {B : Type ℓ} {a a' : A} {b b' : B}
        → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')

对路径正是这一构造：由 a ≡ a' 与 b ≡ b' 逐点得到路径 (a , b) ≡ (a' , b')。序数是可构造的，理由直接：序数 x 属于它自己的后继，而那个层是 L 的集合，属于层即是可构造。该陈述是命题，故其证明在事实之外不携带任何信息。

  pair≡ e1 e2 = λ i → e1 i , e2 i
opaque
  isL-ord : (x : V ℓ) → IsOrd x → ⟨ isL x ⟩
  isL-ord x ox = Lset→isL (sucV x) (suc-ord ox) x (ord∈Lset-suc x ox)

因此，序数 x 可连同其可构造性证明视为可构造载体的元素 ordL x ox。再对「两个坐标都属于 K」这一关系施行可定义分离，便得到由这些有序对组成的可构造集合 prodL K。

ordL : (x : V ℓ) → IsOrd x → S
ordL x ox = x , isL-ord x ox
open import L.InjectionComposition {ℓ} lem public using ( module Relation )
private
  module Product (K : S) = Relation K K

乘积的描述条件说：两个坐标都是 K 的成员。其在宿主一侧的读法，是两个投影在 K 的底层集合中的外围隶属，且该读法的两个方向都已给出。

    ((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K))
    (λ x y → (fst x ∈ˢ fst K) ⊓ (fst y ∈ˢ fst K))
    (λ x y e h → h) (λ x y e h → h)

于是 prodL K 就是由 K 的两个成员组成的有序对之集，在 L 内部从约束它们的层中分离而来。

prodL : S → S
prodL = Product.rel

乘积中的隶属由一条截断的存在陈述刻画：存在 K 的两个成员 a 与 b，使该成员等于它们的有序对。截断如实记录条件所断言的内容，即见证存在，而在此处没有任何东西能区分一对见证与另一对；只有先证明见证唯一，才谈得上消去截断。

InProd : S → V ℓ → Type (ℓ-suc ℓ)
InProd K e = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ]
               (⟨ fst a ∈ˢ fst K ⟩ × ⟨ fst b ∈ˢ fst K ⟩
                × (e ≡ pr (fst a) (fst b))) ∥₁

向内：K 的任意两个成员的有序对属于 prodL K；这正是那条被分离关系自身的引入规则。

prodL-in : (K a b : S) → ⟨ fst a ∈ˢ fst K ⟩ → ⟨ fst b ∈ˢ fst K ⟩
         → ⟨ pr (fst a) (fst b) ∈ˢ fst (prodL K) ⟩
prodL-in K a b ma mb = Product.into K a b ma mb (ma , mb)

向外：prodL K 的成员以截断的形式来自 K 的两个成员与那条对等式。对照 K 的小呈现，更强而不截断的陈述也可用：乘积的每个成员都是 K 的两个索引所指名元素组成的有序对。

prodL-out : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩ → InProd K (fst e)
prodL-out K e h = PT.map (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h)
prodL-fst : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩
          → Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
              (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))

证明把截断的见证转换为 K 的索引的纤维，并沿纤维自身的等同，即「K 的每个成员恰是其索引所指名的集合」，修复那条对等式。

prodL-fst K e h = PT.rec isPropFib
  (λ { (a , b , ma , mb , q) →
     fiber (fst K) ma .fst , fiber (fst K) mb .fst
     , q ∙ cong₂ pr (sym (fiber (fst K) ma .snd)) (sym (fiber (fst K) mb .snd)) })
  (prodL-out K e h)

第二分量是唯一的：有序对的单射性提取出所指名集合的等式，而 K 的索引的单射性把它变成索引的等式。

  where
  inner : (a : ⟪ fst K ⟫)
        → isProp (Σ[ b ∈ ⟪ fst K ⟫ ] (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  inner a (b , q) (b' , q') = Σ≡Prop (λ _ → setIsSet _ _)
    (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .snd))

第一分量基于同样的理由唯一，于是整条纤维陈述是一个命题：不截断的读法不依赖任何选取。

  isPropFib : isProp (Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
                        (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner
    (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .fst))

作为公式的 Gödel 序

乘积到手之后，序登场：当 a 与 b 为序数时，MaxIs 说 m 是它们的最大值。

MaxIs : S → S → S → Type (ℓ-suc ℓ)

定义给出两个选项：要么 a 属于 b 且 m 是 b，要么「a 属于 b」被反驳且 m 是 a。被截断的只是这个析取，因为定义只断言两个选项之一成立而不判定是哪一个；在序数上，排中律将选出分支，被选出的 m 便是 a 与 b 的最大值。

MaxIs m a b =
  ∥ (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
  ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a)) ∥₁

两个对的 Gödel 比较同样是截断之下的数据：要么第一对的最大值 m 属于第二对的最大值 n，要么两个最大值相等，此时按字典序比较，先比第一坐标，再比第二坐标。

OrdIs : S → S → S → S → S → S → Type (ℓ-suc ℓ)
OrdIs m n a b c d =
  ∥ ⟨ fst m ∈ˢ fst n ⟩
  ⊎ ((fst m ≡ fst n)
     × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁) ∥₁

最大值可写成一条有界公式：当 a 属于 b 时 m 等于 b，当 a 属于 b 被反驳时等于 a；否定词使第二个选项成为受守卫的分支。当 a 与 b 为序数时，这条公式说的恰是 m 是它们的最大值。

maxAt : ∀ {k} → Fin k → Fin k → Fin k → Formula S k
maxAt m a b = ((var a ∈̇ var b) ∧̇ (var m ≐ var b))
            ∨̇ ((¬̇ (var a ∈̇ var b)) ∧̇ (var m ≐ var a))

Gödel 比较也可同样写出，且其优先级是显式的：先比较两个最大值；最大值相等时比较第一坐标；第一坐标也相等时再比较第二坐标。

ordAt : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S k
ordAt m n a b c d =
    (var m ∈̇ var n)
  ∨̇ ((var m ≐ var n)
     ∧̇ ((var a ∈̇ var c) ∨̇ ((var a ≐ var c) ∧̇ (var b ∈̇ var d))))

把各部分合起来，Lt p q 说：p 与 q 是编码对，分别由成员 a、b 与成员 c、d 组成，其最大值 m 与 n 满足最大值条件，其比较满足 Gödel 条件。六个见证在截断之下记录：这些条件只断言见证存在，而经典情形分析是随后才在诸选项间作出选择。

Lt : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Lt p q = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ]
           ( (p ≡ pr (fst a) (fst b)) × (q ≡ pr (fst c) (fst d))
           × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d ) ∥₁

六个约束子需要超出调用者环境的六个槽位，↑6 恰好把索引移动这么多位置。

private
  ↑6 : ∀ {k} → Fin k → Fin (suc (suc (suc (suc (suc (suc k))))))
  ↑6 i = suc (suc (suc (suc (suc (suc i)))))

六个槽位被命名为 i0 到 i5，每个量化见证一个。前三条别名绑定第零、第一、第二位置，它们将容纳第二对的最大值、第一对的最大值、以及第二对的第二坐标。

  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc zero
  i2 : ∀ {k} → Fin (suc (suc (suc k)))

别名继续：第二位由第二对的第二坐标填充，第三位由其第一坐标填充，第四位由第一对的第二坐标填充。

  i2 = suc (suc zero)
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc (suc (suc zero))
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
  i4 = suc (suc (suc (suc zero)))

第五位是第一对的第一坐标，六个至此齐备。序公式随之开始：它将依次绑定六个见证，并就 p 与 q 说出 Gödel 比较所要求的内容。

  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc (suc (suc (suc (suc zero))))
opaque
  ltAt : ∀ {k} → Fin k → Fin k → Formula S k
  ltAt p q = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (

公式体依次绑定六个见证，并合取五个原子：p 是第五、第四槽位组成的有序对，q 是第三、第二槽位组成的有序对，第一个最大值原子约束 p 的两个坐标，第二个最大值原子约束 q 的两个坐标，序原子则先比较两个最大值、再比较坐标。在六槽位语境中读出，这恰好说：p 在 Gödel 序下低于 q。

        prAtL (↑6 p) i5 i4
     ∧̇ (prAtL (↑6 q) i3 i2
     ∧̇ (maxAt i1 i5 i4
     ∧̇ (maxAt i0 i3 i2
     ∧̇ ordAt i1 i0 i5 i4 i3 i2)))))))))

充分性对照一个具体的六条目语境检验。该语境把六个见证以最新在前的方式添加到调用者的环境：n、m、d、c、b、a，于是第零槽位是 n、第五槽位是 a，与那些别名一致。

  private
    env : ∀ {k} → S ^ k → S → S → S → S → S → S
        → S ^ (suc (suc (suc (suc (suc (suc k))))))
    env γ a b c d m n = n ∷ m ∷ d ∷ c ∷ b ∷ a ∷ γ

第一条充分性引理在该语境读取配对原子：配对原子的满足，就是调用者的 p 与 a、b 的有序对之间的等式。

    atP : ∀ {k} (p : Fin k) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩
        ≡ (fst (lookup p γ) ≡ pr (fst a) (fst b))
    atP p γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 p) i5 i4 (env γ a b c d m n))

第二条对 q 与 c、d 的有序对做同样的事。有了这两条等同，公式的满足与 Lt 的六见证数据便可互换。

    atQ : ∀ {k} (q : Fin k) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩
        ≡ (fst (lookup q γ) ≡ pr (fst c) (fst d))
    atQ q γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 q) i3 i2 (env γ a b c d m n))

向外方向依次消耗六层嵌套的截断：ltAt p q 在 γ 处的满足给出见证 a 至 n，连同两条对等式、两份最大值数据与一份序数据。

  lt-out : ∀ {k} (p q : Fin k) (γ : S ^ k) → ⟨ γ ⊨ ltAt p q ⟩
         → Lt (fst (lookup p γ)) (fst (lookup q γ))
  lt-out p q γ = PT.rec squash₁ (λ { (a , ha) → PT.rec squash₁ (λ { (b , hb) →
    PT.rec squash₁ (λ { (c , hc) → PT.rec squash₁ (λ { (d , hd) →
    PT.rec squash₁ (λ { (m , hm) → PT.rec squash₁ (λ { (n , (hp , (hq , (hM , (hN , hO))))) →

两条对等式沿充分性路径传输；第一份最大值数据被搬运到外围层级。六个存在见证处于被提升的语义层，因此肯定的情形原样保留，反驳的情形则被从提升中降出。

      ∣ a , b , c , d , m , n
      , ( transport (atP p γ a b c d m n) hp
        , transport (atQ q γ a b c d m n) hq
        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM

第二份最大值数据以同样方式映射，从而在调用者的 p 与 q 处补全 Lt 的见证。

        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hN
        , hO ) ∣₁ }) hm }) hd }) hc }) hb }) ha })

向内方向把 Lt 转为满足陈述，而后者是命题。

  lt-in : ∀ {k} (p q : Fin k) (γ : S ^ k)
        → Lt (fst (lookup p γ)) (fst (lookup q γ)) → ⟨ γ ⊨ ltAt p q ⟩
  lt-in p q γ = PT.rec (snd (γ ⊨ ltAt p q))
    (λ { (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) →
      ∣ a , ∣ b , ∣ c , ∣ d , ∣ m , ∣ n

六个见证作为嵌套的存在见证被重新填入，两条对等式则沿充分性路径反方向传输。

      , ( transport (sym (atP p γ a b c d m n)) ep
        , ( transport (sym (atQ q γ a b c d m n)) eq'
        , ( PT.map (λ { (inl h) → inl h
                      ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM
          , ( PT.map (λ { (inl h) → inl h

两份最大值数据被映射回去，这次提升为对象层带守卫的原子，序数据随之封闭整条公式。Gödel 模块随后为集合 P 打包这条序：其描述条件要求两个坐标都是 P 的成员，并以序公式关联它们。

                        ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hN
            , hO )))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
private
  module Godel (P : S) = Relation P P
    ((var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ltAt (suc zero) zero))

宿主读法在两侧加上对 P 的隶属，与序关系合取；两个方向在两个约束子所占的槽位处引用向外与向内引理：第一坐标在外层槽位，第二坐标在内层槽位。

    (λ p q → (fst p ∈ˢ fst P) ⊓ ((fst q ∈ˢ fst P) ⊓ (Lt (fst p) (fst q) , squash₁)))
    (λ p q e h → h .fst , h .snd .fst , lt-out (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
    (λ p q e h → h .fst , h .snd .fst , lt-in (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))

godel P 就是那条被分离的关系：在 L 内部，由 P 的成员组成的、在 Gödel 序下相互低于的有序对之集。

godel : S → S
godel = Godel.rel

向内：对 P 的两个成员 p、q，若 p 低于 q，则它们的有序对属于 godel P。

godel-in : (P p q : S) → ⟨ fst p ∈ˢ fst P ⟩ → ⟨ fst q ∈ˢ fst P ⟩
         → Lt (fst p) (fst q) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
godel-in P p q mp mq l = Godel.into P p q mp mq (mp , mq , l)

向外：godel P 的成员带有两个成员及其间的序数据。

godel-out : (P p q : S) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
          → ⟨ fst p ∈ˢ fst P ⟩ × ⟨ fst q ∈ˢ fst P ⟩ × Lt (fst p) (fst q)
godel-out = Godel.pair-out

到宿主序的搬运

序模块随后固定一个序数 κ，即平方律所陈述的情形。

module Order (κ : S) (oκ : IsOrd (fst κ)) where

K 是序数 κ 的底层集合；平方律所展开的载体正是这个由 κ 以下序数组成的集合。

  K : V ℓ
  K = fst κ

↑ 借助小呈现的嵌入，在外围点名 K 的成员：每个索引指称它所呈现的那个序数。

  ↑ : ⟪ K ⟫ → V ℓ
  ↑ = ⟪ K ⟫↪

索引 m : ⟪ K ⟫ 指名外围集合 ↑ m，并带有它属于 κ 的证明。可构造性向成员传递，因此 upK m 把这个被指名的序数打包为 L 的元素。

  upK : ⟪ K ⟫ → S
  upK m = ↑ m , isL-trans {x = K} {y = ↑ m} (member K m) (snd κ)

待比较的序的载体是 Pair，即 κ 的两个索引组成的类型：宿主一侧的有序对，每个坐标都指名一个低于 κ 的序数。

  Pair : Type ℓ
  Pair = ⟪ K ⟫ × ⟪ K ⟫

坐标自身之上立着坐标序 ≺₁，引自外部的平方律构造：低于 κ 的序数按其所指名外围集合之间的隶属作严格比较。

  _≺₁_ : ⟪ K ⟫ → ⟪ K ⟫ → Type (ℓ-suc ℓ)
  _≺₁_ = SQ._≺₁_ K oκ

有序对之上立着 Gödel 序 ≺ₚ：先比最大值，再比第一坐标，最后比第二坐标。这正是内部公式必须复现的那条外部序。

  _≺ₚ_ : Pair → Pair → Type (ℓ-suc ℓ)
  _≺ₚ_ = SQ._≺_ K oκ

最大值运算 maxOrd 对低于 κ 的两个序数返回其中较大者，同样引自外部构造，也同样只因条目是序数才读作最大值。

  maxOrd : ⟪ K ⟫ → ⟪ K ⟫ → ⟪ K ⟫
  maxOrd = SQ.maxOrd K oκ

两个小事实为两侧的比较做准备。其一，序数 κ 的每个成员自身也是序数，故被点名的序数携带序数性证书。其二，max-out 陈述：在底层集合指名 a' 与 b' 的元素处读取的内部最大值条件，迫使内部最大值恰为 a' 与 b' 的宿主最大值；证明按宿主序的三歧数据展开。

  ord↑ : (m : ⟪ K ⟫) → IsOrd (↑ m)
  ord↑ m = mem-ord {A = K} oκ (↑ m) (member K m)
  max-out : (a b m : S) (a' b' : ⟪ K ⟫) → fst a ≡ ↑ a' → fst b ≡ ↑ b'
          → MaxIs m a b → fst m ≡ ↑ (maxOrd a' b')
  max-out a b m a' b' ea eb = PT.rec (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))

情形函数固定了该论证的形状：宿主三歧分成低于、相等、高于；内部数据分成肯定分支 (m 即 b) 与反驳分支 (m 即 a)。把两种分裂逐项配上，就是全部内容。

    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
         ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a))
       → fst m ≡ ↑ (SQ.maxGo K oκ a' b' t)

低于情形中，肯定分支把 m 与 b 的等式同 b 的命名复合，给出宿主最大值。其反驳分支不可能：它所反驳的隶属恰是三歧的见证，只须经两次命名传输即得。

    go (lt h) (inl (_ , e))   = e ∙ eb
    go (lt h) (inr (na , _))  =
      Empty.rec (na (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (sym ea) (sym eb) h))
    go (eq p) (inl (a∈b , _)) =
      Empty.rec (∈-irrefl (↑ b')

相等情形中，肯定分支会断言 a 属于 b，而宿主宣布二者相等，这与被点名序数 b 处隶属的非自反性矛盾；反驳分支随即把最大值命名为 a，并沿 a 的命名传输。

        (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (ea ∙ cong ↑ p) eb a∈b))
    go (eq p) (inr (_ , e))   = e ∙ ea
    go (gt h) (inl (a∈b , _)) =
      Empty.rec (∈-irrefl (↑ a')
        (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'}

高于情形中，宿主见证给出 b ∈ a；若内部仍取肯定分支，还会有 a ∈ b，传递性便在 a 处违背非自反性。

          (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea eb a∈b) h))
    go (gt h) (inr (_ , e))   = e ∙ ea

逆向的 max-in 把宿主最大值写进内部谓词：对每一对索引，由 maxOrd 指名的被提升元素在两个被提升坐标处满足 MaxIs。

  max-in : (a' b' : ⟪ K ⟫) → MaxIs (upK (maxOrd a' b')) (upK a') (upK b')
  max-in a' b' = go (SQ.tri₁ K oκ a' b')
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → MaxIs (upK (SQ.maxGo K oκ a' b' t)) (upK a') (upK b')

其三种情形由宿主比较直接得出：低于给出肯定分支且等式定义性成立；相等以非自反性反驳隶属；高于则借该坐标自身的序数性反驳。同一块中还定义了 code，即宿主对的两个被点名序数的外围有序对。

    go (lt h) = ∣ inl (h , refl) ∣₁
    go (eq p) = ∣ inr ((λ h → ∈-irrefl (↑ b') (subst (λ w → ⟨ ↑ w ∈ˢ ↑ b' ⟩) p h)) , refl) ∣₁
    go (gt h) = ∣ inr ((λ h' → ∈-irrefl (↑ a') (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'} h' h)) , refl) ∣₁
  code : Pair → V ℓ
  code p = pr (↑ (fst p)) (↑ (snd p))

搬运的核心是一条反驳引理。它假设一对形状即矛盾的数据：Lt 在 p 与 q 的编码对上成立，而宿主序却拒绝比较它们。这种假设下的 Lt 的六个见证被收拢为一条荒谬性陈述。

  private
    refute : (p q : Pair) → (p ≺ₚ q → Empty.⊥)
           → Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ]
               ( (code p ≡ pr (fst a) (fst b)) × (code q ≡ pr (fst c) (fst d))
               × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d )

结论是空类型：被假设的序数据与被拒绝的比较不能并存。证明拆开六个见证，在其所指名的底层集合上工作。

           → Empty.⊥
    refute (a' , b') (c' , d') nk (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) =
      PT.rec Empty.isProp⊥ outer hO
      where
      ea : fst a ≡ ↑ a'

有序对的单射性从每条编码等式中提取出：每个见证的底层集合与相应被点名序数的等同。这四条等式为后文所有比较提供了锚点。

      ea = sym (pr-inj ep .fst)
      eb : fst b ≡ ↑ b'
      eb = sym (pr-inj ep .snd)
      ec : fst c ≡ ↑ c'
      ec = sym (pr-inj eq' .fst)

两个最大值再经 max-out 施于两份最大值数据，而与宿主最大值等同。至此整个构形的内部读法与外部读法在全部六个坐标上一致。

      ed : fst d ≡ ↑ d'
      ed = sym (pr-inj eq' .snd)
      em : fst m ≡ ↑ (maxOrd a' b')
      em = max-out a b m a' b' ea eb hM
      en : fst n ≡ ↑ (maxOrd c' d')

等式 en 为第二个对给出同样的等同，于是现在可把 OrdIs 完整传输到宿主最大值与坐标上。

      en = max-out c d n c' d' ec ed hN

内层引理传递坐标比较：被点名第一坐标之间的外围隶属，沿两次命名的等同传输后，变成宿主序中的低于关系。

      inner : ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩)
            → (a' ≺₁ c') ⊎ ((a' ≡ c') × (b' ≺₁ d'))
      inner (inl h)       = inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea ec h)
      inner (inr (e , h)) =
        inr ( ↪-inj {a = K} (sym ea ∙ e ∙ ec)

相等情形同样传递：被点名集合的等式经两次命名的循环改写后，由 K 的命名的单射性变成索引的等式，而第二坐标照旧比较。

            , subst2 (λ x y → ⟨ x ∈ˢ y ⟩) eb ed h )

若第一个最大值属于第二个，沿 em 与 en 传输这份隶属，便得到 p ≺ₚ q 的严格最大值分支，与 nk 矛盾。

      outer : ⟨ fst m ∈ˢ fst n ⟩
            ⊎ ((fst m ≡ fst n)
               × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁)
            → Empty.⊥
      outer (inl h)       = nk (inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) em en h))

若两个最大值相等，底层集合的等式经命名单射性变成索引的等式，内层引理随后在宿主序内比较两对，再次反驳拒绝。

      outer (inr (e , h)) = PT.rec Empty.isProp⊥
        (λ w → nk (inr (↪-inj {a = K} (sym em ∙ e ∙ en) , inner w))) h

证明 lt→≺ 时，宿主对的三歧性给出三种可能。所需的严格分支可直接返回；在相等或反向严格的分支中，若拒绝 p ≺ₚ q，refute 会使之与已假设的 Lt 矛盾，因而仍得到所需比较。

  lt→≺ : (p q : Pair) → Lt (code p) (code q) → p ≺ₚ q
  lt→≺ p q l = go (SQ.tri≺ K oκ p q)
    where
    refuted : ((p ≺ₚ q) → Empty.⊥) → p ≺ₚ q
    refuted nk = Empty.rec (PT.rec Empty.isProp⊥ (refute p q nk) l)

相等情形中，假设的 p ≺ₚ q 可传输为 q ≺ₚ q，违背非自反性；反向严格情形中，把这份假设比较与 q ≺ₚ p 复合会得到 p ≺ₚ p，同样不可能。

    go : TriW (p ≺ₚ q) (p ≡ q) (q ≺ₚ p) → p ≺ₚ q
    go (lt k) = k
    go (eq e) = refuted (λ k → SQ.irr≺ K oκ q (subst (λ w → w ≺ₚ q) e k))
    go (gt h) = refuted (λ k → SQ.irr≺ K oκ p (SQ.trans≺ K oκ p q p k h))

逆向的 ≺→lt 把宿主比较写进对象语言。其六个见证是被提升的坐标与两个被提升的最大值，两条对等式定义性成立，最大值数据来自 max-in，序数据来自宿主比较本身。

  ≺→lt : (p q : Pair) → p ≺ₚ q → Lt (code p) (code q)
  ≺→lt (a' , b') (c' , d') k =
    ∣ upK a' , upK b' , upK c' , upK d' , upK (maxOrd a' b') , upK (maxOrd c' d')
    , ( refl , refl , max-in a' b' , max-in c' d' , ord k ) ∣₁
    where

序数据按情形逐条读取：严格隶属原样通过；两种相等情形分别沿最大值的命名与坐标的命名传输。

    ord : (a' , b') ≺ₚ (c' , d')
        → OrdIs (upK (maxOrd a' b')) (upK (maxOrd c' d')) (upK a') (upK b') (upK c') (upK d')
    ord (inl h)                 = ∣ inl h ∣₁
    ord (inr (e , inl h))       = ∣ inr (cong ↑ e , ∣ inl h ∣₁) ∣₁
    ord (inr (e , inr (f , h))) = ∣ inr (cong ↑ e , ∣ inr (cong ↑ f , h) ∣₁) ∣₁

若 x < y，与 y < z 传递即得 x < z；若 x = y，则沿该等式传输已有的 y < z。

  private
    ≤→≺ : (x y z : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≺₁ z → x ≺₁ z
    ≤→≺ x y z (inl h) h' = SQ.trans₁ K oκ x y z h h'
    ≤→≺ x y z (inr e) h' = subst (λ w → w ≺₁ z) (sym e) h'

配套引理由 x ≤ y 与 y = y' 得出 x 属于 y' 的后继。严格情形中，x ∈ y' 直接给出后继隶属；相等情形中，把 x 与 y' 等同后，目标化为 y' 属于自身后继。

    ≤→∈suc : (x y y' : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≡ y'
           → ⟨ ↑ x ∈ˢ sucV (↑ y') ⟩
    ≤→∈suc x y y' (inl h) e = ∈sucV-inl (subst (λ w → x ≺₁ w) e h)
    ≤→∈suc x y y' (inr q) e =
      subst (λ w → ⟨ ↑ w ∈ˢ sucV (↑ y') ⟩) (sym (q ∙ e)) (self∈sucV (↑ y'))

节段引理现在从序中读出：若对 r 低于对 p，则 r 的第一坐标属于 p 的最大值的后继；在最大值严格比较的情形，这是先「至多」再严格比较。

  fst∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (fst r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  fst∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) h)
  fst∈suc (a , b) (c , d) (inr (e , _)) =

最大值相等的情形中，第一坐标至多为共同的最大值，而两个最大值被等同，故隶属由「最大值属于自身后继」得出。

    ≤→∈suc a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) e

把同一论证施于第二坐标，即得 snd∈suc：r 的第二坐标同样落入 p 的最大值的后继，无论两个最大值严格比较还是相等。

  snd∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (snd r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  snd∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) h)
  snd∈suc (a , b) (c , d) (inr (e , _)) =

这两个界说明，对 (c, d) 的每个前驱，其两个坐标都属于 suc(max(c, d))。

    ≤→∈suc b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) e
module Coll (κ : S) (oκ : IsOrd (fst κ)) where

这些界控制 Gödel 序的每个前驱节段。结合良基性与传递性，它们使 prodL κ 上的关系处于可塌缩为序数序型的情形。

  open Order κ oκ

将要被塌缩成序型的集合是 P，即乘积：序数 κ 的成员的有序对之集，已在 L 内部分离而来。

  P : S
  P = prodL κ

塌缩所用关系是 R，即该乘积上的 Gödel 序：P 的两个成员恰好在其一低于另一个时相关。

  R : S
  R = godel P

对 Gödel 关系这可直接读出：只要 y R x，y 与 x 都是该乘积的成员。

  Rsub : (y x : S) → Holds R y x → ⟨ fst y ∈ fst P ⟩ × ⟨ fst x ∈ fst P ⟩
  Rsub y x h = godel-out P y x h .fst , godel-out P y x h .snd .fst

序型机制针对这个乘积一次性实例化。其定义域是塌缩的一个索引集，而 φ 为每个索引读出乘积中相应成员所呈现的宿主对：两个坐标由乘积的呈现读式无截断地恢复。

  module OT = Code P R Rsub using (Dom; Dom≡; isProp≺; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out; module Conjuncts)
  φ : OT.Dom → Pair
  φ m = prodL-fst κ (OT.up m) (OT.up-mem m) .fst
      , prodL-fst κ (OT.up m) (OT.up-mem m) .snd .fst

该读式随附一条等式：索引的内部编码等于两个坐标的外围有序对。这条等式是内部序与外部序之间每一次比较所依赖的枢纽。

  φ-eq : (m : OT.Dom) → OT.↪ m ≡ code (φ m)
  φ-eq m = prodL-fst κ (OT.up m) (OT.up-mem m) .snd .snd

φ 是单射的：若两个索引指名同一宿主对，则它们的编码一致，而定义域自身的判据「编码相等」即返回索引相等。因此两个不同的乘积索引不可能被送到同一个宿主对。

  φ-inj : (m n : OT.Dom) → φ m ≡ φ n → m ≡ n
  φ-inj m n e = OT.Dom≡ (φ-eq m ∙ cong code e ∙ sym (φ-eq n))

向前传递把内部序向外读：若两个索引在 L 内部可比较，则它们的宿主对在 Gödel 序下可比较。证明引用定义等式与公式的外向读式，然后在两个宿主对上施用传递 lt→≺。

  ≺-fwd : (m n : OT.Dom) → m OT.≺ n → φ m ≺ₚ φ n
  ≺-fwd m n k = lt→≺ (φ m) (φ n)
    (subst2 Lt (φ-eq m) (φ-eq n) (godel-out P (OT.up m) (OT.up n) (OT.≺-out m n k) .snd .snd))

向后传递把宿主序向内读，引用公式的向内读式与同一对上的传递 ≺→lt。两个方向合起来说：塌缩索引上的内部关系，恰是经 φ 读出的宿主 Gödel 序。

  ≺-bwd : (m n : OT.Dom) → φ m ≺ₚ φ n → m OT.≺ n
  ≺-bwd m n k = OT.≺-in m n
    (godel-in P (OT.up m) (OT.up n) (OT.up-mem m) (OT.up-mem n)
      (subst2 Lt (sym (φ-eq m)) (sym (φ-eq n)) (≺→lt (φ m) (φ n) k)))

良基性随索引传递。宿主对的可及性给出相应索引的可及性，其前驱向前映到严格更小的对所对应的宿主对。于是沿外部序的归纳成为沿内部序的归纳。

  wf : WellFounded OT._≺_
  wf m = go (SQ.wf≺ K oκ (φ m))
    where
    go : {n : OT.Dom} → Acc _≺ₚ_ (φ n) → Acc OT._≺_ n
    go {n} (acc r) = acc (λ n' k → go (r (φ n') (≺-fwd n' n k)))

传递性同样传递：内部的两步先向外读出，由宿主序的传递性复合，再向内读回为从 a 直达 c 的一步。

  ≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
  ≺-trans {a} {b} {c} k k' =
    ≺-bwd a c (SQ.trans≺ K oκ (φ a) (φ b) (φ c) (≺-fwd a b k) (≺-fwd b c k'))

三歧性补全所传递的整套结构。对任意两个索引，宿主三歧比较它们的对；该陈述是内部比较的三向和。

  tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
  tri a b = go (SQ.tri≺ K oκ (φ a) (φ b))
    where
    go : TriW (φ a ≺ₚ φ b) (φ a ≡ φ b) (φ b ≺ₚ φ a)
       → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))

三种情形分别读回：两个严格情形经向后传递，相等情形经 φ 的单射性，指名同一宿主对的索引相等。

    go (lt h) = inl (≺-bwd a b h)
    go (eq e) = inr (inl (φ-inj a b e))
    go (gt h) = inr (inr (≺-bwd b a h))

良基性与传递性构造出塌缩及其序型；

  module C = OT.Conjuncts wf ≺-trans using (module Inj; col; col-ord; col-out; colTable; colTable-in; colTable-pair; colʟ; otL; otL-out)
  module I = C.Inj tri using (code; col-inj; module Inverse)
  injL-ot : InjL P C.otL
  injL-ot = ∣ C.colTable , I.code ∣₁

三条计数事实

三歧性随后证明塌缩映射单射，因此其图见证内部单射 P ↪ C.otL。

incl : (a b : V ℓ) → ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ b ⟩) → ⟪ a ⟫ ↪ ⟪ b ⟫

计数引理从外围一侧开始。两个外围集合之间的包含作用于小呈现：子集的每个索引指名较大集合的一个成员，而该成员在较大呈现中的纤维则指名相应的索引。

incl a b sub = ι , ι-inj
  where
  ι : ⟪ a ⟫ → ⟪ b ⟫
  ι m = fiber b (sub (⟪ a ⟫↪ m) (member a m)) .fst
  ι-inj : (m n : ⟪ a ⟫) → ι m ≡ ι n → m ≡ n

诱导出的索引映射是单射的：若子集的两个索引所指名的成员在较大呈现中被同一索引指名，则命名的等式迫使被指名成员相等，而子集自身的单射性返回索引的相等。

  ι-inj m n e = ↪-inj {a = a}
    (sym (fiber b (sub (⟪ a ⟫↪ m) (member a m)) .snd)
     ∙ cong ⟪ b ⟫↪ e
     ∙ fiber b (sub (⟪ a ⟫↪ n) (member a n)) .snd)
opaque

L 中的编码单射可在外围读出：图的各项条件确定其定义域与值域的小呈现之间的单射。再结合每个无穷序数 a 都满足 ω ⊆ a，便把内部单射同通常的基数比较连接起来。

  coded→ambient : (a b : S) → Σ[ F ∈ S ] InjCode F a b → ⟪ fst a ⟫ ↪ ⟪ fst b ⟫
  coded→ambient a b (F , sv , dm , ij , ran) = Sm.small , Sm.small-inj
    where module Sm = Small F a b sv dm ij ran
ω⊆ : (a : V ℓ) → IsOrd a → (⟨ a ∈ˢ ω ⟩ → Empty.⊥)
   → (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩

ω 的包含由序数 a 处的三歧性得出：由无穷性假设 a 不属于 ω；a 等于 ω 时传输该隶属；ω 在 a 之内时由传递性转发每一份隶属。

ω⊆ a oa a∉ω z z∈ω = go (ord-tri a oa ω ω-ord)
  where
  go : ⟨ a ∈ˢ ω ⟩ ⊎ ((a ≡ ω) ⊎ ⟨ ω ∈ˢ a ⟩) → ⟨ z ∈ˢ a ⟩
  go (inl h)         = Empty.rec (a∉ω h)
  go (inr (inl e))   = subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω

其最后一种情形是把传递性施于 z ∈ ω 与 ω ∈ a。包含到手之后，第二条计数事实是排除：无穷序数不容许到 ω 之成员 (即有限序数) 的内部单射。

  go (inr (inr ω∈a)) = oa .fst z∈ω ω∈a
no-fin : (a b : S) → IsOrd (fst a) → (⟨ fst a ∈ˢ ω ⟩ → Empty.⊥)
       → IsOrd (fst b) → ⟨ fst b ∈ˢ ω ⟩ → InjL a b → Empty.⊥
no-fin a b oa a∉ω ob b∈ω = PT.rec Empty.isProp⊥ (λ c →
  finite-excl-ω (fst b) ob b∈ω (λ x → h c x , h c x)

反驳的最后一步引用 ω 含于 a 的事实：由于 ω ⊆ a，两条引理得以复合，于是「ω 单射入 b」经过 a 中转就成了「ω 单射入有限集 b」。包含映射 ι 在 where 子句中一次性确定。

    (λ x y e → ι .snd x y
       (coded→ambient a b c .snd (ι .fst x) (ι .fst y) (cong fst e))))
  where
  ι : ⟪ ω ⟫ ↪ ⟪ fst a ⟫
  ι = incl ω (fst a) (ω⊆ (fst a) oa a∉ω)

映射 h 在包含 ω ↪ a 之后求值编码单射。

  h : Σ[ F ∈ S ] InjCode F a b → ⟪ ω ⟫ → ⟪ fst b ⟫
  h c x = coded→ambient a b c .fst (ι .fst x)

编码单射提升到乘积

为构造乘积上的映射，固定一个图 F：它在 a 上单值、定义域为 a、具有单射性，且取值落在 b 中；这四项正是编码单射 a ↪ b 的条件。

module ProdMap (a b F : S)
               (sv : ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩)

映射 h 在包含 ω ↪ a 之后求值编码单射。为构造乘积上的映射，固定一个图 F：它在 a 上单值、定义域为 a、具有单射性，且取值落在 b 中；这四项正是编码单射 a ↪ b 的条件。

               (ij : ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩)
               (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                    → ⟨ fst y ∈ fst b ⟩) where

提取模块从图中读出真正的函数：toFun 在每个定义域元素处计算取值，toFun-graph 证明相应的对属于图，toFun-inj 把图的单射性转移到函数上。

  module E = Extract F a sv dm using (toFun; toFun-graph; toFun-inj)

两个谓词刻画所涉对象。Mem p 说 p 是乘积 prodL a 的成员；Comp p 说 p 可分解为 a 的两个成员 x 与 y，且其有序对恰是 p 的底层集合。

  Mem : S → Type (ℓ-suc ℓ)
  Mem p = ⟨ fst p ∈ˢ fst (prodL a) ⟩
  Comp : S → Type (ℓ-suc ℓ)
  Comp p = Σ[ x ∈ S ] Σ[ y ∈ S ]
             (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩ × (fst p ≡ pr (fst x) (fst y)))

乘积成员的分量唯一，isPropComp 证明这一点。第一投影由有序对的单射性等同；第二投影随后在内层引理中比较。

  isPropComp : (p : S) → isProp (Comp p)
  isPropComp p (x , y , _ , _ , e) (x' , y' , _ , _ , e') =
    Σ≡Prop inner (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .fst))
    where
    inner : (x : S)

内层引理比较第二分量：与同一第一坐标配对的两个候选 y 与 y' 相等，因为对等式把它们的底层集合与同一个集合等同，而可构造性与隶属分量都是命题。

          → isProp (Σ[ y ∈ S ] (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩
                                × (fst p ≡ pr (fst x) (fst y))))
    inner x (y , _ , _ , e) (y' , _ , _ , e') =
      Σ≡Prop (λ w → isProp× (snd (fst x ∈ˢ fst a))
                      (isProp× (snd (fst w ∈ˢ fst a)) (setIsSet _ _)))

最后一个分量由底层集合的相等消解，唯一性随之完成：Comp p 是命题，故其截断的存在可以消去为一份真实的分解。

        (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .snd))

读式 comp 把乘积的截断隶属变成真实的分解，而刚刚证明的唯一性正是这一消去的许可。取值映射 val 随后在 a 的每个成员 x 处计算编码单射 F 指派给它的元素。

  comp : (p : S) → Mem p → Comp p
  comp p mp = PT.rec (isPropComp p) (λ z → z) (prodL-out a p mp)
  opaque
    val : (x : S) → ⟨ fst x ∈ˢ fst a ⟩ → S
    val x mx = E.toFun (x , mx)

图引理证明：计算出的取值与其输入在图中配对，即 x 与 val x 的有序对属于 F。这就是赋值的记录，对 a 的每个成员都予保留。

    val-graph : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩)
              → ⟨ pr (fst x) (fst (val x mx)) ∈ fst F ⟩
    val-graph x mx = E.toFun-graph (x , mx)

单射性引理把图的单射性转移到计算出的取值上：若 a 的两个成员被指派的取值有相同的底层集合，则这两个成员本身相等。这正是使对上的提升映射成为单射的关键。

    val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩) (x' : S) (mx' : ⟨ fst x' ∈ˢ fst a ⟩)
            → fst (val x mx) ≡ fst (val x' mx') → fst x ≡ fst x'
    val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')

提升映射 fn 作用于乘积成员的方式是按坐标施用 F：即第一坐标的像与第二坐标的像组成的内部有序对。

  fn : (p : S) → Mem p → S
  fn p mp = prʟ (val (comp p mp .fst) (comp p mp .snd .snd .fst))
                (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))

像落入 b 之上的乘积：由值域子句，两个分量取值都是 b 的成员，故其内部对属于 prodL b。内部对与外围对的等同则沿其第一投影引理传输。

  into : (p : S) (mp : Mem p) → ⟨ fst (fn p mp) ∈ˢ fst (prodL b) ⟩
  into p mp =
    subst (λ w → ⟨ w ∈ˢ fst (prodL b) ⟩) (sym (prʟ-fst (val x mx) (val y my)))
      (prodL-in b (val x mx) (val y my)
        (ran x (val x mx) (val-graph x mx)) (ran y (val y my) (val-graph y my)))

p 的分解给出坐标 x,y，并同时给出 x ∈ a 与 y ∈ a 的证明。这些隶属证明是数据的一部分，因为 val 只在 a 的成员上定义。

    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst

链类型汇集图公式须见证的全部内容：p 是 x 与 y 的对，q 是 x' 与 y' 的对，且 F 的图包含两个第一坐标的对与两个第二坐标的对。

  Chain : S → S → S → S → S → S → Type (ℓ-suc ℓ)
  Chain q p x y x' y' =
      (fst p ≡ pr (fst x) (fst y)) × (fst q ≡ pr (fst x') (fst y'))
    × ⟨ pr (fst x) (fst x') ∈ fst F ⟩ × ⟨ pr (fst y) (fst y') ∈ fst F ⟩

图公式 mapFo 以存在量词选取 x,y,x',y'，并合取四项断言：p=(x,y)、q=(x',y')，以及 F 的两次应用。

  opaque
    mapFo : Formula S 
    mapFo = ∃̇ (∃̇ (∃̇ (∃̇ (
          prAtL i5 i3 i2
       ∧̇ (prAtL i4 i1 i0

最后两个原子是应用子句：F 的图包含两个第一坐标的对与两个第二坐标的对，这恰是「F 把 x 映到 x'、把 y 映到 y'」的陈述。

       ∧̇ (appC F i3 i1
       ∧̇ appC F i2 i0))))))

充分性对照一个具体的六条目语境检验：该语境先加入四个见证 (最新在前)，再接对 q 与对 p，于是第零槽位是 y'、第五槽位是 p，与四个原子的索引一致。

    private
      env₄ : S → S → S → S → S → S → S ^ 
      env₄ q p x y x' y' = y' ∷ x' ∷ y ∷ x ∷ q ∷ p ∷ []

第一条充分性引理读取 p 的配对原子：该原子在语境中的满足，就是 p 的底层集合与 x、y 的有序对之间的等式。

      at1 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i5 i3 i2 ⟩ ≡ (fst p ≡ pr (fst x) (fst y))
      at1 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i5 i3 i2 (env₄ q p x y x' y'))

第二条充分性引理对 q 与见证 x'、y' 做同样的事。这两条等式为链的对部分提供了锚点。

      at2 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i4 i1 i0 ⟩ ≡ (fst q ≡ pr (fst x') (fst y'))
      at2 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i4 i1 i0 (env₄ q p x y x' y'))

第三条充分性引理读取第一个应用原子：其在 L 中的满足，被等同于两个第一坐标组成的对在 F 图中的外围隶属。

      at3 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i3 i1 ⟩ ≡ ⟨ pr (fst x) (fst x') ∈ fst F ⟩
      at3 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i3 i1 (env₄ q p x y x' y'))

第四条对第二坐标做同样的事，四个原子由此全部翻译为关于集合成员的普通陈述。

      at4 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i2 i0 ⟩ ≡ ⟨ pr (fst y) (fst y') ∈ fst F ⟩
      at4 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i2 i0 (env₄ q p x y x' y'))

向外方向依次消耗四层嵌套的存在量词，组装出截断的链：四个见证连同全部四个原子都传输到其外围读法。

    mapFo-out : (q p : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
              → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] Σ[ x' ∈ S ] Σ[ y' ∈ S ] Chain q p x y x' y' ∥₁
    mapFo-out q p = PT.rec squash₁ (λ { (x , hx) → PT.rec squash₁ (λ { (y , hy) →
      PT.rec squash₁ (λ { (x' , hx') → PT.map (λ { (y' , (h1 , (h2 , (h3 , h4)))) →
        x , y , x' , y'

每个原子都沿其自身的充分性路径传输，因此链所记录的是普通的等式与普通的隶属，而非满足判断。

        , ( transport (at1 q p x y x' y') h1 , transport (at2 q p x y x' y') h2
          , transport (at3 q p x y x' y') h3 , transport (at4 q p x y x' y') h4 ) })
        hx' }) hy }) hx })