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 順序

切り詰めのない読みはどの選択にも依存しない。積を手にしたところで、順序が登場する。MaxIs は、a と b が順序数であるとき、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 までの名前が付き、量化された証人ごとに一つである。最初の三つの別名は位置 0、1、2 を束縛し、そこには第二の対の最大値、第一の対の最大値、第二の対の第二座標が入る。

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

別名は続く。位置 2 には第二の対の第二座標が、位置 3 にはその第一座標が、位置 4 には第一の対の第二座標が入る。

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

位置 5 は第一の対の第一座標であり、六つがそろう。ついで順序の論理式が始まる。六つの証人を順に束縛し、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 の座標を結び、順序の原子が二つの最大値を、ついで座標を比較する。六スロットの文脈で読めば、これはまさに、Gödel 順序において p が 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 であり、スロット 0 が n、スロット 5 が 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))