段階順序の内部の表

related-in : relOf (orderAt α oα) a b → ⟨ Related α (pr (a .fst) (b .fst)) ⟩
related-in h = ∣ oα , ∣ a , ∣ b , (refl , ∣ h ∣₁) ∣₁ ∣₁ ∣₁

逆方向の読みは、意図的に狭い形をしている。入力の対象はすでに固定された端点 a,b の符号化された対として提示されている。この提示があるからこそ、存在的に表された対を二つの端点と比較し、その段階順序の比較を復元できる。任意の関係する対象を、選ばれた端点の対へ分解するものではない。

related-out : ⟨ Related α (pr (a .fst) (b .fst)) ⟩ → relOf (orderAt α oα) a b
related-out h = strict α oα a b (rec₁ squash₁ atOrd h)
  where
  atPair : (o : IsOrd α) (a' b' : Mem (Lset α))
         → (pr (a .fst) (b .fst) ≡ pr (a' .fst) (b' .fst))

切り詰められた記録が端点 a',b' と順序数性の証明 o を与えるとする。二つの符号化された対の等しさから a と a'、b と b' がそれぞれ同一視され、順序数性が命題であることから o と固定された証明 oα が同一視される。この三つの同一視に沿って記録された比較を輸送すると、固定された端点での切り詰められた比較が得られる。

         → ⟨ Ordering α o a' b' ⟩ → ⟨ Ordering α oα a b ⟩
  atPair o a' b' q = map₁
    (λ k → subst2 (relOf (orderAt α oα)) (sym ea) (sym eb)
      (subst (λ o' → relOf (orderAt α o') a' b') (isPropIsOrd α o oα) k))
    where

対の符号化の単射性は、まず底にある端点の集合の等しさを復元する。各端点は、集合とそれが Lset α に属する証明からなる依存対である。その証明は命題なので、第一成分の等しさは要素全体の等しさへ持ち上がる。これにより、比較を正しい依存型の中で輸送できる。

    ea : a ≡ a'
    ea = Σ≡Prop (λ x → (x ∈ Lset α) .snd) (pr-inj q .fst)
    eb : b ≡ b'
    eb = Σ≡Prop (λ x → (x ∈ Lset α) .snd) (pr-inj q .snd)

