L の内部にある極限段階の順序

宇宙レベル ℓ と、いま説明した排中律の実例を固定する。この時点では、後で作る内部関係はまだ条件つきである。有限段階の順序を表す論理式と、その意味論の二方向を与えた後に、モジュール Described の内部で定義される。次章がその実例を与え、後続の構成が使えるように codeOrder を公開する。

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

Lset ω の要素には、外側ですでに狭義整列順序が与えられている。ここでの問いは、その比較を L の内部の論理式からどのように使えるようにするかである。答えは三つの異なる形を順に通る。メタ水準の比較、その比較の対象言語による記述、そして有限段階の記述が与えられた後に、その関係を実現する構成可能集合である。

この章のすべての構成は、レベル ℓ-suc ℓ における一つの明示的な排中律の実例に相対している。先の章では、この仮定から極限段階の要素が最初に現れる有限段階を得た。この章では、用いる分出と上界の結果にも同じ実例を渡す。この仮定は必要な箇所で命題を判定するが、任意の族に対する選択関数を与えない。

対象言語は、構文と階層における意味を混同せずに比較を記述しなければならない。論理式は変数、定数、所属、結合子、量化子を使う。定数領域は構成可能な台なので、定数はすでに特定の構成可能集合を指す。後で必要となる二つの基本的な判定は、符号化の補題から得られる。順序対の等式は二つの成分を決定し、数項の符号化も単射である。さらに #mono は k < m を、# k が # m に属するという事実へ移す。したがって集合論的所属は、有限添字の狭義比較を忠実に表せる。

ここで用いる構造は構成可能宇宙である。その台の要素は、集合と構成可能性の証拠をひとまとめにする。推移性により、その集合の各要素にも同じ種類の証拠が得られる。このため、通常の階層における所属の証人を対象言語の環境へ移せる。とくに、finiteStage n は Lset (# n) という段階であり、極限段階は Lset ω である。数項と順序数に関する事実により、添字と、それが名指す段階を区別できる。包装された段階と定数 ωʟ によって、論理式は構造の内部からこの階層について語れる。

三つの橋によって、意味論上の比較を L の集合へ変える。まず smallDom は、小さな族を一つの共通な構成可能集合に入れるが、その上界が族の像と一致するとは主張しない。次に分出は、その上界から一変数の論理式を満たす要素だけを正確に取り出す。最後に、順序対、関係への所属、階層列を記述する符号化論理式には、充足を対応する集合の事実へ移す妥当性の法則がある。これらにより、共通の領域を見つける問題と、その領域上で正確な関係を述べる問題を分けて扱える。

表現すべき比較は、外側ですでに定義されている。後続段階では、before (suc n) が before n によってより前の点を並べ、finiteStage n の二つの部分集合を最初の相違で比較する。precedes R A x y の証人は A に属し、y に属して x には属さず、より前のすべての点で x と y が一致することを記録する。その存在は命題的に切り詰められている。型 Limit は Lset ω の要素を包装し、その最小出現段階が limitOrder の第一の鍵になる。対応する before の比較を使うのは、段階が等しい場合だけである。得られる関係集合の二つの表現方向は、Adequacy.Keys が要求する形に正確に一致する。

limitOrder は SWO の構造として与えられている。比較そのものに加え、三分性、非反射性、推移性、整礎性を備える。内部化の議論はこれらの法則を証明し直さない。後では、最初の三つを一つの目的に使う。対象言語の選言から読み戻せるのが命題的に切り詰められた狭義比較だけであるとき、三分性が候補となる枝を示し、非反射性と推移性が両立しない枝を退ける。

極限の比較は、後で必要となる辞書式の形をしている。第一の選択肢は、最初の要素のレベルが小さいことを述べる。第二の選択肢は、二つのレベルが一致し、その共通レベルの before によって基礎集合を比較する。自然数の三分性が第一の鍵を分析し、subst2 は等式が符号化されたレベルや端点を同定するとき、二項関係を運ぶ。付随する Lift と lower は宇宙レベルをそろえるだけであり、命題的な切り詰めを取り除く操作ではない。

open import Cubical.Data.Nat.Order using ( _<_; _≟_ )
import Cubical.Data.Nat.Order as NatOrder

対象言語の存在量化と選言は、それぞれ命題的に切り詰められた存在と枝の選択として解釈される。したがって、その証人を使えるのは、不可能性、階層の集合の等式、別の切り詰めなど、目標が命題である場合だけである。ただし、この章に現れるすべての存在型が切り詰められているわけではない。型が明示的なデータを要求する場合、包装された台の要素や共通上界はそのまま見える。また、命題的切り詰めから狭義比較を復元する議論は一般的な除去原理ではなく、limitOrder の三分性と順序法則に特有のものである。

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

上界の補題を使うには、Lset ω の要素に小さな添字型が必要である。ファイバー ⟪ Lset ω ⟫ がその添字を与え、∈-asFiber は与えられた所属証明を、像が元の要素になる添字へ変える。したがって二つのファイバーの積は、極限段階の要素からなるすべての順序対を添字づける。後で作る pairsBound はこれらの対をすべて含むが、正確な関係が得られるのは分出の後である。

  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; ω )

