最初の相違の関係からなる内部の族

宇宙レベル ℓ を固定し、LEM (ℓ-suc ℓ) を仮定する。以下の集合、論理式、命題値関係はすべて、この選択で定まるレベルに属する。

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

各有限段階で、before n は二つの集合を最初に相違する要素によって比較する。本章では、この関係を L 内の集合 relAt n で表し、それらを数項で添字づけられた族にまとめ、その族での参照を対象言語の論理式 BeforeAt で表す。この論理式によって Described を具体化すると codeOrder が得られ、後の名前比較でコードの比較関係として使われる。本章自身は名前を比較せず、その比較の整礎性も証明しない。

この構成で排中律を使うのは、直後にモジュールへ与える明示的な仮定を通してだけである。したがって、この章から公開される各結果には古典的仮定が明示されたままになる。

累積階層上の一階論理式によって関係を記述する。関係の要素には順序対を用い、後にはその単射性によって、符号化された要素から比較される二集合を復元する。

第 n 有限段階は Lset (# n) であり、# n は階層内のフォン・ノイマン数項である。その順序数性と構成可能性により、この段階とその各要素を L のモデルの対象として扱える。

二つの集合構成は異なる役割を担う。分出は一つの段階の関係を上界から切り出し、置換は後で内部の ω に沿ってそれらの関係を集める。有限近似そのものは finSet と finSetL によって構成する。

数学的な再帰はすでに定まっている。before zero は空であり、before (suc n) は before n で先行する点を順序づけ、finiteStage n 上の最初の相違によって次の有限段階の要素を比較する。PrecedesAt はこの後続段階を対象言語で表し、RecShape はその有限近似を組織する。

対象言語の適用と外延性によって、ある集合が関係値を並べた表の値であることを論理式で述べられる。まず一回の再帰段階を記述するために使い、後には完成した族を数項の位置で読み取るために使う。

証明では集合と順序対の等式に沿う移送を繰り返し用いる。また、自然数の狭義順序に関する帰納によって、近似に記録された各値が一意に定まることを示す。

open import Cubical.Data.Nat.Order using

この帰納で使うのは自然数の < の整礎性である。すべての小さい添字で値を同定してから、k における値を決定する。これは before 自身の整礎性とは別の事柄である。

  ( _<_; <-trans; <-asym; pred-≤-pred; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Induction.WellFounded using ( module WFI )
open import Cubical.Data.FinData.Properties using ( toℕ<n; enum; toℕ∘enum )

以下では、いくつかの証人は命題的切り詰めの下でだけ得られる。この証人は存在を保証するが、標準的なデータを選び出さない。所属、before、または V における集合の等式のように、目標が命題である場合に消去できる。

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

集合には、その要素の表示を通してアクセスする。この表示により、有限段階の全要素を走って順序対を構成でき、内部の ω は最終的な族全体の定義域を与える。

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

以下では、論理式を構成可能集合がもつ命題値構造で解釈する。

open hPropView 𝒮ʟ

台 S は、集合と、それが L に属するという証明からなる。したがって内部関係を構成するには、基礎となる集合とその構成可能性の証明の両方が必要である。

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

絶対性は、この構造での充足を基礎となる集合についての対応する主張に結びつける。記法 γ ⊨ φ は、付値 γ が対象言語の論理式 φ を満たすことを表す。

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

二つの新しい変数を束縛すると、既存の各 de Bruijn 位置は二つ後ろへ移る。写像 sh2 はこの移動を記録し、新しい束縛子の下でも各自由変数が同じ対象を指すようにする。

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

二つ分の移動を二度適用して sh4 を得る。これは四つの束縛子の下で必要な調整である。

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

同様に、sh6 は六つの束縛子の下で元の参照を保つ。これらの移動が変えるのは de Bruijn 位置だけであり、論理式の数学的内容ではない。

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

対象 stageS n は有限段階 Lset (# n) を構成可能な台の要素としてまとめる。この包みを不透明にしておけば、後の議論は構成可能性証明の具体的な形に依存しない。

opaque
  stageS : ℕ → S
  stageS n = LsetS (# n) (numeral-ord n)

等式 stageS-fst は、この包みが担う数学的集合だけを明らかにする。その第一成分は finiteStage n である。

  stageS-fst : (n : ℕ) → (stageS n) .fst ≡ finiteStage n
  stageS-fst n = refl

対象 numS k も同様に、フォン・ノイマン数項 # k とその構成可能性の証明をまとめる。

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

等式 numS-fst により、後の論理式は隣に保存された証明を展開せずに、基礎となる数項を読み取れる。

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

z が構成可能集合 A に属するなら、L の推移性によって z も構成可能である。包み memS A z h はこの帰結を記録し、z をモデルの要素として使えるようにする。

  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 A z h の第一成分は元の集合 z のままであり、追加された成分は L への所属証明だけを与える。

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

モデル要素 a と b に対し、prS a b はそれらの順序対を L の内部で作る。以下の関係集合は、まさにこの形の対象を要素にもつ。

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

構成可能性の証明を忘れると、通常の順序対 pr (a .fst) (b .fst) が得られる。この等式が、内部の所属命題を基礎となる集合上の関係 before に結びつける。

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

特に、finiteStage n の各要素 x は台 S に持ち上げられる。その段階自身が、この持ち上げに必要な構成可能性の証明を与える。

stageEl : (n : ℕ) (x : V ℓ) → ⟨ x ∈ finiteStage n ⟩ → S
stageEl n x h = x , Lset→isL (# n) (numeral-ord n) x h

各段階の関係を L の要素にする

分出によって関係を表すには、まず可能な要素をすべて含む一つの集合が必要である。そこで pairsAt n は構成可能な上界 D を与え、u と v がともに finiteStage n に属するとき pr u v を含むようにする。

pairsAt : (n : ℕ)
        → Σ[ D ∶ S ] ((u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
                     → ⟨ pr u v ∈ D .fst ⟩)
pairsAt n = d .fst , onPair
  where

有限段階の表示された要素には、その所属証明がすでに付いている。写像 ixL は、そこから得られる構成可能性証明を添え、各要素を S の要素にする。

  ixL : ⟪ finiteStage n ⟫ → S
  ixL m = ⟪ finiteStage n ⟫↪ m
        , Lset→isL (# n) (numeral-ord n) (⟪ finiteStage n ⟫↪ m)
            (∈∈ₛ {a = ⟪ finiteStage n ⟫↪ m} {b = finiteStage n} .snd
              (∈ₛ⟪ finiteStage n ⟫↪ m))

二つの表示の積は、段階の要素からなるすべての対を添字づける。それらの内部順序対に smallDom を適用すると、この添字族全体が一つの構成可能集合 D に収まる。

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

任意の u,v ∈ finiteStage n に対し、その所属証明から表示の添字 fu と fv が得られる。上界はその添字位置の順序対を含み、復元した成分の等式に沿って移送すれば、pr u v 自身の所属が得られる。

  onPair : (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
         → ⟨ pr u v ∈ (d .fst) .fst ⟩
  onPair u v hu hv = 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))

二つのファイバー fu と fv は、表示の添字と、そこで表された要素をそれぞれ u、v と同定する等式を正確に記録する。

    where
    fu = ∈-asFiber {a = u} {b = finiteStage n} hu
    fv = ∈-asFiber {a = v} {b = finiteStage n} hv

同じ台 A 上で、各 R' w z から R w z が従うとする。このとき R に関する最初の相違の証人から R' に関する証人も得られる。向きが反転するのは、先行点での関係が一致条件の仮定として現れるためである。

precedes-map : (R R' : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (A x y : V ℓ)
             → ((w z : V ℓ) → ⟨ w ∈ A ⟩ → ⟨ z ∈ A ⟩ → ⟨ R' w z ⟩ → ⟨ R w z ⟩)
             → ⟨ precedes R A x y ⟩ → ⟨ precedes R' A x y ⟩
precedes-map R R' A x y f = map₁ step
  where

相違点 z、その A と y への所属、および x に属さないことは変わらない。変換が必要なのは、z より前で x と y が一致するという証明だけである。

  step : Σ[ z ∶ V ℓ ] Witness R A x y z → Σ[ z ∶ V ℓ ] Witness R' A x y z
  step (z , (z∈A , (z∈y , (z∉x , ag)))) =
    z , (z∈A , (z∈y , (z∉x , ag')))
    where
    ag' : Agrees R' A x y z

先行点 w では、仮定 R' w z をまず R w z に写し、それを元の一致証明に渡す。これにより R' に関する必要な一致が得られる。

    ag' w w∈A hR' = ag w w∈A (f w z w∈A z∈A hR')

分出条件は、候補となる関係要素だけを自由変数として受け取る。前の関係と前の段階を存在量化し、等式によって与えられた定数に固定し、二つの端点を現在の段階の中で動かす。

RelCond : (R A A' : S) → Formula S 
RelCond R A A' =
  ∃̇ ( (var zero ≐ con R)
    ∧̇ ∃̇ ( (var zero ≐ con A)
         ∧̇ ∃̇∈ (con A') ( ∃̇∈ (con A')

残る連言は、候補を二端点の順序対と同定し、与えられた直前の段階と関係に関して PrecedesAt が成り立つことを述べる。これは後で再帰ステップに使う後続段階の比較である。ただし、ここでの RelCond は直前の段階と関係を定数で固定するのに対し、再帰の論理式は関係を近似から取得し、対応する段階を階層グラフによって同定する。

              ( prAtL (sh2 (sh2 zero)) (suc zero) zero
              ∧̇ PrecedesAt (sh2 (suc zero)) (sh2 zero) (suc zero) zero ) ) ) )

ここで表現集合を再帰的に定義する。ゼロでは関係は空であり、後続では大きい方の有限段階の全要素対を含む上界から分出を始める。

opaque
  relAt : ℕ → S
  relAt     = ∅ʟ
  relAt (suc n) =
    hasSeparationL (pairsAt (suc n) .fst)

この上界から、RelCond (relAt n) (stageS n) (stageS (suc n)) は、前の関係に基づく後続節によって比較される端点の対だけを選び出す。

      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .fst

等式 relAt-zero は基底の場合を明示する。これにより、ゼロ段階の関係に属するとされる要素を、後で空集合への所属へ帰着できる。

  relAt-zero : relAt zero ≡ ∅ʟ
  relAt-zero = refl

後続段階で relAt (suc n) に属することは二つの部分からなる。候補が順序対の上界に属し、さらに relAt n、前の段階、現在の段階で定まる分出論理式を満たすことである。

  relAt-mem : (n : ℕ) (z : S)
            → (z ∈ˢ relAt (suc n))
            ≡ ( (z ∈ˢ pairsAt (suc n) .fst)
              ⊓ ((z ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n))) )
  relAt-mem n =

この同値は分出が与える正確な仕様である。後の証明では、所属から論理式を取り出す向きと、上界の証明と論理式の証明から所属を組み立てる向きの両方で用いる。

    hasSeparationL (pairsAt (suc n) .fst)
      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .snd

述語 Rel n a b は、順序対 pr a b が表現集合 relAt n に属することの略記である。続く表現補題は、段階の要素について、この述語が before n a b と同値であることを示す。

Rel : ℕ → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Rel n a b = pr a b ∈ (relAt n) .fst

これらの補題の証明では、五つの要素からなる環境で PrecedesAt を解釈する。外側の束縛による移動の後で、s1 と s2 が端点と段階の位置を指定する。

private
  s1 : Fin 
  s1 = suc zero
  s2 : Fin 
  s2 = sh2 zero

残る位置 s3 と s4 は、それぞれ前の関係と符号化された順序対を指す。これらに一度名前を付けることで、意味論的な議論を RelCond の四つの役割に対応させたままにできる。

  s3 : Fin 
  s3 = sh2 (suc zero)
  s4 : Fin 
  s4 = sh2 (sh2 zero)

関係集合の任意の要素を同定するには、その二つの成分を復元する必要がある。そこで RelOf k zv は、finiteStage k に属する x,y、zv をその順序対と同定する等式、そして before k x y の証明を要求する。この証人型は選ばれた成分を含むので、それ自体は命題とは限らない。

RelOf : (k : ℕ) → V ℓ → Type (ℓ-suc ℓ)
RelOf k zv = Σ[ x ∶ S ] Σ[ y ∶ S ]
  ( ⟨ x .fst ∈ finiteStage k ⟩
  × ( ⟨ y .fst ∈ finiteStage k ⟩
    × ( (zv ≡ pr (x .fst) (y .fst)) × ⟨ before k (x .fst) (y .fst) ⟩ ) ) )

relAt k への所属からこのような成分が得られるのは命題的切り詰めの下だけである。関係は適切な表示の存在を記録するが、その一つを標準的に選ばない。逆向きには、明示された成分とその比較から順序対を関係へ書き込める。

relAt-out : (k : ℕ) (zv : V ℓ) → ⟨ zv ∈ (relAt k) .fst ⟩ → ∥ RelOf k zv ∥₁
relAt-in  : (k : ℕ) (zv : V ℓ) → RelOf k zv → ⟨ zv ∈ (relAt k) .fst ⟩

基底の場合は before zero を反映する。relAt zero は空なので、要素があると仮定すれば矛盾が得られる。後続の場合、所属からまず分出条件が得られ、その存在証人は命題的切り詰めを通してのみ利用できる。

relAt-out  zv h = ⊥₀-rec
  (∅-empty zv (∈∈ₛ {a = zv} {b = ∅} .fst
    (subst (λ t → ⟨ zv ∈ t .fst ⟩) relAt-zero h)))
relAt-out (suc n) zv h = rec₁ squash₁
  (λ { (r , (qr , ha)) → rec₁ squash₁

切り詰められた証人を順に開くと、候補となる直前の関係、その有限段階、そして順序対の二成分が現れる。最後の再構成へこれらを渡す間も結果を切り詰めたままにするため、特定の表示が選択済みデータとして外へ出ることはない。

    (λ { (a , (qa , hx)) → rec₁ squash₁
      (λ { (x , (x∈ , hy)) → map₁ (atY r a x qr qa x∈) hy }) hx }) ha }) cond
  where
  zS : S
  zS = memS (relAt (suc n)) zv h

zv ∈ relAt (suc n) と L の推移性により、基礎集合 zv を L の要素として包める。これによって、いま調べている要素そのものにおいて対象言語の分出条件を解釈できる。

  qz : zS .fst ≡ zv
  qz = memS-fst (relAt (suc n)) zv h

分出の定義的性質により、仮定した所属は RelCond の充足へ変わる。したがって以後は、有界な順序対集合への所属だけでなく、その条件の数学的内容を用いて議論できる。

  cond : ⟨ (zS ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = subst ⟨_⟩ (relAt-mem n zS)
    (subst (λ t → ⟨ t ∈ (relAt (suc n)) .fst ⟩) (sym qz) h) .snd

候補の成分 x,y について、残る本体は二つのことを述べる。調べている要素がその順序対であることと、直前の段階上の最初の相違によって x が y に先行することである。後者はまだ r が表す関係を使う。その関係を relAt n と同定することは、外側の証人が担う。

  Body : (r a x y : S) → Type (ℓ-suc ℓ)
  Body r a x y =
      ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ prAtL s4 s1 zero ⟩
    × ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ PrecedesAt s3 s2 s1 zero ⟩

後続段階から x を選んだ後、AtY は同じ段階からの y の選択と、順序対および比較の事実を記録する。二つの選択を分けることで、RelCond の入れ子になった存在構造に対応する。

  AtY : (r a x : S) → Type (ℓ-suc ℓ)
  AtY r a x = Σ[ y ∶ S ] (⟨ y .fst ∈ (stageS (suc n)) .fst ⟩ × Body r a x y)

すべての証人がそろうと、段階の等式によって二成分はいずれも finiteStage (suc n) に属する。残るのは、調べている要素をその順序対と同定し、表された関係による比較を before (suc n) へ移すことである。続く補題がこの二つの変換を行う。

  atY : (r a x : S) → r .fst ≡ (relAt n) .fst → a .fst ≡ (stageS n) .fst
      → ⟨ x .fst ∈ (stageS (suc n)) .fst ⟩ → AtY r a x → RelOf (suc n) zv
  atY r a x qr qa x∈ (y , (y∈ , (hpr , hprec))) =
    x , (y , ( subst (λ t → ⟨ x .fst ∈ t ⟩) (stageS-fst (suc n)) x∈
             , ( subst (λ t → ⟨ y .fst ∈ t ⟩) (stageS-fst (suc n)) y∈

与えられた関係を relAt n と同定する等式により、そこに記録された任意の先行する対を Rel n として読める。これは、一般的な PrecedesAt の主張をここで構成した具体的な関係で解釈するために必要な一方向である。

               , (sym qz ∙ qpair , below) ) ) )
    where
    Rrep : (s t : S) → ⟨ pr (s .fst) (t .fst) ∈ (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) .fst ⟩
         → ⟨ Rel n (s .fst) (t .fst) ⟩
    Rrep s t p = subst (λ w → ⟨ pr (s .fst) (t .fst) ∈ w ⟩) qr p

逆向きの輸送は Rel n の証明を与えられた関係へ書き戻す。両方向がそろうことで、PrecedesAt の妥当性定理は二つの表示を同じ基底関係として扱える。

    Rfill : (s t : S) → ⟨ Rel n (s .fst) (t .fst) ⟩
          → ⟨ pr (s .fst) (t .fst) ∈ (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) .fst ⟩
    Rfill s t p = subst (λ w → ⟨ pr (s .fst) (t .fst) ∈ w ⟩) (sym qr) p

これら二つの表示写像を固定すると、Precedes モジュールが対象言語の論理式とホスト側の述語 precedes を結ぶ意味論的な橋を与える。この橋が扱うのは一回の比較だけであり、ここで順序の性質を証明するものではない。

    module P = Precedes s3 s2 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])
                        (Rel n) Rrep Rfill

PrecedesAt を読み出すと、論理式から与えられた段階上の precedes 比較が得られる。段階の等式はその台を finiteStage n と同定する。これは before (suc n) の再帰的定義が用いる台である。

    onStage : ⟨ precedes (Rel n) (finiteStage n) (x .fst) (y .fst) ⟩
    onStage = subst (λ w → ⟨ precedes (Rel n) w (x .fst) (y .fst) ⟩)
      (qa ∙ stageS-fst n) (P.PrecedesAt-out hprec)

一致の節の内部では、基底関係を使うたびに before n から relAt n への所属へ変換する必要がある。帰納的に得た書き込み補題がこの変換を行い、precedes-map からちょうど後続の関係 before (suc n) が得られる。

    below : ⟨ before (suc n) (x .fst) (y .fst) ⟩
    below = precedes-map (Rel n) (before n) (finiteStage n) (x .fst) (y .fst)
      (λ w t hw ht hb → relAt-in n (pr w t)
        (stageEl n w hw , (stageEl n t ht , (hw , (ht , (refl , hb))))))
      onStage

順序対の論理式の妥当性により、包まれた要素は pr (x .fst) (y .fst) と同定される。この等式を包装の等式と合成すると、元の zv に必要な等式が得られる。

    qpair : zS .fst ≡ pr (x .fst) (y .fst)
    qpair = subst ⟨_⟩ (prAtL-adequate s4 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) hpr

k = 0 のとき、RelOf の証人はすでに不可能な before zero の証明を含むため、書き込み方向は矛盾から従う。後続の場合、目的の順序対を有界な順序対集合へ入れ、それが分出条件を満たすことを示す。

relAt-in  zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = ⊥*-rec hb
relAt-in (suc n) zv (x , (y , (x∈ , (y∈ , (qq , hb))))) =
  subst (λ t → ⟨ t ∈ (relAt (suc n)) .fst ⟩) (prS-fst x y ∙ sym qq)
    (subst ⟨_⟩ (sym (relAt-mem n (prS x y))) (inBound , cond))
  where

二つの段階所属の仮定から、その順序対は pairsAt (suc n) に入る。これは分出に必要な境界であり、有限段階の要素からなる対だけが relAt (suc n) に入り得る。

  inBound : ⟨ prS x y ∈ˢ pairsAt (suc n) .fst ⟩
  inBound = subst (λ t → ⟨ t ∈ (pairsAt (suc n) .fst) .fst ⟩) (sym (prS-fst x y))
    (pairsAt (suc n) .snd (x .fst) (y .fst) x∈ y∈)

逆向きの構成では、環境に実際の直前の関係 relAt n が入っているため、それを Rel n と解釈する写像は恒等写像で足りる。したがって同じ意味論的な橋を使い、ホスト側の比較から PrecedesAt を構成できる。

  module P = Precedes s3 s2 s1 zero
                      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
                      (Rel n) (λ _ _ p → p) (λ _ _ p → p)

仮定 before (suc n) x y は、before n を基底とする最初の相違へ展開される。同じ一致条件を内部の関係で表すため、記録された各先行対を relAt-out で読み出す。目標の before n w t は命題なので、命題的切り詰めを除去できる。

  held : ⟨ precedes (Rel n) (finiteStage n) (x .fst) (y .fst) ⟩
  held = precedes-map (before n) (Rel n) (finiteStage n) (x .fst) (y .fst)
    (λ w t hw ht hR → rec₁ ((before n w t) .snd) (readBack w t)
      (relAt-out n (pr w t) hR))
    hb

復元された RelOf の証人は w,t とは別の成分を名指すかもしれないが、その順序対の等式は pr w t と等しいことを述べる。順序対の単射性が二成分をそれぞれ同定し、記録された before n の証明を必要な端点へ移せる。

    where
    readBack : (w t : V ℓ) → RelOf n (pr w t) → ⟨ before n w t ⟩
    readBack w t (p , (q , (p∈ , (q∈ , (qq' , hbf))))) =
      subst2 (λ s u → ⟨ before n s u ⟩)
        (sym (pr-inj qq' .fst)) (sym (pr-inj qq' .snd)) hbf

変換されたホスト側の比較は PrecedesAt-in の仮定を満たす。これにより、直前の段階と関係を所定の変数に置いた分出論理式の比較節が得られる。

  hprec : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
          ⊨ PrecedesAt s3 s2 s1 zero ⟩
  hprec = P.PrecedesAt-in
    (subst (λ w → ⟨ precedes (Rel n) w (x .fst) (y .fst) ⟩) (sym (stageS-fst n))
      held)

候補の要素は prS x y として構成されているため、順序対を認識する論理式を満たす。その妥当性の等式が、内部の構成を論理式の要求する基礎の順序対へ結び付ける。

  hpr : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) ⊨ prAtL s4 s1 zero ⟩
  hpr = subst ⟨_⟩
    (sym (prAtL-adequate s4 s1 zero
      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []))) (prS-fst x y)

stageS (suc n) の表示等式により、finiteStage (suc n) の既知の各要素を論理式が用いる段階対象へ輸送できる。追加の閉包性は必要ない。

  onStage : (w : V ℓ) → ⟨ w ∈ finiteStage (suc n) ⟩
          → ⟨ w ∈ (stageS (suc n)) .fst ⟩
  onStage w hw = subst (λ t → ⟨ w ∈ t ⟩) (sym (stageS-fst (suc n))) hw

ここまでに構成した証人は分出条件全体を満たす。直前の関係と段階を同定し、x,y を後続段階に置き、順序対と最初の相違の両方を確立する。入れ子の存在量化は命題的切り詰めの下で導入され、存在を主張するだけで標準的な証人を選ばない。

  cond : ⟨ (prS x y ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = ∣ relAt n , (refl
       , ∣ stageS n , (refl
       , ∣ x , (onStage (x .fst) x∈
       , ∣ y , (onStage (y .fst) y∈ , (hpr , hprec)) ∣₁) ∣₁) ∣₁) ∣₁

実用的な読み出しのインターフェースは、両端点が finiteStage n に属すると分かっている順序対 pr u v から始まる。切り詰められた表示を除去する先は命題 before n u v だけなので、標準的な表示がなくても問題はない。

relAt-rep : (n : ℕ) (u v : V ℓ)
          → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
          → ⟨ pr u v ∈ (relAt n) .fst ⟩ → ⟨ before n u v ⟩
relAt-rep n u v hu hv h = rec₁ ((before n u v) .snd) read (relAt-out n (pr u v) h)
  where

復元した表示が成分 p,q を用いていても、その順序対が pr u v と等しいことから p=u と q=v が従う。この二つの等式に沿って輸送すれば、記録された比較が目的の比較になる。

  read : RelOf n (pr u v) → ⟨ before n u v ⟩
  read (p , (q , (p∈ , (q∈ , (qq , hbf))))) =
    subst2 (λ s t → ⟨ before n s t ⟩)
      (sym (pr-inj qq .fst)) (sym (pr-inj qq .snd)) hbf

逆に、u,v の段階所属と before n u v の証明から、pr u v に対する明示的な RelOf の証人が得られる。書き込み補題がその対を relAt n に記録し、対ごとの表示の逆方向が完成する。

relAt-fill : (n : ℕ) (u v : V ℓ)
           → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
           → ⟨ before n u v ⟩ → ⟨ pr u v ∈ (relAt n) .fst ⟩
relAt-fill n u v hu hv h = relAt-in n (pr u v)
  (stageEl n u hu , (stageEl n v hv , (hu , (hv , (refl , h)))))

参照対象すべてに一般的なステップ

再帰的な記述は関係をデータとして受け取る必要があり、relAt を直接参照できない。Held r a b が必要な解釈を与える。すなわち、r が a,b の順序対を含むとき、かつそのときに限り、r は a を b に関係付ける。

Held : S → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Held r a b = pr a b ∈ r .fst

一回の再帰ステップでは、まず現在の添字の ∈ に関する最大要素 c を探する。その添字が後続数項 # (suc n) なら、この要素は直前の数項 # n である。零ではそのような要素が存在しないため、別の基底論理式を置かなくても、ステップが定める関係には要素がない。

opaque
 RelBodyAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
 RelBodyAt z b f =
   ∃̇ ( (var zero ∈̇ var (suc b))
     ∧̇ ( ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero))

c が得られると、論理式は近似から c に記録された関係を読み取る。階層のグラフは Lset (c .fst) と現在の添字における Lset を同定し、二つの候補となる端点は後者の中を動く。現在の添字が数項と同定されたときに限って、これらは有限段階になる。

       ∧̇ ∃̇ ( appAt (sh2 f) (suc zero) zero
            ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero))
                 ∧̇ ∃̇ ( LsetGraphAt zero (sh4 b)
                      ∧̇ ∃̇∈ (var zero)
                           ( ∃̇∈ (var (suc zero))

最も内側の節は、候補の項目が二端点の順序対であることを要求し、近似から読み出した関係を使って、直前の段階上で PrecedesAt により両者を比較する。こうして、特定の relAt n を名指すことなく再帰の後続ステップを記述する。

                               ( prAtL (sh6 z) (suc zero) zero
                               ∧̇ PrecedesAt (suc (suc (suc (suc zero))))
                                             (suc (suc (suc zero)))
                                             (suc zero) zero ) ) ) ) ) ) )

StepOf はこの論理式のメタレベルでの意味である。現在の添字の最大要素となる候補 c、そこで記録された関係値 r、端点 x,y という四つのモデル要素を選ぶ。候補となる項目 zv は、すでに述語の引数である。現在の添字が数項と同定されて初めて、c はその直前の数項と同定される。

StepOf : ∀ {n} → Fin n → Fin n → Vec S n → V ℓ → Type (ℓ-suc ℓ)
StepOf b f γ zv =
  Σ[ c ∶ S ] Σ[ r ∶ S ] Σ[ x ∶ S ] Σ[ y ∶ S ]
    ( ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    × ( ((d : S) → ⟨ d .fst ∈ (lookup b γ) .fst ⟩ → ⟨ c .fst ∈ d .fst ⟩ → ⊥₀)

付随する条件は、c が現在の添字に属してそこで ∈ に関する最大要素であること、近似が c で r を記録すること、二端点が現在の値で添字づけられた階層の段階に属すること、zv がその順序対であること、そして precedes (Held r) が Lset (c .fst) 上で二端点を比較することを述べる。これは一回の再帰ステップに必要な数学的データであり、有限性は後で数項の等式から得られる。

      × ( ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
        × ( ⟨ x .fst ∈ Lset ((lookup b γ) .fst) ⟩
          × ( ⟨ y .fst ∈ Lset ((lookup b γ) .fst) ⟩
            × ( (zv ≡ pr (x .fst) (y .fst))
              × ⟨ precedes (Held r) (Lset (c .fst)) (x .fst) (y .fst) ⟩ ) ) ) ) ) )

ここから、任意の変数 z,b,f と任意の環境について意味論的な対応を示す。lookup b γ の台となる集合が順序数であるという仮定は、階層グラフが記述する段階を対応する Lset の値と同定するために使われる。

module _ {n : ℕ} (z b f : Fin n) (γ : Vec S n)
         (ob : IsOrd ((lookup b γ) .fst)) where

private
  Body : (c r A A' x y : S) → Type (ℓ-suc ℓ)
  Body c r A A' x y =

      ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
    × ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
        ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                     (suc zero) zero ⟩

  AtY : (c r A A' x : S) → Type (ℓ-suc ℓ)
  AtY c r A A' x = Σ[ y ∶ S ] (⟨ y .fst ∈ A' .fst ⟩ × Body c r A A' x y)

  MaxOf : (c : S) → Type (ℓ-suc ℓ)
  MaxOf c = (d : S) → ⟨ d .fst ∈ (lookup b γ) .fst ⟩ → ⟨ c .fst ∈ d .fst ⟩
          → ⊥₀

  atY : (c r A A' x : S) → ⟨ c .fst ∈ (lookup b γ) .fst ⟩ → MaxOf c
      → ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
      → A .fst ≡ Lset (c .fst) → A' .fst ≡ Lset ((lookup b γ) .fst)
      → ⟨ x .fst ∈ A' .fst ⟩
      → AtY c r A A' x → StepOf b f γ ((lookup z γ) .fst)

  atY c r A A' x c∈ cmax hf qA qA' x∈ (y , (y∈ , (hpr , hprec))) =
    c , (r , (x , (y , (c∈ , (cmax , (hf
      , ( subst (λ t → ⟨ x .fst ∈ t ⟩) qA' x∈
        , ( subst (λ t → ⟨ y .fst ∈ t ⟩) qA' y∈
          , (qpair , hprec') ) ) ) ) ) ) ) )

    where
    module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                        (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                        (Held r) (λ _ _ p → p) (λ _ _ p → p)

    hprec' : ⟨ precedes (Held r) (Lset (c .fst)) (x .fst) (y .fst) ⟩
    hprec' = subst (λ t → ⟨ precedes (Held r) t (x .fst) (y .fst) ⟩) qA
      (P.PrecedesAt-out hprec)

    qpair : (lookup z γ) .fst ≡ pr (x .fst) (y .fst)
    qpair = subst ⟨_⟩
      (prAtL-adequate (sh6 z) (suc zero) zero
        (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) hpr

  AtX : (c r A A' : S) → Type (ℓ-suc ℓ)
  AtX c r A A' = Σ[ x ∶ S ] (⟨ x .fst ∈ A' .fst ⟩ × ∥ AtY c r A A' x ∥₁)

  atX : (c r A A' : S) → ⟨ c .fst ∈ (lookup b γ) .fst ⟩ → MaxOf c
      → ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
      → A .fst ≡ Lset (c .fst) → A' .fst ≡ Lset ((lookup b γ) .fst)
      → AtX c r A A' → ∥ StepOf b f γ ((lookup z γ) .fst) ∥₁
  atX c r A A' c∈ cmax hf qA qA' (x , (x∈ , hy)) =

    map₁ (atY c r A A' x c∈ cmax hf qA qA' x∈) hy

  AtA' : (c r A : S) → Type (ℓ-suc ℓ)
  AtA' c r A = Σ[ A' ∶ S ]
    ( ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
    × ∥ AtX c r A A' ∥₁ )

  atA' : (c r A : S) → ⟨ c .fst ∈ (lookup b γ) .fst ⟩ → MaxOf c
       → ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
       → A .fst ≡ Lset (c .fst)
       → AtA' c r A → ∥ StepOf b f γ ((lookup z γ) .fst) ∥₁
  atA' c r A c∈ cmax hf qA (A' , (hg , hx)) =

    rec₁ squash₁ (atX c r A A' c∈ cmax hf qA qA') hx
    where
    qA' : A' .fst ≡ Lset ((lookup b γ) .fst)
    qA' = Lset-only zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) hg ob

  AtA : (c r : S) → Type (ℓ-suc ℓ)
  AtA c r = Σ[ A ∶ S ]
    ( ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
    × ∥ AtA' c r A ∥₁ )

  atA : (c r : S) → ⟨ c .fst ∈ (lookup b γ) .fst ⟩ → MaxOf c
      → ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
      → AtA c r → ∥ StepOf b f γ ((lookup z γ) .fst) ∥₁
  atA c r c∈ cmax hf (A , (hg , hA')) =
    rec₁ squash₁ (atA' c r A c∈ cmax hf qA) hA'

    where
    qA : A .fst ≡ Lset (c .fst)
    qA = Lset-only zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) hg
      (mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈)