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

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

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

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

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

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ¬̇_; ∃̇_; ∀̇∈; ∃̇∈ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )

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

open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using
  ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; mem-ord; boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

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

open import L.Axioms.Basic {ℓ}
  using ( extensionalL; LsetS; ∅ʟ; finSet; finSet-in; finSet-out; module FinOf )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL )
open import L.Recursion {ℓ} lem using ( smallDom; mereFunct )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )

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

open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( before; precedes; Agrees; Witness; finiteStage )
open import L.Choice.LimitStageOrder {ℓ} lem
  using ( PrecedesAt; module Precedes; module Described )
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt; module RecShape )

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

open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; appC; appC-adequate; domAt-intro )
open import L.Coding.Expressions {ℓ} using ( numL; extAt; extAt-out; extAt-in; extAt-in-both )

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

import FOL.Absoluteness
import FOL.ZFModel
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
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.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.FinData.Properties using ( toℕ<n; enum; toℕ∘enum )

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

open import Cubical.Data.FinData.Base using ( toℕ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
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 hPropStructure 𝒮ʟ

台 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 : ℕ) → fst (stageS n) ≡ finiteStage n
  stageS-fst n = refl

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

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

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

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

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

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

memS A z h の第一成分は元の集合 z のままであり、追加された成分は L への所属証明だけを与える。

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

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

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

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

  prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b)
  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 ∈ fst D ⟩)
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 (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
  d = smallDom (⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
        (λ p → prʟ (ixL (fst p)) (ixL (snd p)))

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

  onPair : (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
         → ⟨ pr u v ∈ fst (d .fst) ⟩
  onPair u v hu hv = subst (λ t → ⟨ t ∈ fst (d .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 = PT.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 zero    = ∅ʟ
  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 ∈ fst (relAt n)

これらの補題の証明では、五つの要素からなる環境で 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 ]
  ( ⟨ fst x ∈ finiteStage k ⟩
  × ( ⟨ fst y ∈ finiteStage k ⟩
    × ( (zv ≡ pr (fst x) (fst y)) × ⟨ before k (fst x) (fst y) ⟩ ) ) )

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

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

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

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

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

    (λ { (a , (qa , hx)) → PT.rec squash₁
      (λ { (x , (x∈ , hy)) → PT.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 : fst zS ≡ 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 ∈ fst (relAt (suc n)) ⟩) (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 ] (⟨ fst y ∈ fst (stageS (suc n)) ⟩ × Body r a x y)

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

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

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

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

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

    Rfill : (s t : S) → ⟨ Rel n (fst s) (fst t) ⟩
          → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
    Rfill s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ 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) (fst x) (fst y) ⟩
    onStage = subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩)
      (qa ∙ stageS-fst n) (P.PrecedesAt-out hprec)

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

    below : ⟨ before (suc n) (fst x) (fst y) ⟩
    below = precedes-map (Rel n) (before n) (finiteStage n) (fst x) (fst y)
      (λ 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 (fst x) (fst y) と同定されます。この等式を包装の等式と合成すると、元の zv に必要な等式が得られます。

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

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

relAt-in zero zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = Empty.rec* hb
relAt-in (suc n) zv (x , (y , (x∈ , (y∈ , (qq , hb))))) =
  subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (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 ∈ fst (pairsAt (suc n) .fst) ⟩) (sym (prS-fst x y))
    (pairsAt (suc n) .snd (fst x) (fst y) 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) (fst x) (fst y) ⟩
  held = precedes-map (before n) (Rel n) (finiteStage n) (fst x) (fst y)
    (λ w t hw ht hR → PT.rec (snd (before n w t)) (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 (fst x) (fst y) ⟩) (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 ∈ fst (stageS (suc n)) ⟩
  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 (fst x) x∈
       , ∣ y , (onStage (fst y) 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 ∈ fst (relAt n) ⟩ → ⟨ before n u v ⟩
relAt-rep n u v hu hv h = PT.rec (snd (before n u v)) 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 ∈ fst (relAt n) ⟩
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 ∈ fst r

一回の再帰ステップでは、まず現在の添字の ∈ に関する最大要素 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 (fst c) と現在の添字における 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 → S ^ n → V ℓ → Type (ℓ-suc ℓ)
StepOf b f γ zv =
  Σ[ c ∈ S ] Σ[ r ∈ S ] Σ[ x ∈ S ] Σ[ y ∈ S ]
    ( ⟨ fst c ∈ fst (lookup b γ) ⟩
    × ( ((d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥)

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

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

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

module _ {n : ℕ} (z b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  private
    Body : (c r A A' x y : S) → Type (ℓ-suc ℓ)
    Body c r A A' x y =

六つの存在証人が環境を拡張した後、最も内側の本体には二つの決定的な事実が残ります。z が指す値が x,y の順序対であることと、復元された段階と関係について二端点が PrecedesAt を満たすことです。

        ⟨ (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 ⟩

第一の端点 x を固定すると、AtY は残る端点 y、その現在の段階への所属、そして最も内側の二つの事実をまとめます。この型は、論理式の入れ子になった存在の読みの一層に対応します。

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

MaxOf c は所属順序での最大性を表します。d も現在の添字に属するなら、c ∈ d は不可能です。c 自身が添字に属することと合わせると、c は所属順序で最大になります。後続数項では直前の数項であり、零では c の所属という前提の時点ですでに証人がありません。

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

論理式の証人を StepOf へ変換するため、c の所属と最大性、近似の項目 (c,r)、直前および現在の段階を同定する等式、そして x の現在の段階への所属を仮定します。最後の AtY の証人が y と二つの内側の事実を与えます。

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

段階の等式は、論理式における x,y の所属を Lset (lookup b γ) への所属へ変換し、StepOf の要求に合わせます。順序対の等式とホスト側の precedes 比較は、続く二つの妥当性の議論から得られます。

    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 → ⟨ fst x ∈ t ⟩) qA' x∈
          , ( subst (λ t → ⟨ fst y ∈ t ⟩) qA' y∈
            , (qpair , hprec') ) ) ) ) ) ) ) )

ここでは関係変数を直接 Held r と解釈するため、二つの表示写像は恒等写像です。したがって Precedes の橋は、すでに構成した relAt の族に頼らずに対象言語の比較を読み出せます。

      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)

PrecedesAt を読み出すと、論理式で束縛された段階対象上の比較が得られます。その段階を同定する等式によって台を Lset (fst c) へ輸送すると、ちょうど StepOf が要求する比較になります。

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

prAtL の妥当性により、z が指す値は復元された二端点の順序対と同定されます。これがメタレベルのステップ証人に必要な順序対の等式です。

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

第一の端点 x を取り出した後も、残る端点は命題的に存在することしか分かりません。AtX はこの中間状態、すなわち x の段階所属と命題的に切り詰められた AtY の証人を記録します。

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

目的の結論自体も命題的に切り詰められているため、隠された y の証人を命題の外で選ぶことなく利用できます。その切り詰めの上で各点の変換を写すことで、論理式が与える存在の強さをそのまま保ちます。

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

内側の変換は復元したデータから明示的な StepOf の証人を一つ組み立て、PT.map がそれを命題的切り詰めの下へ戻します。これで、標準的な直前要素や端点の証人を作ることなく、外向きの意味論的な読みが完了します。

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

c が添字づける段階を復元した後、残る内側の量化は現在の添字が指す段階を同定します。AtA' は、構成可能集合 A'、それがそこで段階のグラフを満たす証拠、さらに内側にある証人 x と y の命題的に切り詰められた存在をまとめます。この切り詰めは証人の存在を保ちますが、特定の証人の対を選びません。

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

A' から先へ進むため、論証はすでに得られた c の情報、表の項目 (c,r)、そして A と c が添字づける段階との同一視を保ちます。AtX に隠された証人を意味論的な一ステップとして解釈するには、その前に A' を現在の順序数添字が指す段階と同定しなければなりません。

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

段階のグラフが、まさにこの同一視を与えます。その関数性定理 Lset-only に添字の順序数性を適用すると、fst A' ≡ Lset (fst (lookup b γ)) が得られます。そこで、命題的に切り詰められた AtX を、命題的に切り詰められたステップの結論へ除去できます。

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

量化を一つ外へ戻ると、AtA は c が添字づける段階について同じ役割を果たします。これは、対応する段階のグラフを満たす構成可能集合 A と、続きとなる AtA' の命題的に切り詰められた存在からなります。

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

この層を解釈するには、まず A がどの段階であるかを示す等式が必要です。その等式が得られれば、内側の層と同様に、切り詰められた続きから切り詰められたステップへ除去できます。

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

c は b が指す順序数に属するので、mem-ord により c 自身も順序数です。この順序数における段階のグラフの関数性から、fst A ≡ Lset (fst c) が得られます。この同定に段階の単調性は使いません。

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

さらに外側の証人は、近似表が c に記録する関係です。AtR は、構成可能集合 r、表が項目 (c,r) を含むことを述べる適用論理式の充足、そして必要な二つの段階を復元する続きの命題的切り詰めを記録します。

    AtR : (c : S) → Type (ℓ-suc ℓ)
    AtR c = Σ[ r ∈ S ]
      ( ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ × ∥ AtA c r ∥₁ )

appAt の妥当性は、その充足判断を順序対 (c,r) についての周囲の所属命題へ変換します。この表の項目が得られると、命題的に切り詰められた AtA の続きから、命題的に切り詰められた意味論的ステップへ除去できます。

    atR : (c : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → AtR c → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atR c c∈ cmax (r , (happ , hA)) = PT.rec squash₁ (atA c r c∈ cmax hf) hA
      where
      hf : ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩

具体的に復元される事実は、pr (fst c) (fst r) ∈ fst (lookup f γ) です。これは StepOf が必要とするメタレベルの形であり、f が指す近似が添字 c に関係 r を割り当てることを表します。

      hf = subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) happ

最も外側で、AtC は順序数添字の要素 c を選び、その添字には c ∈ d を満たす要素 d がないと主張します。したがって c は所属関係に関する添字の極大要素です。後で添字が非零のフォン・ノイマン数項と同定されると、この条件がその直前の数項を同定します。残る命題的に切り詰められた成分は、関係と段階のデータを供給します。

    AtC : Type (ℓ-suc ℓ)
    AtC = Σ[ c ∈ S ]
      ( ⟨ fst c ∈ fst (lookup b γ) ⟩
      × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
        × ∥ AtR c ∥₁ ) )

論理式の有界否定は持ち上げられた宇宙で解釈されます。それを降ろすと通常の関数 MaxOf c が得られ、添字に属しかつ c ∈ d を満たすとされる任意の d から矛盾を導けます。すると、切り詰められた関係の証人を先ほどの各層を通して除去できます。

    atC : AtC → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atC (c , (c∈ , (hmax , hr))) = PT.rec squash₁ (atR c c∈ cmax) hr
      where
      cmax : MaxOf c
      cmax d hd hc = lower (hmax d hd hc)

これらの入れ子になった解釈により、ステップ本体を読み出す向きが得られます。逆向きには、同じ本体の論理式を局所的に展開し、明示的な StepOf の証人を存在節と有界節へ戻します。

  opaque
   unfolding RelBodyAt

RelBodyAt の充足から始めると、最外側の存在量化が与えるのは c の命題的に切り詰められた存在だけです。各層の読みは同じ制限のもとで残りのデータを復元し、最後に ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ を得ます。これはステップの存在を示しますが、入れ子の量化に対する標準的な証人を選びません。

   RelBody-out : ⟨ γ ⊨ RelBodyAt z b f ⟩
               → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
   RelBody-out = PT.rec squash₁ atC

逆に、明示的な StepOf の証人は、c、関係 r、比較される対象 x,y、それらの段階への所属、順序対の等式、直前の段階での比較をすでに含みます。RelBody-in は二つの中間段階を再構成し、このデータを入れ子の論理式へ入れます。存在節は命題的に切り詰められるため、結論は充足を主張しますが、内部の証人からなる標準的な組を保存しません。

   RelBody-in : StepOf b f γ (fst (lookup z γ)) → ⟨ γ ⊨ RelBodyAt z b f ⟩
   RelBody-in (c , (r , (x , (y , (c∈ , (cmax , (hf , (x∈ , (y∈
              , (qpair , hprec))))))))))
     = ∣ c , (c∈ , (hmax , ∣ r , (happ , ∣ A , (hgA , ∣ A' , (hgA'
       , ∣ x , (x∈ , ∣ y , (y∈ , (hpr , hprec')) ∣₁) ∣₁) ∣₁) ∣₁) ∣₁)) ∣₁

最初に再構成する事実は、c が順序数だということです。順序数の各要素は順序数なので、これは c ∈ fst (lookup b γ) とその集合の順序数性から従います。また、c を添字とする構成可能段階を作るためにちょうど必要な条件でもあります。

     where
     oc : IsOrd (fst c)
     oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈

この順序数性を用いて、LsetS は Lset (fst c) を模型の要素 A としてまとめます。最初の相違による比較は、この直前の添字が指す段階で評価されます。

     A : S
     A = LsetS (fst c) oc

現在の添字について仮定した順序数性から、同様に Lset (fst (lookup b γ)) を A' としてまとめます。この二つ目の段階が、順序対として現在の関係の要素になる二対象を含む集合の上界を与えます。

     A' : S
     A' = LsetS (fst (lookup b γ)) ob

次に、意味論的な極大性の関数を対象言語の有界全称否定で表します。添字に属する各 d について、c ∈ d の証明は cmax によって矛盾へ送られ、さらに論理式の充足が属する宇宙へ持ち上げられます。

     hmax : ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
     hmax d hd hc = lift (cmax d hd hc)

StepOf の表の項目は、pr (fst c) (fst r) ∈ fst (lookup f γ) という周囲の形をしています。appAt の妥当性を与える経路の逆向きに沿ってこの事実を輸送すると、本体の論理式が必要とする適用原子の充足になります。

     happ : ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩
     happ = subst ⟨_⟩
       (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) hf

選んだ A は定義により c が添字づける段階です。したがって階層の表示定理は、c の順序数性と表される値の反射律から、対応する段階グラフの節を証明します。

     hgA : ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
     hgA = Lset-defines zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) oc refl

同じ表示定理が、今度は現在の添字で A' のグラフ節を証明します。必要な順序数性は仮定 ob そのものなので、論理式は A' を x と y を含む段階として正確に認識します。

     hgA' : ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
     hgA' = Lset-defines zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) ob refl

StepOf の等式は、z が指す候補値を x と y の Kuratowski 対と同定します。prAtL の妥当性を与える経路の逆向きに沿う輸送により、この等式を対象言語の対形成節の充足へ変換します。

     hpr : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
     hpr = subst ⟨_⟩
       (sym (prAtL-adequate (sh6 z) (suc zero) zero
         (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ))) qpair

残るのは、直前の段階における比較の翻訳です。ここでの Precedes のインスタンスは基底関係を Held r、すなわち順序対が r に属するという命題として解釈します。この解釈は対象言語の適用論理式が求める所属命題とすでに同じなので、二つの表現写像はいずれも恒等関数です。

     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)

この解釈を固定すると、PrecedesAt-in は StepOf がもつ意味論的な最初の相違による比較を PrecedesAt の充足へ変換します。これで RelBodyAt のすべての節が満たされ、意味論的ステップから対象言語の論理式へ戻る橋が完成します。

     hprec' : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
              ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                           (suc zero) zero ⟩
     hprec' = P.PrecedesAt-in hprec

ここまでの本体は一つの候補となる順序対を分類するだけです。一つの関係値はそのような候補をちょうどすべて集めなければならないため、次の構成ではこの一ステップの条件を集合全体へ外延的に拡張します。

近似とグラフ

RelStepAt v b f は、v が指す集合の要素が RelBodyAt を満たす対象とちょうど一致することを述べます。候補は新しい零番の変数に束縛され、添字 b,f はその束縛子の下で移動します。したがって二つの包含が得られます。候補関係の各要素は意味論的ステップを実現し、そのようなステップを実現する各対象は候補関係に属します。

opaque
  RelStepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  RelStepAt v b f = extAt v (RelBodyAt zero (suc b) (suc f))

fst (lookup b γ) が順序数であれば、この外延的記述の読みが成り立ちます。本体の論理式は、ステップの証人に現れる二つの構成可能段階を同定するためにこの仮定を使います。

module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  opaque
   unfolding RelStepAt

順向きの包含は、v が指す集合の要素 w から出発し、w における本体の論理式を読み、∥ StepOf b f γ (fst w) ∥₁ を得ます。本体は存在量化によって直前の添字、記録された関係、比較される成分を見つけるため、結果は命題的に切り詰められています。

   RelStep-out : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S)
               → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁
   RelStep-out h w hw = RelBody-out zero (suc b) (suc f) (w ∷ γ) ob
     (extAt-out v (RelBodyAt zero (suc b) (suc f)) γ h w hw)

逆向きの包含は、w に対する明示的な意味論的ステップから始めます。RelBody-in がそれを本体の充足へ変換し、外延的記述の逆向きの含意から w が v の指す集合に属することが従います。

   RelStep-back : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S) → StepOf b f γ (fst w)
                → ⟨ fst w ∈ fst (lookup v γ) ⟩
   RelStep-back h w s = extAt-in v (RelBodyAt zero (suc b) (suc f)) γ h w
     (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob s)

導入原理はその正確な逆を述べます。RelStepAt を証明するには、候補関係の各要素に対して命題的に切り詰められたステップを与え、各明示的ステップ証人に対して所属を証明すれば十分です。この二つの関数が外延性の二つの包含です。

   RelStep-in : ((w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩
                 → ∥ StepOf b f γ (fst w) ∥₁)
              → ((w : S) → StepOf b f γ (fst w)
                 → ⟨ fst w ∈ fst (lookup v γ) ⟩)
              → ⟨ γ ⊨ RelStepAt v b f ⟩

第一の包含では、命題的に切り詰められた各ステップを RelBody-in で写し、命題である充足判断へ除去します。第二の包含では、RelBody-out が命題的に切り詰められたステップを生み、それを与えられた逆向きの関数に渡して、命題である所属判断へ除去します。命題的切り詰めを除去できるのは、どちらの目標も命題だからです。

   RelStep-in into back = extAt-in-both v (RelBodyAt zero (suc b) (suc f)) γ
     (λ w hw → PT.rec (snd ((w ∷ γ) ⊨ RelBodyAt zero (suc b) (suc f)))
       (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob) (into w hw))
     (λ w h → PT.rec (snd (fst w ∈ fst (lookup v γ))) (back w)
       (RelBody-out zero (suc b) (suc f) (w ∷ γ) ob h))

この外延的ステップによって、一般的な再帰形状の構成を具体化します。得られる ApproxAt は、添字より前の部分を定義域とし、各点でのステップ節が RelStepAt に従う表を記述します。RelGraphAt は、その近似に支えられた現在の添字での値を記述します。後で添字を数項と同定したとき、この表は有限になります。

module A = RecShape RelStepAt
open A using ( ApproxAt; ApproxAt-value; ApproxAt-step
             ; ApproxAt-in; GraphOf; PairOf )
     renaming ( GraphAt to RelGraphAt; Graph-in to RelGraph-in
              ; Graph-out to RelGraph-out; PairGraphAt to PairRelGraphAt

同じ構成は、近似のグラフとその対にした形についての導入原理と除去原理も与えます。局所名 RelGraphAt と PairRelGraphAt は、この一般的な仕組みがここでは再帰的に定義された関係値に用いられることを示します。

              ; PairGraph-in to PairRelGraph-in
              ; PairGraph-out to PairRelGraph-out )

ここまでの論理式は再帰の形を記述するだけで、その値をまだ同定していません。次の課題は、この形を満たす任意の表が、先に構成した集合 relAt m を正確に記録することを示すことです。そのため、記録された値の正しさと標準的な項目の存在を分けて扱います。

再帰に対するステップ

Values g k は正しさの条件です。各 m < k について、g が # m と任意の模型要素 w を組にした項目を含むなら、w の台集合は relAt m の台集合に等しくなります。これは、すでに記録された添字における集合値の一意性を述べますが、一意な証明や証人の組を選ぶものではありません。

Values : S → ℕ → Type (ℓ-suc ℓ)
Values g k = (m : ℕ) → m < k → (w : S)
           → ⟨ pr (# m) (fst w) ∈ fst g ⟩ → fst w ≡ fst (relAt m)

Entries g k はそれを補う完全性の条件です。各 m < k について、標準的な項目 (# m, relAt m) が g に現れることを要求します。Values と Entries を合わせると、表がすべての小さい添字をもち、その各添字で意図した集合値だけを記録することが分かります。

Entries : S → ℕ → Type (ℓ-suc ℓ)
Entries g k = (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst g ⟩

比較 before k x y が成り立つなら、k は後続数です。零では関係が空なので比較から矛盾が従い、suc m では直前の数 m と必要な等式がただちに得られます。この補題により、後で relAt k の要素を StepOf が必要とする直前の数のデータへ戻せます。

before-suc : (k : ℕ) (x y : V ℓ) → ⟨ before k x y ⟩ → Σ[ m ∈ ℕ ] (k ≡ suc m)
before-suc zero    x y h = Empty.rec* h
before-suc (suc m) x y h = m , refl

v が指す候補関係、b が指す添字、f が指す表を固定します。等式 qb は添字を数項 # k と同定し、vals と ents は表が k より下で正しく完全であることを主張します。これらの仮定のもとで、添字における意味論的ステップを relAt k への所属と正確に比較できます。

module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (k : ℕ)
         (qb : fst (lookup b γ) ≡ # k)
         (vals : Values (lookup f γ) k) (ents : Entries (lookup f γ) k) where
  private
    ob : IsOrd (fst (lookup b γ))

数項 # k は順序数です。この事実を qb : fst (lookup b γ) ≡ # k に沿って逆向きに輸送すると、fst (lookup b γ) が順序数であることが分かり、先に得たステップ本体の読みと書き入れの補題を使えるようになります。

    ob = subst IsOrd (sym qb) (numeral-ord k)

候補値 x に対する明示的な StepOf の証人を考えます。その極大要素 c は添字に属し、qb によって fst c ∈ # k と読み替えられます。数項への所属を除去すると、命題的切り詰めのもとで自然数 m < k と等式 fst c ≡ # m が復元されます。ここで切り詰めを除去できるのは、目標の所属 x ∈ relAt k が命題だからです。

    into : (x : V ℓ) → StepOf b f γ x → ⟨ x ∈ fst (relAt k) ⟩
    into x (c , (r , (xx , (yy , (c∈ , (cmax , (hf , (xx∈ , (yy∈
           , (qx , hprec)))))))))) =
      PT.rec (snd (x ∈ fst (relAt k))) atC
        (∈#-elim k (fst c) (subst (λ t → ⟨ fst c ∈ t ⟩) qb c∈))

このような m に対しては、relAt k の導入補題により必要な所属を証明します。対応する RelOf k x の証人は、同じ成分 xx と yy、それらの finiteStage k への所属、x をその順序対と同定する等式、そして比較 before k xx yy を用います。したがって残る仕事は、極大要素 c が実際に k の直前の数に対応することを示し、それに従って表に記録された比較を翻訳することです。

      where
      atC : Σ[ m ∈ ℕ ] ((m < k) × (fst c ≡ # m)) → ⟨ x ∈ fst (relAt k) ⟩
      atC (m , (hm , qc)) = relAt-in k x
        (xx , (yy , (xxk , (yyk , (qx , below)))))
        where

c は # m によって符号化され、しかも # k の要素の中で極大なので、k = suc m でなければなりません。三分律で suc m と k を比較すると、等しい場合には求める等式が得られ、二つの狭義不等号の場合は、それぞれ既知の m と k の関係または極大性に矛盾します。

        ksuc : k ≡ suc m
        ksuc = decide (suc m ≟ k)
          where
          decide : NatOrder.Trichotomy (suc m) k → k ≡ suc m
          decide (NatOrder.lt hlt) = Empty.rec

もし suc m < k なら、数項 #(suc m) 自身が # k に属します。また c = # m なので、c ∈ #(suc m) でもあります。この二つの所属は、添字の中に c より真に大きい要素があることを示し、極大性の節に矛盾します。

            (cmax (numS (suc m))
              (subst (λ t → ⟨ fst (numS (suc m)) ∈ t ⟩) (sym qb)
                (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst (suc m)))
                  (#mono (suc m) k hlt)))
              (subst (λ t → ⟨ fst c ∈ t ⟩) (sym (numS-fst (suc m)))

反対に k < suc m なら、後続を外すことで k ≤ m が得られ、既知の m < k と両立しません。したがって等しい場合だけが残り、三分律から得た等式を反転すると、以下で必要な向きの k ≡ suc m が得られます。

                (subst (λ t → ⟨ t ∈ # (suc m) ⟩) (sym qc)
                  (#mono m (suc m) NatOrder.≤-refl))))
          decide (NatOrder.eq e) = sym e
          decide (NatOrder.gt hgt) = Empty.rec (<-asym hm (pred-≤-pred hgt))

ステップの証人はすでに、xx が Lset (fst (lookup b γ)) に属することを与えています。qb に沿って輸送すると、この集合は Lset (# k)、すなわち finiteStage k と同定され、RelOf k x が必要とする第一の段階所属の成分が得られます。

        xxk : ⟨ fst xx ∈ finiteStage k ⟩
        xxk = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) qb xx∈

順序対の二つの端点は、いずれも k で添字づけられた段階に属さなければならない。第二の端点については、上界を # k と同一視する等式により、Lset (fst (lookup b γ)) への所属を finiteStage k への所属に移す。

        yyk : ⟨ fst yy ∈ finiteStage k ⟩
        yyk = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) qb yy∈

前者の数項で添字づけられた表の項目は、関係 r を記録している。第一成分を fst c から # m に移すと、正しさの仮定 vals によって r の台集合が relAt m と同一視される。

        rval : fst r ≡ fst (relAt m)
        rval = vals m hm r
          (subst (λ t → ⟨ pr t (fst r) ∈ fst (lookup f γ) ⟩) qc hf)

ステップの証人は初め、Lset (fst c) 上で r が保持する関係を用いて二つの端点を比較する。等式 fst c ≡ # m と fst r ≡ fst (relAt m) により、これは precedes (Rel m) (finiteStage m) に書き換えられる。

        atM : ⟨ precedes (Rel m) (finiteStage m) (fst xx) (fst yy) ⟩
        atM = subst (λ t → ⟨ precedes (λ s u → pr s u ∈ t) (finiteStage m)
                              (fst xx) (fst yy) ⟩) rval
          (subst (λ t → ⟨ precedes (Held r) (Lset t) (fst xx) (fst yy) ⟩) qc
            hprec)

再帰的な比較を得るため、precedes-map は基底関係 Rel m を before m に置き換える。基底関係は一致条件の前提に現れるため、必要な仮定の向きは逆であり、before m から relAt m への所属へ進む。こうしてまず before (suc m) が得られ、等式 k ≡ suc m から before k が従う。

        below : ⟨ before k (fst xx) (fst yy) ⟩
        below = subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) (sym ksuc)
          (precedes-map (Rel m) (before m) (finiteStage m) (fst xx) (fst yy)
            (λ w t hw ht hbf → relAt-fill m w t hw ht hbf) atM)

逆方向では、RelOf k で記述された要素を意味論的なステップの証人へ変換する。二つの端点はすでに与えられており、残る仕事は前者の添字とその関係の項目を復元し、その前者が上界の最大要素であることを示すことである。

    from : (x : V ℓ) → RelOf k x → StepOf b f γ x
    from x (xx , (yy , (xx∈ , (yy∈ , (qx , hbf))))) =
      numS m , (relAt m , (xx , (yy , (c∈ , (cmax , (hf , (xxb , (yyb
        , (qx , hprec)))))))))
      where

k が零なら before k の証明は存在しない。したがって補題 before-suc は、比較が後者段階で生じるような自然数 m を取り出す。

      m : ℕ
      m = before-suc k (fst xx) (fst yy) hbf .fst

同じ後者の分析から等式 k ≡ suc m も得られる。この等式が、段階 k での比較と、段階 m のデータを基底とする再帰のステップを結びつける。

      qk : k ≡ suc m
      qk = before-suc k (fst xx) (fst yy) hbf .snd

k は suc m なので、前者は m < k を満たす。この上界により、添字 m における近似表の正しさと完全性の仮定をともに利用できる。

      hm : m < k
      hm = subst (λ j → m < j) (sym qk) NatOrder.≤-refl

前者を表す数項は、b に保存された上界の要素でなければならない。不等式 m < k から # m ∈ # k が得られ、numS m と上界についての等式がこの所属を必要な形へ移す。

      c∈ : ⟨ fst (numS m) ∈ fst (lookup b γ) ⟩
      c∈ = subst (λ t → ⟨ fst (numS m) ∈ t ⟩) (sym qb)
        (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst m)) (#mono m k hm))

さらに、# m が # k の要素のうち最大であることを示す必要がある。d ∈ # k と # m ∈ d が与えられると、数項の消去は命題的切り詰めの中で d を j < k を満たすある # j として表す。この二つの所属から m < j と j ≤ m が同時に従う。

      cmax : (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩
           → ⟨ fst (numS m) ∈ fst d ⟩ → Empty.⊥
      cmax d hd hc = PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst d) (subst (λ t → ⟨ fst d ∈ t ⟩) qb hd))
        where

d ≡ # j という分岐では、d が # k = # (suc m) に属することから j ≤ m が得られる。一方、# m が d に属することから狭義不等式 m < j が得られるので、自然数順序の非対称性がこの分岐を退ける。

        step : Σ[ j ∈ ℕ ] ((j < k) × (fst d ≡ # j)) → Empty.⊥
        step (j , (hj , qd)) = <-asym mj (pred-≤-pred (subst (λ i → j < i) qk hj))
          where
          mj : m < j
          mj = #∈#-elim m j