ここでは三つの所属記号が別々の役割をもつ。台の要素に対する x ∈ˢ y は、構成可能構造の命題値の所属である。基礎となる階層の集合どうしでは、x .fst ∈ y .fst が周囲の所属を表す。論理式の内部では _∈̇_ は所属を表す構文上の原子にすぎない。次に導入する充足判定が、第三の形に最初の二つの意味を与える。この層の区別により、順序を記述する論理式を、その実現集合が内部で整列順序をなすという証明と取り違えずに済む。

open hPropView 𝒮ʟ

判定 _⊨_ は、周囲の階層構造を構成可能クラスに制限して得られる内側の充足関係である。その台は集合と構成可能性の証拠からなるので、定数も量化される値も構成可能な対象を範囲とする。原子的所属は第一射影を通して解釈され、推移性により、構成可能な限界の要素を再び台の要素として包装できる。したがって充足は、対象言語の論理式から、その基礎集合についての通常の所属事実へ至る正確な橋になる。

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

limitOrder がもつ比較を _≺ˡ_ と書く。二つの極限段階の要素を、まず最小出現レベルで比較し、それが一致するときは共通の有限段階における最初の相違で比較する。残る目標は条件つきである。各有限段階の before 関係を所定の領域で表現する対象言語の論理式が与えられたと仮定し、Described の内部で集合 codeOrder を作る。そして u と v の順序対がこの集合に属することとu ≺ˡ v が成り立つことを同値にする。次章が必要な有限段階の論理式を与え、実際に使える実例を得る。

open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )

束縛変数は de Bruijn 位置で表される。二つの入れ子になった束縛を開くと、外側の環境にある各位置は二つの新しい項目を越える必要があり、sh2 がその移動を正確に記録する。最初の相違を表す論理式が候補となる相違点と、その下にある点を順に束縛するとき、また異なるレベルの枝が二つのレベル数項を束縛するときに使う。この移動は既存の自由変数の参照位置だけを変え、その変数が指す集合や関係を変えない。

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

環境が含むのは、裸の階層集合ではなく構成可能な台の要素である。そこで自然数 k に対し、towerS k は段階 Lset (# k) とその構成可能性の証拠を包装する。定義は不透明なので、後の証明は階層の構成を展開せず、公開された射影等式を通して使う。この不透明性は簡約を制御するだけであり、数学的な仮定を加えない。

opaque
  towerS : ℕ → S
  towerS k = LsetS (# k) (numeral-ord k)

等式 towerS-fst k は、この台の要素の基礎集合を Lset (# k) と同一視する。同じ段階に対する二つの見方を結ぶ点である。論理式は包装された要素 towerS k を受け取り、外側の階層の補題は基礎となる階層集合への所属を述べる。後の証明は、二つの見方の間で所属事実を運ぶたびにこの等式を通る。

  towerS-fst : (k : ℕ) → (towerS k) .fst ≡ Lset (# k)
  towerS-fst k = refl

添字そのものにも別の台の要素が必要である。numS k は数項 # k と、それが構成可能であることの証拠を包装する。numS k と towerS k を区別することで、前者が順序数添字を指し、後者がその添字で指定される構成可能段階を指すという違いが明確になる。LevelAt は階層列の記述を通して、この二つの対象を結ぶ。

  numS : ℕ → S
  numS k = # k , numL k

射影等式 numS-fst k は、包装された数項から # k を取り出す。towerS-fst k と合わせることで、同じ自然数を二つの役割で整合的に使える。一方では環境におけるレベルの値であり、他方では証人が示す段階の添字である。これらの等式が、対象言語の値と、数項や段階についての外側の事実との間の輸送を正当化する。

  numS-fst : (k : ℕ) → (numS k) .fst ≡ # k
  numS-fst k = refl

環境の位置 i の基礎集合が # j であるとする。補題 towerGraph は、新しい位置に towerS j を置き、LsetGraphAt が二つの位置を関係づけることを証明する。その内容は階層列の仕様そのものである。数項 # j に対応する値は段階 Lset (# j) である。したがって同じ補題が、真のレベルにおける存在と、そのレベルを用いた最小性の検証の双方に、実際の塔の証人を与える。

towerGraph : ∀ {n} (j : ℕ) (δ : Vec S n) (i : Fin n) → (lookup i δ) .fst ≡ # j
           → ⟨ (towerS j ∷ δ) ⊨ LsetGraphAt zero (suc i) ⟩
towerGraph j δ i q = Lset-defines zero (suc i) (towerS j ∷ δ)
  (subst IsOrd (sym q) (numeral-ord j))
  (towerS-fst j ∙ cong Lset (sym q))

レベルを内部で述べる

論理式 LevelAt b x が第一の鍵の記述を始める。まず位置 b の値が ω に属することを要求するので、その値は数項として復号できる。次に、その数項において LsetGraphAt が記述する値の存在を求め、位置 x の値が得られた段階に属することを要求する。これらの節により b は x の出現段階となり、残る節がそれを最小にする。

LevelAt : ∀ {n} → Fin n → Fin n → Formula S n
LevelAt b x =
  (var b ∈̇ con ωʟ)
  ∧̇ ( ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) )
    ∧̇ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero)

最小性は、候補となる数項 b の直前の要素だけでなく、すべての要素 u にわたって表される。そのような u で記述される各段階に、位置 x の値は属してはならない。# k の要素はちょうど小さい数項なので、候補 b = # k は 0 からk-1 までのすべての段階を排除する。二つの入れ子の束縛が x の位置の移動を説明する。意味論上、これらの全称節は関数型である。近くにある数項所属の命題的に切り詰められた復号は、命題を目標とするときだけ使われ、小さい添字を一つ選び出すことはない。

                     ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) )

