定義域の表示と符号化された関係を共通の土台として、二つの論理式を用意する。`CF` は `R` に対する局所的な崩壊値の論理式であり、`PF` は入力と、その論理式を満たす値との順序対を認識する。この時点では、どちらも崩壊値の存在や一意性を主張しない。
```agda
open Collapse D R Rsub public
module CF = ColFo R using ( colFo; colFo-in; colFo-out )
module PF = PairFo CF.colFo using ( pair-in; pair-out; pairFo )
```
`q` が `D` の要素なら、その所属証明を復号して添字 `toDom q mq` を得る。`toDom-val` により、この添字を埋め戻したものと `q` は同じ基礎の反復的集合をもつ。さらに `S` の構成可能性の成分は命題なので、基礎の集合の等しさから `S` における等しさが従う。
```agda
up-toDom : (q : S) (mq : Mem q) → up (toDom q mq) ≡ q
up-toDom q mq = Σ≡Prop (λ v → (isL v) .snd) (toDom-val q mq)
```
崩壊の論理式は、環境の第二の枠を通して入力に依存する。したがって等式 `x ≡ y` に沿ってその枠で直接置換でき、値 `v` が `x` で論理式を満たすなら `y` でも満たす。後で正準な表示 `up (toDom q mq)` と元の要素 `q` を結びつけるのは、この置換である。
```agda
colFo-at : (v : S) {x y : S} → x ≡ y
→ ⟨ (v ∷ x ∷ []) ⊨ CF.colFo ⟩ → ⟨ (v ∷ y ∷ []) ⊨ CF.colFo ⟩
colFo-at v e = subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ CF.colFo ⟩) e
```
ここで小さな関係が整礎かつ推移的であると仮定する。整礎性は `col` の再帰的定義と一意性証明の帰納を支え、推移性は得られる崩壊値が順序数であることを示すために使われる。二つの仮定の役割は異なり、先の `R` の端点条件からはどちらも従わない。
```agda
module Graph (wf : WellFounded _≺_)
(≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where
```
この二つの仮定のもとで、Mostowski 再帰は各 `a` に、その先行者の崩壊値からなる集合 `col a` を割り当てる。導入と除去の補題がその集合への所属を特徴づけ、`col-ord` は個々の `col a` が順序数であることを示す。ここでの主張は各点の崩壊値についてであり、後で集める集合 `otL` についてではない。
```agda
open Col wf ≺-trans public
```
整礎性はループ `a ≺ a` を排除する。帰納段階でそのようなループがあると、先行者についての帰納仮定を `a` 自身に適用できる。同じループが、`a` が自分自身より小さいことの証拠と、帰納仮定から矛盾を得るための入力の両方になる。
```agda
≺-irrefl : (a : Dom) → a ≺ a → ⊥₀
≺-irrefl = W.induction {P = λ a → a ≺ a → ⊥₀} (λ a rec h → rec a h h)
```
ここでの一意性は、項目が存在することを条件とする。正しい表 `F` が実際の定義域の点 `up a` で値 `v` を記録するなら、`v` の基礎の集合は `col a` に等しくなる。すべての正しい表が `D` の全要素で項目をもつとは主張していない。証明は `a` に関する整礎帰納で進み、表示された等式を帰納的述語とする。
```agda
correct-val : (F : S) → Correct F R → (a : Dom) (v : S)
→ Holds F (up a) v → v .fst ≡ col a
correct-val F hc = W.induction {P = λ a → (v : S) → Holds F (up a) v → v .fst ≡ col a} go
where
go : (a : Dom) → ((b : Dom) → b ≺ a → (v : S) → Holds F (up b) v → v .fst ≡ col b)
```
証明は、各点の同値に帰着する。`w` が記録された値に属することと、`w` が崩壊に属することは同値である。正しさの仮定から、`up a` での完備さと、値の条項という二つの補助の事実が取り出される。
```agda
→ (v : S) → Holds F (up a) v → v .fst ≡ col a
go a IH v hv = extensionalV {a = v .fst} {b = col a} (λ w → ⇔toPath (fwd w) (bwd w))
where
cmp : Complete F R (up a)
cmp = hc (up a) v hv .fst
```
`a` での項目の正しさには、相補的な二つの帰結がある。先の `cmp` はすべての先行者に表の項目を与え、`val` は `v` への所属と先行者の値として現れることを同定する。続く外延性の議論の二方向では、この二つを逆の順で用いる。
```agda
val : ValueIs F R (up a) v
val = hc (up a) v hv .snd
```
第一の包含を示すため、記録された値 `v` の要素 `w` を取る。`v` は構成可能であり、その要素 `w` も構成可能なので、台の要素 `wS` として組にできる。すると `val` の前向きの半分から、`a` のある `R`-先行者 `y` で表が `wS` を記録することが、命題的切り詰めのもとで得られる。
```agda
fwd : (w : V ℓ) → ⟨ w ∈ v .fst ⟩ → ⟨ w ∈ col a ⟩
fwd w w∈ = rec₁ ((w ∈ col a) .snd) read (val wS .fst w∈)
where
wS : S
wS = w , isL-trans {x = v .fst} {y = w} w∈ (v .snd)
```
出所の項目は、必要な二つの事実に変換される。載せられた先行者と入力の間の関係と、載せられた先行者での表の項目である。先行者は、その内部の添字に復号される。
```agda
read : Σ[ y ∶ S ] (Holds R y (up a) × Holds F y wS) → ⟨ w ∈ col a ⟩
read (y , (ry , fy)) = subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b b≺a)
where
my : Mem y
my = Rsub y (up a) ry .fst
```
内部の添字 `b` は所属を下降して復元され、関係の項目は内部の形 `b ≺ a` へ運ばれる。等式 `e` が、`w` と `b` の崩壊の同定を記録する。これは次に証明される。
```agda
b : Dom
b = toDom y my
b≺a : b ≺ a
b≺a = ≺-in b a (subst (λ t → ⟨ pr t (↪ a) ∈ R .fst ⟩) (sym (toDom-val y my)) ry)
e : w ≡ col b
```
この等式は、復号された先行者に帰納の仮定を適用したものである。表の、載せられた先行者での値は、その内部の添字の崩壊に等しく、輸送によって `w` に等しくなる。
```agda
e = IH b b≺a wS (subst (λ t → ⟨ pr t w ∈ F .fst ⟩) (sym (toDom-val y my)) fy)
```
逆向きの包含では `w ∈ col a` とする。崩壊の除去則から、ある先行者 `r ≺ a` について `col r ≡ w` であることが、命題的切り詰めのもとで得られる。目標 `w ∈ v .fst` は命題なので、その切り詰めの内側で議論できる。また `w` は構成可能な集合 `col a` の要素なので、構成可能性の証拠と組にして `wS` とできる。
```agda
bwd : (w : V ℓ) → ⟨ w ∈ col a ⟩ → ⟨ w ∈ v .fst ⟩
bwd w w∈ = rec₁ ((w ∈ v .fst) .snd) read (col-out a w w∈)
where
wS : S
wS = w , isL-trans {x = col a} {y = w} w∈ (col-isL a)
```
`col-out` が与える先行者 `r` について、`a` での項目の完全性から、`up r` におけるある表の値 `u` が単に存在することが得られる。目標である `w ∈ v` は命題なので、この切り詰めを除去できる。残る仕事は、`r` での正しさを用いて `u` を `col r` と比較し、したがって `w` と比較することである。
```agda
read : Σ[ r ∶ Dom ] ((r ≺ a) × (col r ≡ w)) → ⟨ w ∈ v .fst ⟩
read (r , (ra , e)) = rec₁ ((w ∈ v .fst) .snd) inner (cmp (up r) (≺-out r a ra))
where
inner : Σ[ u ∶ S ] Holds F (up r) u → ⟨ w ∈ v .fst ⟩
inner (u , fu) = val wS .snd
```
値の方程式の逆向きの半分は、出所の証人から `v` への所属を導く。ここでの証人は、先行者 `up r`、それと `up a` の関係、および値 `u` をもつ表の項目からなる。帰納仮定が `u` を `col r` と同定し、さらに等式 `col r ≡ w` に沿って項目を輸送することで、その値を `w` にする。
```agda
∣ up r , (≺-out r a ra , subst (λ t → ⟨ pr (↪ r) t ∈ F .fst ⟩) (IH r ra u fu ∙ e) fu) ∣₁
```
ここで `q` が実際に `D` の要素であり、`v` が `q` で局所的な崩壊の論理式を満たすとする。論理式から得られるのは、`(q,v)` を含む正しい表が単に存在することだけであるが、求める集合の等式は命題なので切り詰めを除去できる。項目を `q` から復号された表示へ輸送すると、`correct-val` によって `v .fst` は `col (toDom q mq)` と同定される。
```agda
colFo-val : (q : S) (mq : Mem q) (v : S) → ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩
→ v .fst ≡ col (toDom q mq)
colFo-val q mq v h = rec₁ (setIsSet (v .fst) (col (toDom q mq)))
(λ { (F , (hc , hv)) → correct-val F hc (toDom q mq) v
(subst (λ t → ⟨ pr t (v .fst) ∈ F .fst ⟩) (sym (toDom-val q mq)) hv) })
```
崩壊の論理式の外向きの読み出しが、正しい表と表の項目を供給する。それらは、一意性の補題の二つの入力である。
```agda
(CF.colFo-out v q h)
```
局所表のモジュールは、定義域の入力 `a` と、より小さい入力ごとに崩壊の論理式を供給する帰納の仮定によってパラメータづけられる。`a` のために、実際の先行者での項目が崩壊値を記録し、それ以外の項目が既定の対を記録する表を作る。
```agda
module Approx (a : Dom)
(IH : (b : Dom) → b ≺ a → ⟨ (colʟ b ∷ up b ∷ []) ⊨ CF.colFo ⟩) where
```
既定の項目 `ea` は、載せられた入力とその自身の崩壊の順序対で、台の要素として提示される。
```agda
ea : S
ea = prʟ (up a) (colʟ a)
```
局所の論理式の本体は、二つの選言肢をもつ。左は、`q` が `a` の実際の先行者であり、`z` が `q` と、崩壊の論理式を満たす値とを対にすること。右は、`q` が先行者ではなく、`z` が既定の項目であること。この場合分けは排中律で決定される。
```agda
Body : S → S → Type (ℓ-suc ℓ)
Body z q =
(Holds R q (up a)
× ∥ Σ[ v ∶ S ] ((z .fst ≡ pr (q .fst) (v .fst)) × ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩) ∥₁)
⊎ ((Holds R q (up a) → ⊥₀) × (z .fst ≡ ea .fst))
```
対象言語の中で先行者の場合と既定の場合を分けるには、変化する入力 `q` と固定された点 `a` からなる順序対を関係検査に使う必要がある。対の式は、局所的な論理式の二つの自由な枠において、この項を一様に与える。
```agda
module PE = PairExpression
```
式 `image` は順序対 `(q,up a)` を表す。第一成分は入力の枠から取り、第二成分は `a` を表す台の要素をリテラルとして置く。したがって `image` が `R` に属することは、ちょうど `q` が `a` の `R`-先行者であることを述べ、局所表の項目を記述するものではない。
```agda
image : PE.Expr 2
image = PE.pair (PE.slot (suc zero)) (PE.literal (up a))
```
論理式 `ψ` は `Body` の二つの場合に対応する。`q R a` なら、第一の分岐は出力 `z` が `q` と、`q` で `colFo` を満たすある値との順序対であることを要求する。`q` が `a` の先行者でないなら、第二の分岐は `z` が固定された既定の項目 `ea` に等しいことを要求する。どちらの分岐を選ぶかという古典的な判定は後の関数性証明で使われるのであり、選言そのものに含まれるわけではない。
```agda
opaque
ψ : Formula S 2
ψ = (PE.member image (con R) ∧̇ PF.pairFo)
∨̇ ((¬̇ PE.member image (con R)) ∧̇ (var zero ≐ con ea))
```
`ψ` を外向きに読むとき、選言を包む命題的切り詰めは保たれる。先行者の分岐では、対の式の読みが第一の連言肢を `q R a` へ変換し、`PF.pair-out` は、`q` で `colFo` を満たすある `v` について `z` が `(q,v)` であることを単に述べる。既定の分岐では、対象言語の否定をホストレベルでの `q R a` の反証へ変換する必要がある。
```agda
ψ-out : (z q : S) → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩ → ∥ Body z q ∥₁
ψ-out z q = map₁
(λ { (inl (h1 , h2)) → inl (PE.member-out image (con R) (z ∷ q ∷ []) h1
, PF.pair-out z q h2)
; (inr (h1 , h2)) → inr
```
このホストレベルの反証を得るため、`q R a` と仮定する。対の式を内向きに読むと、この仮定は所属原子式の充足へ移るが、対象言語の否定がそれを排除する。`z` を既定の項目と同定する等式はすでに必要なホストレベルの形なので、そのまま保たれる。
```agda
((λ k → lower (h1 (PE.member-in image (con R) (z ∷ q ∷ []) k))) , h2) })
```
内向きの読み出しは、左の分岐を、対の式の導入と対のグラフの導入を通して注入し、切り詰められた値を、命題値の充足の中へ消去する。
```agda
ψ-in : (z q : S) → Body z q → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
ψ-in z q (inl (h1 , hv)) = rec₁ (((z ∷ q ∷ []) ⊨ ψ) .snd)
(λ { (v , (e , hc)) → ∣ inl (PE.member-in image (con R) (z ∷ q ∷ []) h1
, PF.pair-in z q v e hc) ∣₁ }) hv
ψ-in z q (inr (h1 , e)) =
```
右の分岐は、ホスト側の反駁を対象言語へ持ち上げ、既定の等式を運ぶ。どちらの分岐も、論理式の切り詰められた選言へ注入される。
```agda
∣ inr ((λ k → lift (h1 (PE.member-out image (con R) (z ∷ q ∷ []) k))) , e) ∣₁
```
補助の `b≺a-of` は、ホスト側の関係の所属を、内部の比較へ復号する。`q` が `a` と関係するなら、`q` の内部の添字は `a` より下である。復号は、所属を下降して添字を取り出すことによって行われる。
```agda
private
b≺a-of : (q : S) (mq : Mem q) → Holds R q (up a) → toDom q mq ≺ a
b≺a-of q mq h = ≺-in (toDom q mq) a
(subst (λ t → ⟨ pr t (↪ a) ∈ R .fst ⟩) (sym (toDom-val q mq)) h)
```
帰納仮定は正準な表示 `up (toDom q mq)` で述べられているが、局所的な論理式は元の台の要素 `q` で満たされなければならない。往復の等式が二つの表示を同定し、`colFo-at` が充足証明を正準な表示から `q` へ輸送する。
```agda
IHq : (q : S) (mq : Mem q) → toDom q mq ≺ a
→ ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
IHq q mq k = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (IH (toDom q mq) k)
```
置換が要求するのは、各 `q ∈ D` で `ψ` を満たす値が可縮なファイバーをなすことである。証明では排中律を用いて `q R a` かどうかを判定する。どちらの場合にも、論理式を満たす正準な出力と、それを満たすほかの出力がすべて正準な出力に等しいことの証明を、命題的切り詰めのもとで与える。`mereFunct` は、この切り詰められた一意存在を可縮性へ変換する。
```agda
fc : (q : S) → ⟨ q ∈ˢ D ⟩ → isContr (Σ[ z ∶ S ] ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩)
fc q mq = mereFunct ψ q
(decide (FOL.Semantics.decideMembership 𝒮ᵥ lem
(pr (q .fst) (↪ a)) (R .fst)))
where
b : Dom
b = toDom q mq
```
先行者の分岐における正準な出力は `zb = prʟ q (colʟ b)` であり、その基礎集合が `(q,col b)` を符号化する。ここで `b` は `q` から復号された内部の添字である。一方、先行者でない分岐では既定の出力 `ea` を使う。局所的な判定の補題は、どちらの場合にも論理式を満たす出力が一つあり、それを満たすほかの出力はすべてその出力に等しいことを、命題的切り詰めのもとで示す。
```agda
zb : S
zb = prʟ q (colʟ b)
decide : Dec (Holds R q (up a))
→ ∥ Σ[ z ∶ S ] (⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
× ((z' : S) → ⟨ (z' ∷ q ∷ []) ⊨ ψ ⟩ → z' ≡ z)) ∥₁
```
`q R a` と仮定する。帰納仮定は `col b` が `q` で `colFo` を満たすことを与え、`prʟ-fst` は `zb .fst` と順序対の符号 `pr (q .fst) (col b)` の間に必要な等式を与えるので、正準な出力 `zb` は左の分岐を満たす。一意性を示すため、任意の充足する出力を同じ二つの場合に分けて読む。左の分岐の証人は `colFo-val` によって決まり、右の分岐の証人は仮定 `q R a` と矛盾する。
```agda
decide (yes h) = ∣ zb
, ( ψ-in zb q (inl (h , ∣ colʟ b , (prʟ-fst q (colʟ b) , IHq q mq (b≺a-of q mq h)) ∣₁))
, λ z' hz' → rec₁ (isSetS z' zb)
(λ { (inl (_ , hv)) → rec₁ (isSetS z' zb)
(λ { (v , (e , hcol)) → Σ≡Prop (λ w → (isL w) .snd)
```
左の分岐にある別の証人について、`colFo-val` はその第二成分を `col b` と同定する。これを順序対の等式と合成すると、出力全体が `zb` に等しいことが従う。右の分岐にある別の証人は `q R a` の反証を含むので存在できない。これで先行者の場合の一意性が完了する。最後の行からは、既定の出力 `ea` を選ぶ、先行者でない場合が別に始まり、その一意性証明は次のコードブロックへ続く。
```agda
(e ∙ cong (pr (q .fst)) (colFo-val q mq v hcol) ∙ sym (prʟ-fst q (colʟ b))) })
hv
; (inr (nh , _)) → ⊥₀-rec (nh h) })
(ψ-out z' q hz') ) ∣₁
decide (no nh) = ∣ ea
```
所属を否定する場合が一意性の議論を閉じる。既定の項目 `ea` は `ψ` を満たす。別の証人を外向きに読むと、`nh` と矛盾する肯定的な所属が得られるか、既定の分岐から `z' .fst ≡ ea .fst` が得られる。後者では、構成可能性の証明が命題であることにより、基礎集合のこの等式が `S` で必要な等式 `z' ≡ ea` へ持ち上がる。
```agda
, ( ψ-in ea q (inr (nh , refl))
, λ z' hz' → rec₁ (isSetS z' ea)
(λ { (inl (h , _)) → ⊥₀-rec (nh h)
; (inr (_ , e)) → Σ≡Prop (λ w → (isL w) .snd) e })
(ψ-out z' q hz') ) ∣₁
```
この局所再帰の定義域は `D` 全体である。`q R up a` なら、その一意な値は `q` と、`q` が表示する添字での崩壊値との順序対である。そうでなければ、値は共通の既定項 `ea` である。`ψ` とこの一意性証明に置換を適用すると、得られる値が一つの構成可能集合に集められる。
```agda
module T = Of (record { dom = D ; graph = ψ ; funct = fc }) using ( table; table-in; table-out )
```
`Fa` は置換で得られたこの値域を表す。以下の所属補題により、その要素は `b ≺ a` を満たす順序対 `pr(↪ b,col b)` と、既定の分岐が与える最上部の順序対 `pr(↪ a,col a)` にちょうど限られることが分かる。
```agda
Fa : S
Fa = T.table
```
`Below b` は、添字 `b` が現在のもの以下であることを述べる。真に下か、等しいかのいずれかである。この二つの述語が、局所的な表の導入と正しさの両方を支える。
```agda
Below : Dom → Type ℓ
Below b = (b ≺ a) ⊎ (b ≡ a)
```
`b` が `a` 以下なら、`Fa-in` は入力 `up b` と値 `colʟ b` からなるグラフの項を `Fa` に入れる。狭義の比較の場合は帰納仮定によって `ψ` の第一の選言肢を満たし、等式 `b ≡ a` の場合はこの順序対を `ea` と同一視して既定の分岐を使う。
```agda
Fa-in : (b : Dom) → Below b → Holds Fa (up b) (colʟ b)
Fa-in b k = subst (λ w → ⟨ w ∈ Fa .fst ⟩) (prʟ-fst (up b) (colʟ b))
(T.table-in (up b) (prʟ (up b) (colʟ b)) (up-mem b) (ψ-in _ (up b) (bodyOf k)))
where
bodyOf : Below b → Body (prʟ (up b) (colʟ b)) (up b)
```
狭義の場合、式の本体には関係の証拠 `b ≺ a` と、`colʟ b` が `up b` で崩壊の論理式を満たすという帰納仮定が入る。等しい場合、非反射性が `up b R up a` を排除し、`b ≡ a` に沿う輸送が対象の順序対を既定の順序対と同一視する。
```agda
bodyOf (inl k) = inl (≺-out b a k , ∣ colʟ b , (prʟ-fst (up b) (colʟ b) , IH b k) ∣₁)
bodyOf (inr e) = inr
( (λ h → ≺-irrefl a (≺-in a a (subst (λ t → Holds R (up t) (up a)) e h)))
, prʟ-fst (up b) (colʟ b) ∙ cong (λ t → pr (↪ t) (col t)) e ∙ sym (prʟ-fst (up a) (colʟ a)) )
```
逆に、`Fa` への所属からは、`b ≺ a` または `b ≡ a` を満たす添字 `b` と、その要素を `pr(↪ b,col b)` と同一視する等式が単に得られる。添字は命題的切り詰めの中にあるため、この結論は代表を選ばない。
```agda
Fa-out : (y : S) → ⟨ y ∈ˢ Fa ⟩
→ ∥ Σ[ b ∶ Dom ] (Below b × (y .fst ≡ pr (↪ b) (col b))) ∥₁
Fa-out y hy = rec₁ squash₁
(λ { (q , (mq , hψ)) → rec₁ squash₁
(λ { (inl (h , hv)) → map₁
```
先行者の分岐では、`colFo-val` が論理式から得た値を `toDom q mq` での崩壊値と同一視し、続いて `q` の表示等式が順序対を標準形へ書き換える。既定の分岐で記録されるのは、`a` 自身を添字とする順序対である。
```agda
(λ { (v , (e , hcol)) → toDom q mq
, (inl (b≺a-of q mq h)
, e ∙ cong₂ pr (sym (toDom-val q mq)) (colFo-val q mq v hcol)) })
hv
; (inr (_ , e)) → ∣ a , (inr refl , e ∙ prʟ-fst (up a) (colʟ a)) ∣₁ })
```
置換の読み出し補題と `ψ-out` は、どちらも命題的に切り詰められた証人だけを返す。目標も命題的に切り詰められているので、どちらの証人も大域的に選ぶことなく、外側、内側の順に切り詰めを除去できる。
```agda
(ψ-out y q hψ) })
(T.table-out y hy)
```
直前の結果を `x` と `v` の順序対符号に適用すると、その二つの座標を復元できる。したがってグラフの項 `Holds Fa x v` からは、`x .fst ≡ ↪ b` かつ `v .fst ≡ col b` を満たすある `b ≤ a` が単に得られる。
```agda
Fa-pair : (x v : S) → Holds Fa x v
→ ∥ Σ[ b ∶ Dom ] (Below b × (↪ b ≡ x .fst) × (col b ≡ v .fst)) ∥₁
Fa-pair x v h = map₁ step
(Fa-out (prʟ x v) (subst (λ w → ⟨ w ∈ Fa .fst ⟩) (sym (prʟ-fst x v)) h))
where
```
輸送は等式を内部の対に向け直し、補助が順序対の単射性を通してそれを、添字の名指しの等式と崩壊の値の名指しの等式に分ける。
```agda
step : Σ[ b ∶ Dom ] (Below b × ((prʟ x v) .fst ≡ pr (↪ b) (col b)))
→ Σ[ b ∶ Dom ] (Below b × (↪ b ≡ x .fst) × (col b ≡ v .fst))
step (b , (k , e)) = b , (k , sym (q .fst) , sym (q .snd))
where
q : (x .fst ≡ ↪ b) × (v .fst ≡ col b)
```
合成した順序対の等式に `pr-inj` を適用すると、`x .fst ≡ ↪ b` と `v .fst ≡ col b` が得られる。`Fa-pair` が要求する結果では正準な座標が等式の左辺にあるため、`step` は二つの成分の等式を反転してから返す。
```agda
q = pr-inj (sym (prʟ-fst x v) ∙ e)
```
`c ≺ b` かつ `b ≺ a` なら、推移性から `c ≺ a` が従う。一方 `b ≡ a` なら、この等式を `c ≺ b` に代入して同じ結論を得る。これが `Below b` の二つの場合である。
```agda
below-trans : {c b : Dom} → c ≺ b → Below b → c ≺ a
below-trans cb (inl k) = ≺-trans cb k
below-trans {c} cb (inr e) = subst (c ≺_) e cb
```
`Correct Fa R` を示すため、`Fa` の実際の項 `(x,v)` を固定する。対の読み出しから得られる、この項を表示する添字は命題的に切り詰められている。しかし `Complete Fa R x` と `ValueIs Fa R x v` はともに命題なので、その連言へ切り詰めを除去できる。
```agda
Fa-correct : Correct Fa R
Fa-correct x v hxv = rec₁
(isProp× (isPropΠ (λ _ → isPropΠ (λ _ → squash₁)))
(isPropΠ (λ w → isProp× (isPropΠ (λ _ → squash₁))
(isPropΠ (λ _ → (w .fst ∈ v .fst) .snd)))))
```
選んだ項がある `b ≤ a` で表され、`x` が `b` を表示し、`v` の基礎集合が `col b` であるとする。完全性では、`x` の各 `R`-先行者が `Fa` で値をもつことを示す。値条件では各 `w` について、`w ∈ v` と、そのような先行者の一つが `Fa` で `w` と対になっていることとの同値を示す。
```agda
build (Fa-pair x v hxv)
where
build : Σ[ b ∶ Dom ] (Below b × (↪ b ≡ x .fst) × (col b ≡ v .fst))
→ Complete Fa R x × ValueIs Fa R x v
build (b , (k , ex , ev)) = cmp , (λ w → fwd w , bwd w)
```
ここで中心となる変換は、符号化された先行者 `y R x` を `Dom` 上の狭義比較へ移すことである。項目の表示が同一視するのは `x .fst` と表示された要素 `↪ b` であり、台の要素 `x` と外部の添字 `b` ではない。`Rsub` がまず `y` を `D` に入れ、その後で `toDom` が `b` と比較できる添字を復元する。
```agda
where
```
`y R x` から端点の包含仮定によって `y ∈ D` が得られるので、`toDom y my` は添字 `c` を定める。`y` と `x` の表示等式に沿って関係の証拠を輸送すると `c ≺ b` が従い、第二成分には `↪ c` が `y` の基礎集合であることが記録される。
```agda
pred : (y : S) → Holds R y x → Σ[ c ∶ Dom ] ((c ≺ b) × (↪ c ≡ y .fst))
pred y hy = c , (≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ R .fst ⟩)
(sym (toDom-val y my)) (sym ex) hy) , toDom-val y my)
where
my : Mem y
```
証明 `my` は `Rsub` が与える第一端点の所属そのものであり、`toDom y my` を作るために必要な根拠である。`D` への所属は命題なので、この根拠を使っても表示の選択が新たに加わることはない。
```agda
my = Rsub y x hy .fst
c : Dom
c = toDom y my
```
先行者 `y R x` に対し、直前に復元した添字を `c` とする。完全性の値の証人は `colʟ c` である。`Fa-in` が入力 `up c` での標準的な項を与え、それを `↪ c ≡ y .fst` に沿って輸送すると、入力 `y` で必要な項になる。`b ≤ a` を介する推移性により、`c` は `a` より真に下にある。
```agda
cmp : Complete Fa R x
cmp y hy = ∣ colʟ c , subst (λ t → ⟨ pr t (col c) ∈ Fa .fst ⟩) ec
(Fa-in c (inl (below-trans cb k))) ∣₁
where
c = pred y hy .fst
```
ここで `pred y hy` の二つの射影を `cb` と `ec` と名づける。`cb` は狭義比較 `c ≺ b` であり、`ec` は標準的な代表 `↪ c` を実際の入力 `y` と同一視する。前者は `Fa-in` に必要な境界を、後者は項を `y` へ運ぶ輸送を与える。
```agda
cb = pred y hy .snd .fst
ec = pred y hy .snd .snd
```
`ValueIs` の順方向では、`w ∈ v` を `w .fst ∈ col b` と書き換える。崩壊の外向き補題から単に得られる `r ≺ b` と `col r ≡ w .fst` により、`up r` から `x` への `R`-辺と、`up r` を `w` に対応させる表の項が構成できる。
```agda
fwd : (w : S) → ⟨ w .fst ∈ v .fst ⟩ → Src Fa R x w
fwd w w∈ = map₁ read (col-out b (w .fst) (subst (λ t → ⟨ w .fst ∈ t ⟩) (sym ev) w∈))
where
read : Σ[ r ∶ Dom ] ((r ≺ b) × (col r ≡ w .fst)) → Σ[ y ∶ S ] (Holds R y x × Holds Fa y w)
read (r , (rb , er)) = up r
```
二つの所属は添字の等式と狭義の比較に沿って輸送され、関係と表の所属の両方が名指された先行者のところに置かれる。
```agda
, ( subst (λ t → ⟨ pr (↪ r) t ∈ R .fst ⟩) ex (≺-out r b rb)
, subst (λ t → ⟨ pr (↪ r) t ∈ Fa .fst ⟩) er (Fa-in r (inl (below-trans rb k))) )
```
逆方向では、`Src Fa R x w` の証人から、`y R x` を満たし、表で `y` から `w` への項をもつような `y` が単に得られる。目標 `w .fst ∈ v .fst` は命題なので、出所の証人と表の読み出しに含まれる命題的切り詰めを順にそこへ除去できる。
```agda
bwd : (w : S) → Src Fa R x w → ⟨ w .fst ∈ v .fst ⟩
bwd w = rec₁ ((w .fst ∈ v .fst) .snd) (λ { (y , (hy , fy)) →
rec₁ ((w .fst ∈ v .fst) .snd) (read y hy) (Fa-pair y w fy) })
where
read : (y : S) → Holds R y x
```
表の項を読むと、添字 `c`、`y` を `↪ c` と同一視する等式、そして `w` を `col c` と同一視する等式が得られる。最初の等式を `y R x` および `x` が `b` で表示されることと合わせると `c ≺ b` が従う。そこで `col-in` が `col c ∈ col b` を与え、残りの等式がこの所属を `w ∈ v` へ輸送する。
```agda
→ Σ[ c ∶ Dom ] (Below c × (↪ c ≡ y .fst) × (col c ≡ w .fst))
→ ⟨ w .fst ∈ v .fst ⟩
read y hy (c , (_ , ey , ew)) =
subst2 (λ s t → ⟨ s ∈ t ⟩) ew ev (col-in b c cb)
where
```
`c` と `b` の間の狭義の比較は、二つの名指しの等式と関係の証人から満たされ、先行者のデータがそろう。
```agda
cb : c ≺ b
cb = ≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ R .fst ⟩) (sym ey) (sym ex) hy)
```
局所的な表は頂点の要素でグラフの論理式を満たし、既定の項目が値の節の証人になる。これがこの節の帰納の段階である。
```agda
approx-step : ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
approx-step = CF.colFo-in (colʟ a) (up a) Fa Fa-correct (Fa-in a (inr refl))
```
ここで整礎帰納により、崩壊の論理式が各 `a : Dom` で成り立つことを示す。帰納仮定は各狭義先行者での充足証拠を与え、`Approx.approx-step` はそれらを用いて `a` で正しい局所表を構成する。結論は `Dom` のすべての添字に関するものであり、`D` 自体がすでに順序数と同一視されていることは必要ない。
```agda
approx : (a : Dom) → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
approx = W.induction {P = λ a → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩}
(λ a IH → Approx.approx-step a IH)
```
`q : S` と `mq : Mem q` に対して、直前の帰納はまず正準な表示 `up (toDom q mq)` で論理式を与える。往復の等式 `up-toDom q mq` がその表示を `q` と同一視し、`colFo-at` が充足証明を `D` のもとの要素へ輸送する。
```agda
approx-at : (q : S) (mq : Mem q) → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
approx-at q mq = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (approx (toDom q mq))
```
再帰 `otR` は `D` を定義域、`CF.colFo` を値関係とする。要素 `q ∈ D` で選ばれる値は、小さい添字 `toDom q mq` での崩壊値である。直前の近似により、この値が `q` で論理式を満たすことが示される。
```agda
private
otR : Recursion
otR = record
{ dom = D
; graph = CF.colFo
```
フィールド `funct` は、各 `q ∈ D` で `CF.colFo` を満たす値のファイバーが可縮であることを示さなければならない。その中心は `colʟ (toDom q mq)` と `approx-at q mq` である。別の要素 `(v,hv)` に対して、`colFo-val` は `v` の基礎集合を同じ崩壊値と同一視する。構成可能性の証明と充足の証明が命題であることにより、この等式はまず `v` の等式へ、最後にファイバーの要素全体の等式へ持ち上がる。
```agda
; funct = λ q mq → (colʟ (toDom q mq) , approx-at q mq)
, λ { (v , hv) → Σ≡Prop (λ w → ((w ∷ q ∷ []) ⊨ CF.colFo) .snd)
(sym (Σ≡Prop (λ w → (isL w) .snd) (colFo-val q mq v hv))) } }
```
一般の置換構成 `Of` は、この関数的な再帰をその値の表へ変える。また所属の特徴づけを両方向に与える。再帰関係を満たす値は表に入り、表の各要素は、必要な論理式の証拠を伴う `D` のある入力から生じる。
```agda
module OT = Of otR using ( table; table-in; table-out )
```
`otL` は `otR` の置換による値域であり、したがって `L` の要素である。その基礎集合はすべての `b : Dom` に対する崩壊値 `col b` を集めるが、それらの値が互いに異なる添字から来る必要はない。ここではこの正確な値域の記述だけを用い、値域全体の順序数性はさらに導くべき結論として残す。
```agda
otL : S
otL = OT.table
```
各 `b : Dom` について、近似補題は `colʟ b` が `up b` における `otR` の値であることを示す。したがって置換の導入方向から `col b ∈ otL .fst` が得られる。
```agda
otL-in : (b : Dom) → ⟨ col b ∈ otL .fst ⟩
otL-in b = OT.table-in (up b) (colʟ b) (up-mem b) (approx b)
```
逆に、各 `y ∈ otL .fst` について、`col b ≡ y` を満たす添字 `b : Dom` が単に存在する。結論には意図的に命題的切り詰めが残されているため、各要素の原像を選ぶことなく正確な値域を記述している。
```agda
otL-out : (y : V ℓ) → ⟨ y ∈ otL .fst ⟩ → ∥ Σ[ b ∶ Dom ] (col b ≡ y) ∥₁
otL-out y hy = map₁ (λ { (q , (mq , h)) → toDom q mq , sym (colFo-val q mq yS h) })
(OT.table-out yS hy)
where
yS : S
```
置換の読み出しを適用するには、周囲の集合 `y` を構成可能な領域の要素として扱う必要がある。`y ∈ otL .fst` と `otL` の構成可能性から、構成可能性の下方閉性がこの組を与える。
```agda
yS = y , isL-trans {x = otL .fst} {y = y} hy (otL .snd)
```
再帰グラフの構成を `otR` に適用すると、裸の値ではなく順序対が集められる。`D` の各入力について、その入力と一意に定まる崩壊値を記録し、対応する内向きと外向きの読み、一価性、そして定義域が正確に `D` であることを与える。
```agda
module CT = RecursionGraph otR using ( F; F-in; F-out; pair-out; sv; dm )
```
`colTable` は、`L` の内部で `otR` から構成されたグラフの集合である。`b : Dom` における正準な項目は `pr(↪ b,col b)` である。表に保存される入力は `D` の表示された要素 `↪ b` であり、`b` 自体は外部の小さな表示に属する添字のままである。
```agda
colTable : S
colTable = CT.F
```
標準的な代表 `up b` において、再帰グラフが最初に記録する値は `col (toDom (up b) (up-mem b))` である。表示等式から、この復元された添字と `b` との等式が得られる。その `col` による像に沿って第二座標を輸送すると、主張された順序対 `pr(↪ b,col b)` が得られる。
```agda
colTable-in : (b : Dom) → ⟨ pr (↪ b) (col b) ∈ colTable .fst ⟩
colTable-in b = subst (λ t → ⟨ pr (↪ b) t ∈ colTable .fst ⟩)
(cong col (Dom≡ (toDom-val (up b) (up-mem b)))) (CT.F-in (up b) (up-mem b))
```
逆に `colTable-out` は、グラフの任意の要素 `y` について、ある `b : Dom` に対する `y .fst ≡ pr(↪ b,col b)` が単に成り立つと述べる。その添字は命題的切り詰めの中にあるため、この外向きの読みはグラフを特徴づけるが、各要素を表示する添字を選ばない。
```agda
colTable-out : (y : S) → ⟨ y ∈ˢ colTable ⟩
→ ∥ Σ[ b ∶ Dom ] (y .fst ≡ pr (↪ b) (col b)) ∥₁
colTable-out y hy = map₁ (λ { (q , mq , e) → toDom q mq
, e ∙ cong (λ t → pr t (col (toDom q mq))) (sym (toDom-val q mq)) }) (CT.F-out (y .fst) hy)
```
ファイバーの述語は、`x` と対にされる要素 `v` が `x` の提示する添字の崩壊の値であることを述べ、提示の所属をデータとして伴う。
```agda
Fib : S → S → Type (ℓ-suc ℓ)
Fib x v = Σ[ mx ∶ Mem x ] (v .fst ≡ col (toDom x mx))
```
`x` と `v` を固定すると、`Fib x v` は命題である。所属 `mx : Mem x` は命題値であり、各 `mx` に対する等式 `v .fst ≡ col (toDom x mx)` も、`V` が集合であるため命題である。したがって、この依存和は追加の選択データをもたない。
```agda
isPropFib : (x v : S) → isProp (Fib x v)
isPropFib x v = isPropΣ (isPropMem x) (λ mx → setIsSet (v .fst) (col (toDom x mx)))
```
したがって、`x` と `v` の符号化された順序対が `colTable` に属すれば、切り詰められていない情報が得られる。すなわち `x` は `D` に属し、`v` の基礎集合は `x` が表示する添字での崩壊値に等しいという情報である。`Fib x v` が命題であるため、グラフの読み出しに含まれる切り詰めを除去できる。
```agda
colTable-pair : (x v : S) → Holds colTable x v → Fib x v
colTable-pair = CT.pair-out
```