L 中无穷基数的平方律

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

对底层集合及其可构造性证明应用 isSetClass，得到内层载体的 h-集合性。随后的对路径引理由两处分量的等式构造两个对的等式。

isSetS : isSet S
isSetS = isSetClass setIsSet (λ v → (isL v) .snd)
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
private module Product (K : S) = Relation K K

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

          ((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K))
          (λ x y → (x .fst ∈ˢ K .fst) ⊓ (y .fst ∈ˢ K .fst))
          (λ 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 ]
               (⟨ a .fst ∈ˢ K .fst ⟩ × ⟨ b .fst ∈ˢ K .fst ⟩
                × (e ≡ pr (a .fst) (b .fst))) ∥₁

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

prodL-in : (K a b : S) → ⟨ a .fst ∈ˢ K .fst ⟩ → ⟨ b .fst ∈ˢ K .fst ⟩
         → ⟨ pr (a .fst) (b .fst) ∈ˢ (prodL K) .fst ⟩
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) → ⟨ e .fst ∈ˢ (prodL K) .fst ⟩ → InProd K (e .fst)
prodL-out K e h = map₁ (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h)
prodL-fst : (K e : S) → ⟨ e .fst ∈ˢ (prodL K) .fst ⟩
          → Σ[ a ∶ ⟪ K .fst ⟫ ] Σ[ b ∶ ⟪ K .fst ⟫ ]
              (e .fst ≡ pr (⟪ K .fst ⟫↪ a) (⟪ K .fst ⟫↪ b))

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

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

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

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

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

  isPropFib : isProp (Σ[ a ∶ ⟪ K .fst ⟫ ] Σ[ b ∶ ⟪ K .fst ⟫ ]
                        (e .fst ≡ pr (⟪ K .fst ⟫↪ a) (⟪ K .fst ⟫↪ b)))
  isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner
    (↪-inj {a = K .fst} (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 =
  ∥ (⟨ a .fst ∈ˢ b .fst ⟩ × (m .fst ≡ b .fst))
  ⊎ ((⟨ a .fst ∈ˢ b .fst ⟩ → ⊥₀) × (m .fst ≡ a .fst)) ∥₁

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

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

最大值可写成一条有界公式：当 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 (a .fst) (b .fst)) × (q ≡ pr (c .fst) (d .fst))
           × 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} → Vec S k → S → S → S → S → S → S
        → Vec 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) (γ : Vec S k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩
        ≡ ((lookup p γ) .fst ≡ pr (a .fst) (b .fst))
    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) (γ : Vec S k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩
        ≡ ((lookup q γ) .fst ≡ pr (c .fst) (d .fst))
    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) (γ : Vec S k) → ⟨ γ ⊨ ltAt p q ⟩
         → Lt ((lookup p γ) .fst) ((lookup q γ) .fst)
  lt-out p q γ = rec₁ squash₁ (λ { (a , ha) → rec₁ squash₁ (λ { (b , hb) →
    rec₁ squash₁ (λ { (c , hc) → rec₁ squash₁ (λ { (d , hd) →
    rec₁ squash₁ (λ { (m , hm) → 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
        , map₁ (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM

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

        , 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) (γ : Vec S k)
        → Lt ((lookup p γ) .fst) ((lookup q γ) .fst) → ⟨ γ ⊨ ltAt p q ⟩
  lt-in p q γ = rec₁ ((γ ⊨ ltAt p q) .snd)
    (λ { (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'
        , ( map₁ (λ { (inl h) → inl h
                      ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM
          , ( 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 → (p .fst ∈ˢ P .fst) ⊓ ((q .fst ∈ˢ P .fst) ⊓ (Lt (p .fst) (q .fst) , 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) → ⟨ p .fst ∈ˢ P .fst ⟩ → ⟨ q .fst ∈ˢ P .fst ⟩
         → Lt (p .fst) (q .fst) → ⟨ pr (p .fst) (q .fst) ∈ˢ (godel P) .fst ⟩
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 (p .fst) (q .fst) ∈ˢ (godel P) .fst ⟩
          → ⟨ p .fst ∈ˢ P .fst ⟩ × ⟨ q .fst ∈ˢ P .fst ⟩ × Lt (p .fst) (q .fst)
godel-out = Godel.pair-out

到宿主序的搬运

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

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

K : V ℓ
K = κ .fst

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

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

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

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

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

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

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 ⟫) → a .fst ≡ ↑ a' → b .fst ≡ ↑ b'
        → MaxIs m a b → m .fst ≡ ↑ (maxOrd a' b')
max-out a b m a' b' ea eb = rec₁ (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))

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

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

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

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

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')

  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 (↑ (p .fst)) (↑ (p .snd))

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

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

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

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

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

    inner : ⟨ a .fst ∈ˢ c .fst ⟩ ⊎ ((a .fst ≡ c .fst) × ⟨ b .fst ∈ˢ d .fst ⟩)
          → (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)

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

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

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

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) → ⊥₀) → p ≺ₚ q
  refuted nk = ⊥₀-rec (rec₁ isProp⊥ (refute p q nk) l)

  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 : (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) ∣₁) ∣₁

private
  ≤→≺ : (x y z : ⟪ K ⟫) → let module O = SQ.OnOrdinal K oκ in x O.≤₁ 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'

  ≤→∈suc : (x y y' : ⟪ K ⟫) → let module O = SQ.OnOrdinal K oκ in x O.≤₁ 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'))

fst∈suc : (r p : Pair) → r ≺ₚ p
        → ⟨ ↑ (r .fst) ∈ˢ sucV (↑ (maxOrd (p .fst) (p .snd))) ⟩
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 : Pair) → r ≺ₚ p
        → ⟨ ↑ (r .snd) ∈ˢ sucV (↑ (maxOrd (p .fst) (p .snd))) ⟩
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 , _)) =

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

module Coll (κ : S) (oκ : IsOrd (κ .fst)) where

open Order κ oκ

P : S
P = prodL κ

R : S
R = godel P

Rsub : (y x : S) → Holds R y x → ⟨ y .fst ∈ P .fst ⟩ × ⟨ x .fst ∈ P .fst ⟩
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))