LevelAt の二つの読みを証明するため、実際の極限段階の要素 a、自然数 k、そして k をその最小出現レベルと同定する等式 qk : level a ≡ k を固定する。levelData a の正の成分を qk に沿って運ぶと aIn が得られる。これは a の基礎集合が Lset (# k) に属するという事実である。負の成分は、m < k である任意の m に対し、Lset (# m) への所属が不可能であることを述べる。これらは、論理式が真のレベルを認識するために必要な存在と最小性の事実であり、さらに論理式が認識したどのレベルも # k に等しいことを示すために使われる。

module Level (a : Limit) (k : ℕ) (qk : level a ≡ k) where

private
  aIn : ⟨ a .fst ∈ Lset (# k) ⟩
  aIn = subst (λ j → ⟨ a .fst ∈ Lset (# j) ⟩) qk (level-in a)

  aMin : (m : ℕ) → ⟨ a .fst ∈ Lset (# m) ⟩ → m < k → ⊥₀
  aMin m h hm = levelData a .snd .snd m h
    (lift (subst (λ j → m < j) (sym qk) hm))

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

private
  Body : S → Type (ℓ-suc ℓ)
  Body c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
         × ⟨ (lookup x γ) .fst ∈ c .fst ⟩

LevelAt-in : (lookup b γ) .fst ≡ # k → (lookup x γ) .fst ≡ a .fst
           → ⟨ γ ⊨ LevelAt b x ⟩
LevelAt-in qb qx = hω , (hex , hmin)
  where
  hω : ⟨ (lookup b γ) .fst ∈ ω ⟩

  hω = subst (λ u → ⟨ u ∈ ω ⟩) (sym qb) (#∈ω k)

  hex : ⟨ γ ⊨ ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ⟩
  hex = ∣ towerS k , (towerGraph k γ b qb , hm) ∣₁
    where
    hm : ⟨ (lookup x γ) .fst ∈ (towerS k) .fst ⟩
    hm = subst (λ u → ⟨ (lookup x γ) .fst ∈ u ⟩) (sym (towerS-fst k))

      (subst (λ u → ⟨ u ∈ Lset (# k) ⟩) (sym qx) aIn)

  hmin : ⟨ γ ⊨ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero)
                              ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ⟩
  hmin u u∈ c hg hmem = lift (rec₁ isProp⊥ step
    (∈#-elim k (u .fst) (subst (λ w → ⟨ u .fst ∈ w ⟩) qb u∈)))
    where

    step : Σ[ m ∶ ℕ ] ((m < k) × (u .fst ≡ # m)) → ⊥₀
    step (m , (hm , qu)) = aMin m inStage hm
      where
      qc : c .fst ≡ Lset (u .fst)
      qc = Lset-only zero (suc zero) (c ∷ u ∷ γ) hg

        (subst IsOrd (sym qu) (numeral-ord m))
      inStage : ⟨ a .fst ∈ Lset (# m) ⟩
      inStage = subst (λ w → ⟨ a .fst ∈ Lset w ⟩) qu
        (subst (λ w → ⟨ w ∈ Lset (u .fst) ⟩) qx
          (subst (λ w → ⟨ (lookup x γ) .fst ∈ w ⟩) qc hmem))

LevelAt-out : ⟨ γ ⊨ LevelAt b x ⟩ → (lookup x γ) .fst ≡ a .fst
            → (lookup b γ) .fst ≡ # k
LevelAt-out (hω , (hex , hmin)) qx =
  rec₁ (setIsSet ((lookup b γ) .fst) (# k)) named hω
  where

  notAbove : (m : ℕ) → (lookup b γ) .fst ≡ # m → k < m → ⊥₀
  notAbove m qb hk = lower (hmin (numS k)
    (subst (λ w → ⟨ w ∈ (lookup b γ) .fst ⟩) (sym (numS-fst k))
      (subst (λ w → ⟨ # k ∈ w ⟩) (sym qb) (#mono k m hk)))
    (towerS k) (towerGraph k (numS k ∷ γ) zero (numS-fst k))

    (subst (λ w → ⟨ (lookup x γ) .fst ∈ w ⟩) (sym (towerS-fst k))
      (subst (λ w → ⟨ w ∈ Lset (# k) ⟩) (sym qx) aIn)))

  notBelow : (m : ℕ) → (lookup b γ) .fst ≡ # m → m < k → ⊥₀
  notBelow m qb hm = rec₁ isProp⊥ atTower hex
    where
    atTower : Σ[ c ∶ S ] Body c → ⊥₀
    atTower (c , (hg , hmem)) = aMin m inStage hm

      where
      qc : c .fst ≡ Lset (# m)
      qc = Lset-only zero (suc b) (c ∷ γ) hg
             (subst IsOrd (sym qb) (numeral-ord m))
         ∙ cong Lset qb

      inStage : ⟨ a .fst ∈ Lset (# m) ⟩
      inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx
        (subst (λ w → ⟨ (lookup x γ) .fst ∈ w ⟩) qc hmem)

  named : Σ[ j ∶ Lift ℕ ] (# (lower j) ≡ (lookup b γ) .fst)
        → (lookup b γ) .fst ≡ # k
  named (j , qj) = qb ∙ cong #_ (decide (lower j ≟ k))
    where
    qb : (lookup b γ) .fst ≡ # (lower j)

    qb = sym qj
    decide : NatOrder.Trichotomy (lower j) k → lower j ≡ k
    decide (NatOrder.lt h) = ⊥₀-rec (notBelow (lower j) qb h)
    decide (NatOrder.eq e) = e
    decide (NatOrder.gt h) = ⊥₀-rec (notAbove (lower j) qb h)

最初の相違を内部で述べる

論理式で集合を比較するには、構成可能な台の外部の要素を、まず意味論的な台S の要素として提示しなければならない。A : S で、その基礎集合に zが属するなら、構成可能性の推移性により、A に格納された証明から z が構成可能であるという証明が得られる。memS は z をこの継承された証明とともに包装する。これは依存的な台の要素を作るのであって、集合論的な順序対を作るのではない。

opaque
  memS : (A : S) (z : V ℓ) → ⟨ z ∈ A .fst ⟩ → S
  memS A z h = z , isL-trans {x = A .fst} {y = z} h (A .snd)

射影等式 memS-fst は、この包装が議論中の集合を保つことを述べる。memS A z h の基礎集合は z である。この等式自体は反射性で成り立つが、補題として明示することで、後の運搬は包装を展開せずに、量化された台の要素とそれが表す外部の集合との間を行き来できる。

  memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ A .fst ⟩) → (memS A z h) .fst ≡ z
  memS-fst A z h = refl

PrecedesAt は、r に格納された関係と A に格納された台に相対して、最初の相違による比較の一段階を表す。x と y にある集合について、台の要素 z で、y には属するが x には属さないものを要求する。この向きが比較を決める。決定点では右側の集合の所属値が一、左側の集合の所属値が零なので、x が y に先立つ。

PrecedesAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
PrecedesAt r A x y =
  ∃̇ ( (var zero ∈̇ var (suc A))
    ∧̇ ( (var zero ∈̇ var (suc y))
      ∧̇ ( ¬̇ (var zero ∈̇ var (suc x))

この証人はさらに、r の関係が定める最初の相違でなければならない。台 Aの各 w について、その関係が w を z より前に置くなら、w の x への所属と y への所属は両方向で一致しなければならない。論理式は appAt を通して関係を調べる。意味論的には、w と z の集合論的な順序対が r に格納された関係集合に属するかを問うている。z を束縛する存在量化子と w を束縛する全称量化子が、以前の変項を二つずらす理由である。

        ∧̇ ∀̇∈ (var (suc A))
             ( appAt (sh2 r) zero (suc zero)
             ⇒̇ ( ((var zero ∈̇ var (sh2 x)) ⇒̇ (var zero ∈̇ var (sh2 y)))
               ∧̇ ((var zero ∈̇ var (sh2 y)) ⇒̇ (var zero ∈̇ var (sh2 x))) ) ) ) ) )

モジュール Precedes は、この論理式を読むために必要なデータを正確に述べる。四つの位置と環境に加えて、メタレベルの関係 R を固定する。法則 Rrep は r にある関係集合への集合論的な順序対の所属を R の事実として読み、Rfill はその事実を所属へ書き戻す。これらの法則が構成可能な端点だけを扱えば十分なのは、量化された端点はすでにS に属し、外部の台の要素も memS で包装できるからである。ここでは R に順序公理を仮定しない。この論理式は一段階の比較の定義を表すだけであり、特定の関係が整列順序であるという後の証明には依存しない。

module Precedes {n : ℕ} (r A x y : Fin n) (γ : Vec S n)
                (R : V ℓ → V ℓ → hProp (ℓ-suc ℓ))
                (Rrep : (u v : S) → ⟨ pr (u .fst) (v .fst) ∈ (lookup r γ) .fst ⟩
                      → ⟨ R (u .fst) (v .fst) ⟩)
                (Rfill : (u v : S) → ⟨ R (u .fst) (v .fst) ⟩
                       → ⟨ pr (u .fst) (v .fst) ∈ (lookup r γ) .fst ⟩)
                where

private
  Aʟ : S
  Aʟ = lookup A γ

  xv : V ℓ
  xv = (lookup x γ) .fst

  yv : V ℓ
  yv = (lookup y γ) .fst

  Both : V ℓ → Type (ℓ-suc ℓ)
  Both w = (⟨ w ∈ xv ⟩ → ⟨ w ∈ yv ⟩) × (⟨ w ∈ yv ⟩ → ⟨ w ∈ xv ⟩)

  Agreeing : S → Type (ℓ-suc ℓ)
  Agreeing z = (w : S) → ⟨ w .fst ∈ Aʟ .fst ⟩
             → ⟨ (w ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩
             → Both (w .fst)

  Body : S → Type (ℓ-suc ℓ)
  Body z = ⟨ z .fst ∈ Aʟ .fst ⟩
         × ( ⟨ z .fst ∈ yv ⟩
           × ( (⟨ z .fst ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀) × Agreeing z ) )

PrecedesAt-out : ⟨ γ ⊨ PrecedesAt r A x y ⟩
               → ⟨ precedes R (Aʟ .fst) xv yv ⟩
PrecedesAt-out = rec₁ squash₁ atZ
  where
  atZ : Σ[ z ∶ S ] Body z → ⟨ precedes R (Aʟ .fst) xv yv ⟩

  atZ (z , (z∈A , (z∈y , (z∉x , hag)))) =
    ∣ z .fst , (z∈A , (z∈y , ((λ h → lower (z∉x h)) , ag))) ∣₁
    where
    ag : Agrees R (Aʟ .fst) xv yv (z .fst)
    ag w w∈A hR = subst Both (memS-fst Aʟ w w∈A) (hag wS w∈A' happ)

      where
      wS : S
      wS = memS Aʟ w w∈A
      w∈A' : ⟨ wS .fst ∈ Aʟ .fst ⟩
      w∈A' = subst (λ u → ⟨ u ∈ Aʟ .fst ⟩) (sym (memS-fst Aʟ w w∈A)) w∈A

      hp : ⟨ pr (wS .fst) (z .fst) ∈ (lookup r γ) .fst ⟩
      hp = Rfill wS z
        (subst (λ u → ⟨ R u (z .fst) ⟩) (sym (memS-fst Aʟ w w∈A)) hR)
      happ : ⟨ (wS ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩
      happ = subst ⟨_⟩

        (sym (appAt-adequate (sh2 r) zero (suc zero) (wS ∷ z ∷ γ))) hp

PrecedesAt-in : ⟨ precedes R (Aʟ .fst) xv yv ⟩
              → ⟨ γ ⊨ PrecedesAt r A x y ⟩
PrecedesAt-in = rec₁ squash₁ atZ
  where
  atZ : Σ[ z ∶ V ℓ ] Witness R (Aʟ .fst) xv yv z

      → ⟨ γ ⊨ PrecedesAt r A x y ⟩
  atZ (z , (z∈A , (z∈y , (z∉x , ag)))) =
    ∣ zS , (z∈A' , (z∈y' , (z∉x' , hag))) ∣₁
    where
    zS : S

    zS = memS Aʟ z z∈A
    qz : zS .fst ≡ z
    qz = memS-fst Aʟ z z∈A
    z∈A' : ⟨ zS .fst ∈ Aʟ .fst ⟩
    z∈A' = subst (λ u → ⟨ u ∈ Aʟ .fst ⟩) (sym qz) z∈A

    z∈y' : ⟨ zS .fst ∈ yv ⟩
    z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y
    z∉x' : ⟨ zS .fst ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀
    z∉x' h = lift (z∉x (subst (λ u → ⟨ u ∈ xv ⟩) qz h))
    hag : Agreeing zS

    hag w w∈A happ = ag (w .fst) w∈A hR
      where
      hp : ⟨ pr (w .fst) (zS .fst) ∈ (lookup r γ) .fst ⟩
      hp = subst ⟨_⟩ (appAt-adequate (sh2 r) zero (suc zero) (w ∷ zS ∷ γ)) happ
      hR : ⟨ R (w .fst) z ⟩

      hR = subst (λ u → ⟨ R (w .fst) u ⟩) qz (Rrep w zS hp)

順序を合成する

要素 a : Limit は、その底の集合が Lset ω に属するという証明を持つ。この構成可能な段階への所属から必要な isL の証拠が得られ、同じ底の集合をモデル要素 limitEl a とみなせる。

opaque
  limitEl : Limit → S
  limitEl a = a .fst , Lset→isL ω ω-ord (a .fst) (a .snd)

まとめる操作は集合を変えない。limitEl a を射影すると、定義により a .fst が戻る。この等式は後で、モデル内で作った順序対を表現定理に現れる周囲の順序対とそろえる。

  limitEl-fst : (a : Limit) → (limitEl a) .fst ≡ a .fst
  limitEl-fst a = refl

関係を L の内部に置くには、関係する二つの端点を、それ自身がモデル要素である順序対で表さなければならない。prS は任意の二つの構成可能な端点に対して、その内部順序対を与える。

  prS : S → S → S
  prS a b = prʟ a b

prS の射影則は、その底の集合を二つの端点の底の集合からなる周囲の順序対と同一視する。したがって、内部の対構成と外部の関係への所属は同じ集合について述べている。

  prS-fst : (a b : S) → (prS a b) .fst ≡ pr (a .fst) (b .fst)
  prS-fst a b = prʟ-fst a b

分出によって比較を満たす順序対を選ぶ前に、候補となるすべての対を含む集合サイズの共通の上界が必要である。Lset ω の要素を小さなファイバーで表示し、各要素を構成可能なものとしてまとめ、その二つの小さなファイバーの積で順序対を添字づける。

pairsBound : Σ[ D ∶ S ] ((u v : Limit) → ⟨ pr (u .fst) (v .fst) ∈ D .fst ⟩)
pairsBound = d .fst , onPair
  where
  ixL : ⟪ Lset ω ⟫ → S
  ixL m = ⟪ Lset ω ⟫↪ m , Lset→isL ω ω-ord (⟪ Lset ω ⟫↪ m)

各表示添字は実際に Lset ω の要素を表す。所属の橋は表示についての事実を通常の所属へ変え、その段階への所属から ixL がまとめるために必要な構成可能性の証明が得られる。

    (∈∈ₛ {a = ⟪ Lset ω ⟫↪ m} {b = Lset ω} .snd (∈ₛ⟪ Lset ω ⟫↪ m))

この小さな積に smallDom を適用すると、内部で作られたすべての順序対を含む構成可能集合が得られる。これは共通の上界にすぎず、余分な対象を含んでもかまわない。正確な比較関係は、その中で分出を行うことによって得られる。

  d : Σ[ D ∶ S ] ((p : ⟪ Lset ω ⟫ × ⟪ Lset ω ⟫)
                  → ⟨ prʟ (ixL (p .fst)) (ixL (p .snd)) ∈ˢ D ⟩)
  d = smallDom (⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) (λ p → prʟ (ixL (p .fst)) (ixL (p .snd)))

任意の u,v : Limit に対し、それぞれの底の集合は Lset ω の小さなファイバー内に表示添字を持つ。その添字から作った順序対は共通の上界に属し、射影の等式に沿って運ぶことで、周囲の順序対 pr (u .fst) (v .fst) の所属が得られる。

  onPair : (u v : Limit) → ⟨ pr (u .fst) (v .fst) ∈ (d .fst) .fst ⟩
  onPair u v = subst (λ t → ⟨ t ∈ (d .fst) .fst ⟩)
    (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd))
    (d .snd (fu .fst , fv .fst))
    where

二つのファイバーの証人は、上で使う表示添字と、そこで示される要素をそれぞれ u .fst、v .fst と同一視する等式を取り出す。この等式があるため、小さな表示で実際のすべての極限段階の端点を扱える。

    fu = ∈-asFiber {a = u .fst} {b = Lset ω} (u .snd)
    fv = ∈-asFiber {a = v .fst} {b = Lset ω} (v .snd)

論理式から読み取れるのが、極限上の狭義比較の命題的切り詰めだけである場合がある。strictLimit は、すでに証明された狭義整列順序 limitOrder の三分律を先に調べて比較を復元する。三分律が a ≺ˡ b を与える場合、選ぶべきものはもうない。

strictLimit : (a b : Limit) → ∥ a ≺ˡ b ∥₁ → a ≺ˡ b
strictLimit a b h = decide (SWO.tri∙ limitOrder a b)
  where
  decide : Tri (a ≺ˡ b) (a ≡ b) (b ≺ˡ a) → a ≺ˡ b
  decide (lt k) = k

切り詰められた順向きの比較があるなら、三分律の残る二つの場合は不可能である。a = b なら、運ぶことで自己比較が得られる。b ≺ˡ a なら、隠された順向きの比較と推移性から再び自己比較が得られる。非反射性がどちらの命題も否定するため、命題的切り詰めは矛盾へだけ除去されている。

  decide (eq q) = ⊥₀-rec (rec₁ isProp⊥
    (λ k → SWO.irr∙ limitOrder b (subst (λ t → t ≺ˡ b) q k)) h)
  decide (gt k) = ⊥₀-rec (rec₁ isProp⊥
    (λ j → SWO.irr∙ limitOrder a (SWO.trans∙ limitOrder a b a j k)) h)

level a の定義的性質により、a .fst は finiteStage (level a) に属する。等式 level a ≡ k に沿ってこの所属を finiteStage k へ運ぶと、有限段階の比較を使う際に必要な段階の境界がちょうど得られる。

levelStage : (a : Limit) (k : ℕ) → level a ≡ k → ⟨ a .fst ∈ finiteStage k ⟩
levelStage a k q = subst (λ j → ⟨ a .fst ∈ Lset (# j) ⟩) q (level-in a)

Described は条件つきの枠組みである。before m を記述するための論理式 BeforeAt と内向きの規則を受け取る。この規則を使えるのは、b にある値が # m を表し、第一の端点が finiteStage m に属する場合に限られる。

module Described
  (BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n)
  (BeforeAt-in : ∀ {n} (b x y : Fin n) (γ : Vec S n) (m : ℕ)
               → (lookup b γ) .fst ≡ # m
               → ⟨ (lookup x γ) .fst ∈ finiteStage m ⟩
               → ⟨ (lookup y γ) .fst ∈ finiteStage m ⟩
               → ⟨ before m ((lookup x γ) .fst) ((lookup y γ) .fst) ⟩
               → ⟨ γ ⊨ BeforeAt b x y ⟩)
  (BeforeAt-out : ∀ {n} (b x y : Fin n) (γ : Vec S n) (m : ℕ)
                → (lookup b γ) .fst ≡ # m
                → ⟨ (lookup x γ) .fst ∈ finiteStage m ⟩
                → ⟨ (lookup y γ) .fst ∈ finiteStage m ⟩
                → ⟨ γ ⊨ BeforeAt b x y ⟩
                → ⟨ before m ((lookup x γ) .fst) ((lookup y γ) .fst) ⟩)
  where

opaque
  LimitOrdAt : ∀ {n} → Fin n → Fin n → Formula S n
  LimitOrdAt x y =
    ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x)
           ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) )

    ∨̇ ∃̇ ( LevelAt zero (suc x)
         ∧̇ ( LevelAt zero (suc y) ∧̇ BeforeAt zero (suc x) (suc y) ) )

module Order {n : ℕ} (x y : Fin n) (γ : Vec S n)
             (u v : Limit) (ku kv : ℕ)
             (qu : level u ≡ ku) (qv : level v ≡ kv)
             (qx : (lookup x γ) .fst ≡ u .fst)
             (qy : (lookup y γ) .fst ≡ v .fst)
             where

private module Lu = Level u ku qu
private module Lv = Level v kv qv

private
  Split : S → S → Type (ℓ-suc ℓ)
  Split c d = ⟨ (d ∷ c ∷ γ) ⊨ LevelAt (suc zero) (sh2 x) ⟩
            × ( ⟨ (d ∷ c ∷ γ) ⊨ LevelAt zero (sh2 y) ⟩
              × ⟨ c .fst ∈ d .fst ⟩ )

  Same : S → Type (ℓ-suc ℓ)
  Same c = ⟨ (c ∷ γ) ⊨ LevelAt zero (suc x) ⟩
         × ( ⟨ (c ∷ γ) ⊨ LevelAt zero (suc y) ⟩
           × ⟨ (c ∷ γ) ⊨ BeforeAt zero (suc x) (suc y) ⟩ )

  split-in : ku < kv → Split (numS ku) (numS kv)
  split-in hlt =
      Lu.LevelAt-in (suc zero) (sh2 x) (numS kv ∷ numS ku ∷ γ)
        (numS-fst ku) qx
    , ( Lv.LevelAt-in zero (sh2 y) (numS kv ∷ numS ku ∷ γ)

          (numS-fst kv) qy
      , subst2 (λ s t → ⟨ s ∈ t ⟩) (sym (numS-fst ku)) (sym (numS-fst kv))
          (#mono ku kv hlt) )

  same-in : (e : level v ≡ level u)
          → ⟨ before (level u) (u .fst) (v .fst) ⟩ → Same (numS ku)
  same-in e h =
      Lu.LevelAt-in zero (suc x) (numS ku ∷ γ) (numS-fst ku) qx
    , ( Level.LevelAt-in v ku (e ∙ qu) zero (suc y) (numS ku ∷ γ)

          (numS-fst ku) qy
      , BeforeAt-in zero (suc x) (suc y) (numS ku ∷ γ) ku (numS-fst ku)
          (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx)
            (levelStage u ku qu))
          (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy)

            (levelStage v ku (e ∙ qu)))
          (subst2 (λ s t → ⟨ before ku s t ⟩) (sym qx) (sym qy)
            (subst (λ j → ⟨ before j (u .fst) (v .fst) ⟩) qu h)) )

  split-out : (c d : S) → Split c d → level u < level v
  split-out c d (hx , (hy , hlt)) = subst2 _<_ (sym qu) (sym qv)
    (#∈#-elim ku kv (subst2 (λ s t → ⟨ s ∈ t ⟩) qc qd hlt))
    where
    qc : c .fst ≡ # ku

    qc = Lu.LevelAt-out (suc zero) (sh2 x) (d ∷ c ∷ γ) hx qx
    qd : d .fst ≡ # kv
    qd = Lv.LevelAt-out zero (sh2 y) (d ∷ c ∷ γ) hy qy

  same-out : (c : S) → Same c
           → (level v ≡ level u) × ⟨ before (level u) (u .fst) (v .fst) ⟩
  same-out c (hx , (hy , hb)) = e , below
    where
    qc : c .fst ≡ # ku

    qc = Lu.LevelAt-out zero (suc x) (c ∷ γ) hx qx
    qc' : c .fst ≡ # kv
    qc' = Lv.LevelAt-out zero (suc y) (c ∷ γ) hy qy
    e : level v ≡ level u
    e = qv ∙ sym (#-inj′ (sym qc ∙ qc')) ∙ sym qu

    xIn : ⟨ (lookup x γ) .fst ∈ finiteStage ku ⟩
    xIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu)
    yIn : ⟨ (lookup y γ) .fst ∈ finiteStage ku ⟩
    yIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy)
      (levelStage v ku (e ∙ qu))

    below : ⟨ before (level u) (u .fst) (v .fst) ⟩
    below = subst (λ j → ⟨ before j (u .fst) (v .fst) ⟩) (sym qu)
      (subst2 (λ s t → ⟨ before ku s t ⟩) qx qy
        (BeforeAt-out zero (suc x) (suc y) (c ∷ γ) ku qc xIn yIn hb))

opaque
  unfolding LimitOrdAt

  LimitOrdAt-in : u ≺ˡ v → ⟨ γ ⊨ LimitOrdAt x y ⟩
  LimitOrdAt-in h = decide-in h
    where
    lower-in : ku < kv → ⟨ γ ⊨ LimitOrdAt x y ⟩
    lower-in hlt = ∣ inl ∣ numS ku , ∣ numS kv , split-in hlt ∣₁ ∣₁ ∣₁