```agda
module PairFo (φ : Formula S 2) where
```
## 順序対の論理式
値と添字の関係として読む二変数の論理式 `φ` を固定する。モジュール `PairFo` は別の二変数の論理式を作る。順序対の候補 `e` と添字 `p` に対し、`φ(z,p)` を満たす値 `z` が存在し、`e` が順序対 `pr(p,z)` であることを述べる。
```agda
ρ : Fin 2 → Fin 3
ρ zero = zero
ρ (suc zero) = suc (suc zero)
```
改名写像は、`φ` の二つの自由変数が存在量化子の下でどこに現れるかを記録する。値の変数は位置 0 に残って量化子に束縛され、添字の変数は位置 2 へ移る。`pairFo` は不透明なので、以後は定義を展開せず、証明された意味論的特徴づけを用いる。
```agda
opaque
pairFo : Formula S 2
```
この論理式は、存在量化子の下で二つの主張を連言する。第一は `e` が `p` と量化された値との順序対を符号化すること、第二は改名された `φ` である。したがって、この構文は関数グラフの要素の数学的記述をそのまま表す。
```agda
pairFo = ∃̇ (prAtL (suc zero) (suc (suc zero)) zero ∧̇ renameFo ρ φ)
```
一致の証明は、改名が意図した環境を保つことを確かめる。長い環境 `(z ∷ e ∷ p ∷ [])` では、改名後の値の位置は `z` を、添字の位置は `p` を読み、元の論理式を `(z ∷ p ∷ [])` で読む場合と正確に一致する。
```agda
private
ag : (z e p : S) → Ren.Agrees ρ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ [])
ag z e p zero = refl
ag z e p (suc zero) = refl
```
二つの意味論的等式が外向きの読みを準備する。順序対の論理式の正しさにより、その充足は周囲の等式 `e .fst ≡ pr (p .fst) (z .fst)` と同一視される。改名定理により、改名後の論理式の充足は、値 `z` と添字 `p` における元の `φ` の充足と同一視される。
```agda
at : (z e p : S)
→ ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩
≡ (e .fst ≡ pr (p .fst) (z .fst))
at z e p = cong ⟨_⟩ (prAtL-adequate (suc zero) (suc (suc zero)) zero (z ∷ e ∷ p ∷ []))
gr : (z e p : S)
```
`pairFo` を外向きに読むと、命題的に切り詰められた値 `z` と、順序対の等式および `φ(z,p)` の証明が得られる。内向きにはこれらの輸送を逆に行い、値、等式、グラフの証明から `pairFo` の充足の証人を作る。以下ではこの二つの意味論的方向を用いる。
```agda
→ ⟨ (z ∷ e ∷ p ∷ []) ⊨ renameFo ρ φ ⟩ ≡ ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
gr z e p = cong ⟨_⟩ (Ren.⊨-rename ρ φ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ []) (ag z e p))
pair-out : (e p : S) → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
→ ∥ Σ[ z ∶ S ] ((e .fst ≡ pr (p .fst) (z .fst)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁
pair-out e p = map₁ (λ { (z , (q , h)) →
```
内向きの補題で意味論的同値が完成し、ここから一つの再帰を固定する。もとの定義域と値の関係は保たれる。変わるのは置換へ渡す値だけで、出力そのものから入力と出力の順序対へ変わる。
```agda
z , (transport (at z e p) q , transport (gr z e p) h) })
pair-in : (e p z : S) → e .fst ≡ pr (p .fst) (z .fst) → ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
→ ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
pair-in e p z q h = ∣ z , (transport (sym (at z e p)) q , transport (sym (gr z e p)) h) ∣₁
```
```agda
module Graph (R₀ : Recursion) where
```
## 定義域と値
再帰は、定義域、もとの値のグラフを表す論理式、および定義域の各要素におけるグラフの値ファイバーの可縮性を与える。そこから得られる値を `fn` と記する。局所的な述語 `Mem x` は、`fn` が必要とする基礎の所属の主張である。
```agda
open Of R₀ public using ( dom; graph; funct ) renaming ( val to fn )
Mem : S → Type (ℓ-suc ℓ)
Mem x = ⟨ x .fst ∈ dom .fst ⟩
isPropMem : (x : S) → isProp (Mem x)
isPropMem x = (x .fst ∈ dom .fst) .snd
```
集合への所属は命題値なので、`Mem x` は命題である。したがって、`x` が定義域に属することの任意の二つの証明は等しくなる。この証明無関係性により、値 `fn x m` は選んだ所属の証明に依存しない。
```agda
private
defines : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
defines x m = funct x m .fst .snd
only : (x : S) (m : Mem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
only x m y h = sym (cong (λ p → p .fst) (funct x m .snd (y , h)))
```
可縮性から、もとの値関係について二つの事実が得られる。選ばれた中心は、環境 `(fn x m ∷ x ∷ [])` で論理式 `graph` が満たされることを証明する。収縮は、`x` でこの論理式を満たす他の任意の `y` が `fn x m` に等しいことを証明する。
```agda
module Fo = PairFo graph renaming ( pairFo to fo; pair-out to out; pair-in to into )
fn-irr : (x : S) (m m' : Mem x) → fn x m ≡ fn x m'
fn-irr x m m' = cong (fn x) (isPropMem x m m')
pairOf : (x : S) → Mem x → S
pairOf x m = prʟ x (fn x m)
```
ここで順序対の論理式をもとの値関係に適用する。`Mem x` の証明無関係性から `fn-irr` が得られ、`pairOf x m` は `x` とその値との構成可能な順序対である。その基礎集合は `pr (x .fst) ((fn x m) .fst)` である。
```agda
uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m
uniq x m p h = rec₁ (isSetS p (pairOf x m))
(λ { (z , (e , g)) → Σ≡Prop (λ v → (isL v) .snd)
(e ∙ cong (λ w → pr (x .fst) (w .fst)) (only x m z g) ∙ sym (prʟ-fst x (fn x m))) })
(Fo.out p x h)
```
候補 `p` が `x` で特殊化した順序対の論理式を満たすとする。外向きの補題は、値 `z`、`p` の基礎集合と `pr(x,z)` との等式、および `z` がもとのグラフを満たす証明を単に与える。もとの値の一意性により `z` は `fn x m` と同一視され、得られた等式を合成すると `p ≡ pairOf x m` が従う。
```agda
R : Recursion
R = record
{ dom = dom
; graph = Fo.fo
; funct = λ x m →
```
## 関数グラフを集める
もとの定義域を保ち、順序対の論理式を値関係とする新しい再帰を作る。`x` における中心は `pairOf x m` である。内向きの意味論的補題がこの順序対による式の充足を証明し、`uniq` が他のすべての候補はそれと等しいことを証明する。
```agda
( pairOf x m
, Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m) )
, λ { (p , h) → Σ≡Prop (λ w → ((w ∷ x ∷ []) ⊨ Fo.fo) .snd) (sym (uniq x m p h)) } }
module T = Of R using ( table; table-in; table-out )
F : S
```
依存対の収縮は、候補の値とその充足の証明を、選ばれた中心と比較する。第一成分の等式は `uniq` が与え、充足の証明は命題なので、この等式から依存対全体のパスが定まる。これにより、順序対についての正しい `Recursion` が得られる。
```agda
F = T.table
F-in : (x : S) (m : Mem x) → ⟨ pr (x .fst) ((fn x m) .fst) ∈ F .fst ⟩
F-in x m = subst (λ w → ⟨ w ∈ F .fst ⟩) (prʟ-fst x (fn x m))
(T.table-in x (pairOf x m) m
(Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m)))
```
この再帰に置換を適用すると、順序対としての値の値域ができる。この値域が求める関数グラフ `F` である。したがって `F` は `L` の要素であり、そこに入る各要素は、定義域の要素と再帰で定まる値との順序対である。
```agda
F-out : (p : V ℓ) → ⟨ p ∈ F .fst ⟩
→ ∥ Σ[ x ∶ S ] Σ[ m ∶ Mem x ] (p ≡ pr (x .fst) ((fn x m) .fst)) ∥₁
F-out p h = rec₁ squash₁ step (T.table-out pS h)
where
pS : S
```
所属の内向きは置換の仕様から直ちに得られる。定義域の証人 `m` に対し、構成可能な順序対 `pairOf x m` は順序対の論理式を満たすので、置換の値域に属する。`prʟ-fst` に沿って輸送すると、周囲の符号 `pr (x .fst) ((fn x m) .fst)` が `F` の基礎集合に属するという形になる。
```agda
pS = p , isL-trans {x = F .fst} {y = p} h (F .snd)
step : Σ[ x ∶ S ] (Mem x × ⟨ (pS ∷ x ∷ []) ⊨ Fo.fo ⟩)
→ ∥ Σ[ x ∶ S ] Σ[ m ∶ Mem x ] (p ≡ pr (x .fst) ((fn x m) .fst)) ∥₁
step (x , (m , g)) = map₁
(λ { (z , (e , gz)) →
```
外向きには、周囲の集合 `p ∈ F .fst` から始める。構成可能性の下方閉性により、`p` を `L` の要素 `pS` として包む。置換の仕様からまず、添字 `x`、定義域の証明 `m`、および `pS` が順序対の論理式を満たすことが、単に得られる。
```agda
x , m , (e ∙ cong (λ w → pr (x .fst) (w .fst)) (only x m z gz)) })
(Fo.out pS x g)
Fib : S → S → Type (ℓ-suc ℓ)
Fib x y = Σ[ m ∶ Mem x ] (y .fst ≡ (fn x m) .fst)
isPropFib : (x y : S) → isProp (Fib x y)
```
次に意味論的な外向きの補題が第二の切り詰めを開き、値 `z`、順序対の等式、もとの値関係の証明を与える。もとの値の一意性により `z` を `fn x m` に置き換える。その結果、ある定義域の要素 `x` に対して `p` が符号 `pr(x,fn x m)` であることが単に示される。
```agda
isPropFib x y = isPropΣ (isPropMem x) (λ m → setIsSet (y .fst) ((fn x m) .fst))
pair-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → Fib x y
pair-out x y h = rec₁ (isPropFib x y) step (F-out (pr (x .fst) (y .fst)) h)
where
step : Σ[ x' ∶ S ] Σ[ m' ∶ Mem x' ] (pr (x .fst) (y .fst) ≡ pr (x' .fst) ((fn x' m') .fst))
```
## 二つの座標を復元する
`x` と `y` を固定すると、ファイバー `Fib x y` は二つの成分からなる。定義域の証明 `m : Mem x` と、`y` の基礎集合と `fn x m` の基礎集合との等式である。定義域への所属は命題値であり、`V` の等式も命題なので、両方の成分が命題である。したがってファイバー全体も命題である。
```agda
→ Fib x y
step (x' , m' , e) = subst (λ z → Fib z y)
(Σ≡Prop (λ v → (isL v) .snd) (sym (pr-inj e .fst))) (m' , pr-inj e .snd)
γ : Vec S 2
γ = F ∷ dom ∷ []
```
順序対の符号 `pr(x,fst .fst y)` が `F` に属するなら、外向きの特徴づけから `x'`、`m'`、および `pr(x',fst .fst(fn x' m'))` との等式が得られる。`pr` の単射性が両方の座標の等式を与える。入力座標の等式に沿って `m'` を輸送すると `x` が定義域に属する証明となり、出力座標の等式が `Fib x y` の第二成分となる。
```agda
sv : ⟨ γ ⊨ svAt zero ⟩
sv = svAt-in zero γ (λ x y y' p q →
let (m , e) = pair-out x y p
(m' , e') = pair-out x y' q
in e ∙ cong (λ p → p .fst) (fn-irr x m m') ∙ sym e')
```
環境 `γ = F ∷ dom ∷ []` は、単値性と定義域を表す論理式の二つの自由変数に値を割り当てる。単値性を示すため、第一座標が同じ `x` である二つの順序対が `F` に属するとする。それぞれのファイバーから所属の証明 `m`、`m'` と、二つの出力が `fn x m`、`fn x m'` に等しいことが得られる。証明無関係性により二つの関数値が等しくなり、したがって出力も等しくなる。
```agda
dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
dm = domAt-intro zero (suc zero) γ (λ x → fwd x , bwd x)
where
fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (x .fst) (y .fst) ∈ F .fst) ⟩ → Mem x
fwd x = rec₁ (isPropMem x) (λ { (y , p) → (pair-out x y p) .fst })
```
最後に、定義域の論理式を両方向に証明する。`x` が `F` のある順序対の第一座標として現れるなら、`pair-out` がファイバーを返し、そこから `Mem x` の証明が得られる。逆に `m : Mem x` なら、`F-in` により順序対 `pr(x,fn x m)` が `F` に属するので、`x` は第一座標として現れる。したがって、構成した関数グラフの定義域はちょうど `dom` である。
```agda
bwd : (x : S) → Mem x → ⟨ ∃[ y ∶ S ] (pr (x .fst) (y .fst) ∈ F .fst) ⟩
bwd x m = ∣ fn x m , F-in x m ∣₁
```