外側の順序数性の証明書は明示されているが、各端点は命題的切り詰めのもとでしか存在しない。そこで切り詰めを一層ずつ、命題 Ordering α oα a b へ除去する。この目標の中では一時的な代表を使えるが、どちらの端点も選ばれたデータとして外へ出ることはない。

  atOrd : Σ[ o ∶ IsOrd α ] ⟨ ∃[ a' ∶ Mem (Lset α) ] (∃[ b' ∶ Mem (Lset α) ] ((pr (a .fst) (b .fst) ≡ pr (a' .fst) (b' .fst))
               , setIsSet _ (pr (a' .fst) (b' .fst))) ⊓ Ordering α o a' b') ⟩
        → ⟨ Ordering α oα a b ⟩
  atOrd (o , h₁) = rec₁ squash₁
    (λ { (a' , h₂) → rec₁ squash₁

二つの一時的な端点を開いた後、対を整列する議論が a,b での切り詰められた比較を与え、strict がその特定の比較から必要な証人を復元する。この合成によって逆方向の読みが得られるが、三分性で正当化された比較の証人を除き、存在に関する切り詰めの境界はすべて保たれる。

      (λ { (b' , (q , hr)) → atPair o a' b' q hr }) h₂ }) h₁

private
  memL : Mem (Lset α) → S
  memL c = c .fst , Lset→isL α oα (c .fst) (c .snd)

まとめられた端点からモデル内部で作る順序対と、その底の集合からホスト側で作る Kuratowski 対は命題的に等しいが、定義的に同じものとは扱わない。この等しさに「r に属する」を作用させると、最初の輸送の橋が得られる。

  atRel : (a b : Mem (Lset α))
        → ((prʟ (memL a) (memL b)) .fst ∈ r .fst)
        ≡ (pr (a .fst) (b .fst) ∈ r .fst)
  atRel a b = cong (λ x → x ∈ r .fst) (prʟ-fst (memL a) (memL b))

同じ対の等しさに Related α を作用させると、意味論の側のもう一つの橋が得られる。二つの橋を合わせることで、内部の順序対に実現の証明を使い、その結果を底の集合の素の対について述べ直せる。逆向きにも同様である。

  atRelated : (a b : Mem (Lset α))
            → ⟨ Related α ((prʟ (memL a) (memL b)) .fst) ⟩
            ≡ ⟨ Related α (pr (a .fst) (b .fst)) ⟩
  atRelated a b = cong (λ x → ⟨ Related α x ⟩) (prʟ-fst (memL a) (memL b))

埋める向きは、二つの要素のホスト側の比較から始まる。Related の順方向の読みがそれを符号化された対の関係へ変え、実現の証明が関係を r への所属へ変え、対の橋が主張をホスト側の対へ戻す。したがって、orderAt で比較されるすべての対は、任意の実現集合に属する。

rel-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
         → ⟨ pr (a .fst) (b .fst) ∈ r .fst ⟩
rel-fill a b h = subst ⟨_⟩ (atRel a b)
  (hr (prʟ (memL a) (memL b)) .snd
    (transport (sym (atRelated a b)) (related-in α oα a b h)))

読む向きは同じ経路を逆にたどる。ホスト側の対の所属を内部の対の所属へ輸送し、実現の証明を外向きに読んで Related の事実を得て、固定されたホスト側の対へ戻す。最後に related-out が、切り詰められていない段階順序の比較を返す。

rel-rep : (a b : Mem (Lset α))
        → ⟨ pr (a .fst) (b .fst) ∈ r .fst ⟩ → relOf (orderAt α oα) a b
rel-rep a b h = related-out α oα a b
  (transport (atRelated a b)
    (hr (prʟ (memL a) (memL b)) .fst (subst ⟨_⟩ (sym (atRel a b)) h)))

後の議論には、依存的な要素の対ではなく、小さな提示 ⟪ Lset α ⟫ を用いるものがある。その提示の添字は底の集合へ埋め込まれ、Mem (Lset α) の要素を作るために必要な所属の証明を備えている。

private
  atIx : ⟪ Lset α ⟫ → Mem (Lset α)
  atIx m = ⟪ Lset α ⟫↪ m , memOf (Lset α) m

この提示に沿って orderAt を運ぶと、小さな添字型上の狭義順序が得られる。これは埋め込みを通して見た同じ比較なので、対応する表現定理に新たな順序論の議論は必要ない。

open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ )

提示の添字 u,v について、運ばれた比較は、まず対応する段階要素の比較として読まれる。先の埋める定理が、埋め込まれた端点の Kuratowski 対を r に入れる。これが、比較から所属へ向かう小さい添字での形である。

ixRel-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v
           → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ r .fst ⟩
ixRel-fill u v = rel-fill (atIx u) (atIx v)

逆に、埋め込まれた端点の対が r に属するなら、先の定理によって対応する段階要素の比較として読める。運ばれた順序の定義から、これは小さな提示における u と v の狭義比較そのものである。

ixRel-rep : (u v : ⟪ Lset α ⟫)
          → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ r .fst ⟩ → u ≺ᶜ v
ixRel-rep u v = rel-rep (atIx u) (atIx v)

変数形式の仮定は点ごとであり、実際に双方向である。論理式を満たす符号化対象を関係する対として読む向きと、関係することから充足を構成する向きの両方を含む。必要なのは、順序数より下の項目の正しさと、命題的切り詰めのもとの存在だけである。ここでは正確な定義域を仮定しないので、上界の外にありうる項目はこの意味論的な同一視に関与しない。

順序数と表が固定されたモデル要素になった後、定数形式の等式が同じ点ごとの同値を与える。分出で用いる定義論理式は、関係の要素の候補のために一つだけ自由スロットを残すので、この第二の提示が必要である。この等式は二つの文脈の意味を同一視するが、Cond と Cond₀ が構文的に等しいとは主張しない。

変数形式の条件を与えると、StepAt v b f は候補の値を外延的に指定する。ある対象がスロット v の値に属することと、Cond b f を満たすことがちょうど一致する。これは双方向の所属仕様であり、存在定理ではない。この仕様を実現する実際の集合は、後の再帰で置換と分出を用いて作られる。

StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
StepAt v b f = extAt v (Cond b f)

候補の値、順序数の添字、小さい段階の表の三つのスロットを固定し、順序数性、値の健全性、命題的切り詰めのもとの項目の存在を満たす環境を与える。これらの仮定のもとで、妥当性の等式は条件に共通の点ごとの意味を与える。続く二つの読みはこれを逆向きに用いる。外延的なステップ仕様から候補の値についての IsRel の証明を得る向きと、すでにある IsRel の証明からその仕様を満たす向きである。後の章で具体的な実例が与えられるまでは、構成全体がこの仮定されたステップ記述に相対したままである。

module _ {n : ℕ} (v b f : Fin n) (γ : Vec S n)
         (ob : IsOrd ((lookup b γ) .fst))
         (vals : Values (lookup f γ) ((lookup b γ) .fst))
         (ents : Entries (lookup f γ) ((lookup b γ) .fst)) where

private

  same : (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related ((lookup b γ) .fst) (z .fst)
  same = cond-spec b f γ ob vals ents

step-rel : ⟨ γ ⊨ StepAt v b f ⟩ → IsRel ((lookup b γ) .fst) (lookup v γ)
step-rel h z =
    (λ hz → subst ⟨_⟩ (same z) (extAt-out v (Cond b f) γ h z hz))
  , (λ hz → extAt-in v (Cond b f) γ h z (subst ⟨_⟩ (sym (same z)) hz))

step-table : IsRel ((lookup b γ) .fst) (lookup v γ) → ⟨ γ ⊨ StepAt v b f ⟩
step-table sp = extAt-in-both v (Cond b f) γ
  (λ z hz → subst ⟨_⟩ (sym (same z)) (sp z .fst hz))
  (λ z h → sp z .snd (subst ⟨_⟩ (same z) h))

近似とグラフ

ここで一般の再帰の形をこの一段階に特殊化する。近似とは、指定された定義域をもち、記録した各要素で一段階の条件を満たす集合符号化された表である。グラフは、そのような近似が現在の引数での値を支えることを述べ、順序対を値とするグラフは引数とその値を一緒に記録する。導入規則と除去規則を使えば、命題的切り詰めの存在から証人を選ぶことなく、以後はこの意味に沿って議論できる。

module A = RecShape StepAt
open A using ( ApproxAt; GraphAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step
             ; ApproxAt-in; GraphOf; Graph-in; Graph-out
             ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )

近似が記録するすべての値

近似が正しい値だけを記録することを示すため、その表と定義域を固定し、引数の候補 u を考える。帰納に用いる性質は、u が構成可能な順序数なら、記録された各対 (u,r) の値 r が u での関係を実現する、というものである。記録されたすべての値を対象にするため、単値性を仮定していない。

module _ {n : ℕ} (f a : Fin n) (γ : Vec S n) where

private
  Value : V ℓ → Type (ℓ-suc ℓ)
  Value u = ⟨ isL u ⟩ → IsOrd u → (r : S)
          → ⟨ pr u (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel u r

approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd ((lookup a γ) .fst)
           → (c : S) → IsOrd (c .fst) → (r : S)
           → ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel (c .fst) r
approx-val h oa c = ∈-induction {P = Value} go (c .fst) (c .snd)
  where

  go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
  go u IH hu ou r p = step-rel zero (suc zero) (sh2 f) (r ∷ d ∷ γ) ou vals ents
    (ApproxAt-step f a γ h d r p)
    where
    d : S

    d = u , hu
    u∈a : ⟨ u ∈ (lookup a γ) .fst ⟩
    u∈a = ApproxAt-dom f a γ h d r p
    vals : Values (lookup f γ) u
    vals e t e∈ q =

      IH (e .fst) e∈ (e .snd) (mem-ord {A = u} ou (e .fst) e∈) t q
    ents : Entries (lookup f γ) u
    ents e e∈ = ApproxAt-value f a γ h e (oa .fst {x = u} {y = e .fst} e∈ u∈a)

グラフが決定する値

グラフの主張が含む、それを支える近似の証人は命題的切り詰めの中にある。しかし、求める結論である「表示された値が順序数の引数での関係を実現する」は命題である。したがって、その結論へ切り詰めを除去できる。ここで得られるのはグラフの値の正しさであり、一意性にはさらに二つの実現集合を外延性で比較する必要がある。

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

graph-only : ⟨ γ ⊨ GraphAt w b ⟩ → IsOrd ((lookup b γ) .fst)
           → IsRel ((lookup b γ) .fst) (lookup w γ)
graph-only h ob = rec₁ ((Realizes ((lookup b γ) .fst) (lookup w γ)) .snd)
  read (Graph-out w b γ h)

  where
  read : GraphOf w b γ → IsRel ((lookup b γ) .fst) (lookup w γ)
  read (f , (ha , hs)) = step-rel (suc w) (suc b) zero (f ∷ γ) ob vals ents hs
    where
    vals : Values f ((lookup b γ) .fst)

    vals c r c∈ p = approx-val zero (suc b) (f ∷ γ) ha ob c
      (mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈) r p
    ents : Entries f ((lookup b γ) .fst)
    ents = ApproxAt-value zero (suc b) (f ∷ γ) ha

graph-table : (h : S) → IsOrd ((lookup b γ) .fst)
            → Values h ((lookup b γ) .fst) → Entries h ((lookup b γ) .fst)
            → Domain h ((lookup b γ) .fst)
            → IsRel ((lookup b γ) .fst) (lookup w γ) → ⟨ γ ⊨ GraphAt w b ⟩
graph-table h ob vals ents dom sp = Graph-in w b γ h approx

  (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents sp)
  where
  onDom : (c : S)
        → (⟨ ∃[ r ∶ S ] pr (c .fst) (r .fst) ∈ h .fst ⟩
           → ⟨ c .fst ∈ (lookup b γ) .fst ⟩)

        × (⟨ c .fst ∈ (lookup b γ) .fst ⟩
           → ⟨ ∃[ r ∶ S ] pr (c .fst) (r .fst) ∈ h .fst ⟩)
  onDom c = (λ hr → rec₁ ((c .fst ∈ (lookup b γ) .fst) .snd)
                      (λ { (r , p) → dom c r p }) hr)
          , ents c

  onStep : (c r : S) → ⟨ pr (c .fst) (r .fst) ∈ h .fst ⟩
         → ⟨ (r ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
  onStep c r p = step-table zero (suc zero) (suc (suc zero)) (r ∷ c ∷ h ∷ γ)
    oc vals' ents' (vals c r c∈ p)
    where

    c∈ : ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    c∈ = dom c r p
    oc : IsOrd (c .fst)
    oc = mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈
    vals' : Values h (c .fst)

    vals' e t _ q = vals e t (dom e t q) q
    ents' : Entries h (c .fst)
    ents' e e∈ = ents e (ob .fst {x = c .fst} {y = e .fst} e∈ c∈)

  approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
  approx = ApproxAt-in zero (suc b) (h ∷ γ)
    (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep

順序対を値とするグラフ

置換公理は、完全な表の項目を値とするグラフに作用する。そこで PairGraphAt は、表示された値が現在の添字とある関係集合との Kuratowski 対であり、その関係集合がその添字で GraphAt を満たすことを述べる。二つの読みは、関係集合の証人を命題的切り詰めの内側に保つ。これが、関係集合を値とする再帰と、添字つきの項目からなる置換の像との橋になる。

表と上界における関係

クラス Recorded B は、B より下の表がもつべき要素を記述する。ある対象がこのクラスに属するとは、モデル要素 c と r が命題的切り詰めのもとで存在し、c が B に属し、r が c での関係を実現し、その対象が二つの基礎の集合の順序対に等しいことである。定義そのものは B が順序数であることを要求せず、このクラスを順序数の上界で使うときに順序数性が働く。

Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Recorded B z = ∃[ c ∶ S ] (c .fst ∈ B) ⊓ (∃[ r ∶ S ]
  ((z ≡ pr (c .fst) (r .fst)) , setIsSet z (pr (c .fst) (r .fst)))
  ⊓ Realizes (c .fst) r)

モデルの集合が B の表であるとは、その集合への所属が各点で Recorded B への所属と同値であることである。二つの向きがともに必要である。一方は無関係な対象や領域外の対象を排除し、他方は c∈B かつ r が c での関係を実現する各対 (c,r) を含める。したがって IsTable は、正しい要素についての閉性だけでなく正確な表現を述べる。

IsTable : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
IsTable B h = (z : S) → (z .fst ∈ h .fst) ≡ Recorded B (z .fst)

α での再帰データは、モデル内の二つの集合を含む。一つは α より下の正しい要素すべてを正確に表す表であり、もう一つは α 自身での関係を実現する集合である。より大きい引数を扱うとき、第一成分は近似を検査するための既存の表を与え、第二成分は後の表に記録する関係の値を与える。この束は所属に沿う再帰が返すデータである。その型が命題であるという証明はなく、また必要でもない。所属に沿う帰納は任意の Type 値の族を受け取るからである。

Bundle : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
Bundle α = Σ[ h ∶ S ] Σ[ r ∶ S ] (IsTable α h × IsRel α r)

上界 B に対する正確な表 h を固定する。その仕様を具体的な要素に使うには、モデル要素の内部の順序対と、それらの基礎の集合からなるホスト側の Kuratowski 対をそろえる必要がある。内部対の射影則に沿って表の所属同値を運ぶと、基礎の順序対 (c,r) で使える形になる。

module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsTable B h) where

private
  atPair : (c r : S)
         → (pr (c .fst) (r .fst) ∈ h .fst) ≡ Recorded B (pr (c .fst) (r .fst))
  atPair c r = subst (λ x → (x ∈ h .fst) ≡ Recorded B x) (prʟ-fst c r)

    (sp (prʟ c r))

table-out : Domain h B × Values h B
table-out = (λ c r p → read c r p .fst) , (λ c r _ p → read c r p .snd)
  where
  read : (c r : S) → ⟨ pr (c .fst) (r .fst) ∈ h .fst ⟩
       → ⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r

  read c r p = rec₁ isPropBoth outer (subst ⟨_⟩ (atPair c r) p)
    where
    isPropBoth : isProp (⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r)
    isPropBoth = isProp× ((c .fst ∈ B) .snd) ((Realizes (c .fst) r) .snd)

    inner : (d t : S) → ⟨ d .fst ∈ B ⟩
          → (pr (c .fst) (r .fst) ≡ pr (d .fst) (t .fst)) → IsRel (d .fst) t
          → ⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r
    inner d t d∈ q hr =
        subst (λ x → ⟨ x ∈ B ⟩) (sym (pr-inj q .fst)) d∈

      , subst2 IsRel (sym (pr-inj q .fst)) (sym rt) hr
      where
      rt : r ≡ t
      rt = Σ≡Prop (λ x → (isL x) .snd) (pr-inj q .snd)

    outer : Σ[ d ∶ S ] ( ⟨ d .fst ∈ B ⟩
              × ⟨ ∃[ t ∶ S ] ((pr (c .fst) (r .fst) ≡ pr (d .fst) (t .fst))
                    , setIsSet _ (pr (d .fst) (t .fst))) ⊓ Realizes (d .fst) t ⟩ )
          → ⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r
    outer (d , (d∈ , hs)) = rec₁ isPropBoth

      (λ { (t , (q , hr)) → inner d t d∈ q hr }) hs

table-in : (c r : S) → ⟨ c .fst ∈ B ⟩ → IsRel (c .fst) r
         → ⟨ pr (c .fst) (r .fst) ∈ h .fst ⟩
table-in c r c∈ hr = subst ⟨_⟩ (sym (atPair c r))
  ∣ c , (c∈ , ∣ r , (refl , hr) ∣₁) ∣₁

順序数 α での関係を分出によって得る前に、関係しうるすべての順序対を含む一つの L の集合が必要である。求める上界は、Related α の各対象を含むモデル集合 D を返す。これは共通の容器にすぎず、無関係な要素を含んでもよいため、この時点では正確性を主張しない。

bound : (α : V ℓ) (oα : IsOrd α)
      → Σ[ D ∶ S ] ((z : S) → ⟨ Related α (z .fst) ⟩ → ⟨ z .fst ∈ D .fst ⟩)
bound α oα = d .fst , confine
  where
  ixL : ⟪ Lset α ⟫ → S

Lset α の小さい提示は、その全要素に添字を与える。各添字が提示する基礎の集合を、構成可能な段階への所属から得た構成可能性の証明と組にして、モデル要素にする。これにより、提示された各端点について内部の順序対を作れる。

  ixL m = ⟪ Lset α ⟫↪ m , Lset→isL α oα (⟪ Lset α ⟫↪ m) (memOf (Lset α) m)

提示の添字の対は小さい添字型をなす。それらに対応する内部順序対の族へ共通領域の原理を適用すると、その族の各要素を含むモデル集合 D が得られる。この原理が与えるのは包含だけであり、正確な像を計算せず、段階の順序に従って対を選別することもない。

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

共通の上界は提示の添字だけでなく、Lset α の通常の要素 a,b にも使えなければならない。各要素をそのファイバー添字で表し、対応する内部順序対について上界を使い、提示された対とホスト側の対 pr(a,fst .fst b) との等しさに沿って所属を運ぶ。したがって、段階の任意の二要素からなる順序対は D に属する。

  onPair : (a b : Mem (Lset α)) → ⟨ pr (a .fst) (b .fst) ∈ (d .fst) .fst ⟩
  onPair a b = subst (λ x → ⟨ x ∈ (d .fst) .fst ⟩)
    (prʟ-fst (ixL (fa .fst)) (ixL (fb .fst))
      ∙ cong₂ pr (fa .snd) (fb .snd))
    (d .snd (fa .fst , fb .fst))

a と b の所属証明は、それぞれを小さい提示の要素と同定する。得られるファイバーの等しさが二つの端点をそろえ、順序対を作る操作の合同性がホスト側の二つの対を同定する。内部対の射影則と合わせると、直前の所属の輸送に必要な等しさになる。

    where
    fa = ∈-asFiber {a = a .fst} {b = Lset α} (a .snd)
    fb = ∈-asFiber {a = b .fst} {b = Lset α} (b .snd)

Related α の任意の対象を取る。その定義は、命題的に切り詰められた三重の存在量化を通して、順序数性の証明、Lset α の二要素 a,b、および対象をその順序対と同定する等しさを与える。段階順序の比較そのものも、さらに命題的切り詰めの内側にある。目標である D への所属は命題なので、三つの存在量化の切り詰めを順に除去できる。この粗い上界に必要なのは二つの端点と対の等しさだけであり、切り詰められた比較の事実さえ使わない。

  confine : (z : S) → ⟨ Related α (z .fst) ⟩ → ⟨ z .fst ∈ (d .fst) .fst ⟩
  confine z = rec₁ ((z .fst ∈ (d .fst) .fst) .snd)
    (λ { (_ , h₁) → rec₁ ((z .fst ∈ (d .fst) .fst) .snd)
      (λ { (a , h₂) → rec₁ ((z .fst ∈ (d .fst) .fst) .snd)
        (λ { (b , (q , _)) →

回収した二つの端点からなる順序対は、先の結果によりすでに D に属する。回収した対の等しさの逆向きにこの所属を運ぶと、もとの対象が D に属すると分かる。証人は命題の証明の内部にとどまるため、この上界は各対象の端点を選んでいない。

          subst (λ x → ⟨ x ∈ (d .fst) .fst ⟩) (sym q) (onPair a b) }) h₂ }) h₁ })

表と現在の関係を、所属に沿う再帰で同時に構成する。実際の入力範囲は構成可能な順序数であり、α には L に属することの証明と順序数性の証明の両方が伴う。再帰の値は先ほどの束であり、後ではその仕様を通して使うよう定義を閉じている。この再帰は Type 値の族に適用でき、Bundle α が命題であることには依存しない。

opaque
  tableAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → Bundle α
  tableAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → Bundle α}
    (build (PairGraphAt zero (suc zero)) refl)
    where

α での帰納の一段階では、α の各要素 δ について、その構成可能性と順序数性が与えられれば対応する束がある、と再帰的に仮定する。ここでの課題は、α より下の表と α での関係を作ることである。順序対を値とするグラフの論理式を、意図した論理式との等しさとともに明示的な引数として保つ。これは数学的仮定を増やさず、置換の議論がまさにそのグラフを使うことを保証する。

    build : (φ : Formula S ) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → Bundle δ)
          → ⟨ isL α ⟩ → IsOrd α → Bundle α
    build φ qφ α IH hα oα = rep .fst .fst , (sep .fst .fst , (spec , rspec))

順序数 α とその構成可能性の証明を組にして、モデル要素 A を作る。これは順序対を値とするグラフを考える内部の定義域である。その要素は、順序数性を示せば所属に沿う再帰仮定を適用できる、より小さい集合にちょうど当たる。

      where
      A : S
      A = α , hα

順序数 α の各要素 c はそれ自身も順序数である。この継承された順序数性は不可欠である。再帰的構成の定義域は任意の構成可能な要素ではなく、構成可能な順序数だからである。この順序数性の証明を得る際に命題的切り詰めは使わない。

      ordOf : (c : S) → ⟨ c .fst ∈ α ⟩ → IsOrd (c .fst)
      ordOf c c∈ = mem-ord {A = α} oα (c .fst) c∈

c∈α のとき、モデル要素 c はすでに構成可能性の証明をもち、順序数の要素であることから順序数性も得られる。これは帰納仮定を適用するために必要な入力そのものである。結果として、c より下の正確な表と c での関係の実現集合をともに含む、c での完全な束が得られる。

      bun : (c : S) → ⟨ c .fst ∈ α ⟩ → Bundle (c .fst)
      bun c c∈ = IH (c .fst) c∈ (c .snd) (ordOf c c∈)

c での再帰的な束から、現在の関係の成分を取り出し、c での値とする。これは具体的なモデル要素であり、表の命題的切り詰められた Entries から取り出した証人ではない。定義域内の各構成可能な順序数での関係をその下の表と一緒に再帰が運ぶのは、この具体的な値を利用するためである。

      value : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      value c c∈ = bun c c∈ .snd .fst

その成分とともに保存された仕様は、選んだ値が Related c を実現すると述べる。これは帰納仮定が与える意味論的な正しさそのものである。この事実だけでは、その値が順序対を値とするグラフを満たすことも、c との対が完成した表に属することも主張できない。

      relOK : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) → IsRel (c .fst) (value c c∈)
      relOK c c∈ = bun c c∈ .snd .snd .snd

底の順序数が α に属する各 c について、帰納法の仮定はすでに c における関係集合を与えている。置換公理では、どの添字がその関係を生んだかを残す必要があるため、候補となる値は関係集合だけではなく、c とその関係集合との内部順序対である。

      entry : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      entry c c∈ = prʟ c (value c c∈)

次に、この候補が置換公理で用いるグラフ上にあることを示す。順序対を作る前に、選んだ関係集合が c における再帰グラフを満たさなければならない。c における束は、その下の表とそこで実現された関係をともに与える。また、順序数 α に c が属することから c 自身も順序数なので、表からグラフを得る一般の議論を適用できる。

      below : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) (k : S)
            → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ GraphAt zero (suc (suc zero)) ⟩
      below c c∈ k = graph-table zero (suc (suc zero))
        (value c c∈ ∷ k ∷ c ∷ []) (bun c c∈ .fst) (ordOf c c∈)
        (reads .snd) ents (reads .fst) (relOK c c∈)

下方の表の正確な仕様から、この議論に必要な三つの事実のうち二つが得られる。c より下で記録された各値は対応する関係を実現し、添字が c の外にある順序対は記録されない。残るのは完全性、すなわち c の各要素に何らかの記録値があることである。

        where
        reads : Domain (bun c c∈ .fst) (c .fst) × Values (bun c c∈ .fst) (c .fst)
        reads = table-out (c .fst) (ordOf c c∈) (bun c c∈ .fst)
                  (bun c c∈ .snd .snd .fst)
        ents : Entries (bun c c∈ .fst) (c .fst)