Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ宇宙レベル ℓ と、レベル ℓ-suc ℓ における排中律を固定する。以下の分出から最後に用いる平方律まで、すべての構成はこの一つの名づけられた仮定に相対的であり、最終的な列の上界もまったく同じ仮定をもつ。
module L.GCH.FiniteSequenceCoding {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
有限なパラメータ列を数えるには、その列を集める集合が L の内部に存在しなければならない。本章ではまず、構成可能集合上のすべての有限列を一つの構成可能集合に集める。次に無限順序数 α に対し、α × α から α への内部の符号化された単射を用いて列を項ごとに畳み込み、最後に長さをタグとして付け、列の集合から α への内部単射を示す。この結論は上界だけを与える。α のすべての要素を覆うことも、α 全体で定義された復号写像を与えることもない。
この構成で用いる古典性は、明示された排中律の仮定だけから来る。とくに、命題的に切り詰められた証人は、一意性によって証人型そのものが命題になる場合を除いて、切り詰められたままである。列の表現や単射のグラフを任意に選ぶための選択原理は用いない。
open import Cubical.HITs.PropositionalTruncation using ( rec2 )
以下では、同じ対象について二つの記述を行き来する。対象言語の水準では、等号、連言、有界および非有界の量化によって、L の内部の列のグラフと再帰の軌跡を記述する。ホストの水準では、提示によって集合の要素を小さな添字として扱い、正則性は後で平方律を支える整礎的な議論に用いられる。
符号化は、二つの剛直な集合符号の族に依存する。順序対の符号の単射性により、対の符号の等しさから二つの座標を復元でき、フォン・ノイマン数項は自然数とその順序を ω の内部で忠実に記録する。構成可能性の推移性により、構成可能な順序数の各要素も L にとどまるので、これらの周囲の符号を構成可能モデルの要素として使える。
ここで用いる集合論的グラフは、L の内部の一階推論から読めなければならない。分出によって正確な部分集合を作り、対、グラフの適用、定義域、環境についての妥当性が、各対象言語の節を底集合間の意図された関係と同一視する。この橋によって、後でホスト側の再帰的な畳み込みを内部の定義可能なグラフへ移せる。
有限列は、数項をちょうど定義域とする環境のグラフとして表す。各固定長について、環境集合の構成はそのようなグラフだけを集め、要素から表現を読み戻す向きは命題的に切り詰められている。それでも、グラフの論理式の出力が一意なら、再帰の仕組みは実際の値を与える。さらに、符号化された単射の合成によって、得られた上界を構成可能集合の間で移せる。
最後の数え上げでは、与えられた無限順序数がすでに基数であると仮定する必要はない。まず基数代表へ移り、そこで平方律を用いて対を圧縮し、もとの順序数へ合成して戻す。本章は、その対の圧縮から有限列の定義可能な単射を構成する。
長さは自然数、位置は Fin n の要素、内部の定義域の標識は数項として表す。この三つの見方の間を移るには、toℕ i < n のような順序の事実と、n 未満の自然数から有限添字を作り直す逆変換が必要である。付随する所属の証明は命題なので、依存対の等しさはデータの成分によって決まる。
open import Cubical.Data.Nat.Order
using ( _<_; ≤-refl; ≤-suc; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-split; zero-≤ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
単射性の証明では、後続数未満の添字について、前の数未満である場合と最後の添字である場合を繰り返し分ける。命題外延性は二つの所属の含意を集合の等しさへ変え、累積階層はこの議論を行う集合とその標準的な提示を与える。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
フォン・ノイマン数項とその後続演算は、有限な長さを内部集合 ω と結び付ける。不可能な有限上界は空型で表す。整礎帰納法が現れるのは、後で平方律から対の圧縮を構成するときだけであり、与えられた有限列を畳み込む初等的な再帰には用いない。
using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV; #_ )
import Cubical.Induction.WellFounded as WF
命題的切り詰めは、ある表現が存在することを記録しつつ、どの表現が与えられたかを意図的に忘れる。その除去則を使うのは、集合の所属や等しさのように、目標自身が命題である場合だけである。この制限により、長さ、割り当て、内部グラフを暗黙に選ぶことなく、存在と単射性を証明できる。
周囲の水準では、所属は命題値である。切り詰められた証人を所属の主張へ除去するとき、この点が効く。データは何も選ばれず、所属が成り立つという事実だけが残る。
open hPropView 𝒮ᵥ using ( _∈ˢ_ )
周囲の累積階層上の命題値構造を SV と書く。これは、順序対の符号、数項、集合論的グラフを構成可能な対象として見る前に比較するための、外側の所属概念を与える。
module SV = hPropView 𝒮ᵥ using ()
構成可能構造 SL の台を S と書く。S の要素は、周囲の集合と、それが L に属すことの証拠からなる。したがって、内部単射で用いる列の集合、グラフ、順序数には、いずれも実際の構成可能な代表がある。
module SL = hPropView 𝒮ʟ using ( S; _∈ˢ_ )
open SL using ( S )
S の定数を含む論理式は構成可能構造で評価され、その原子的な内容は周囲の集合へ射影して読むこともできる。L の推移性により二つの読み方が一致するので、対象言語のグラフ条件から、畳み込みで用いる周囲の所属の等式を得られる。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )
数項 nn k は、周囲のフォン・ノイマン数項とその構成可能性の証明をまとめたものである。数項は有限環境の正確な定義域を示し、零の数項は畳み込みの初期累積値と ext の範囲外での無意味な既定値にもなり、長さの数項は完了した畳み込みにタグを付ける。これらの役割によって、有限添字を構成可能モデルの内部で扱える。
nn : ℕ → S
nn k = # k , numL k
集合上のすべての有限列を集める
A の上の列とは、ホストの水準では、有限順序数から A の提示への関数である。小さな索引型は、長さとそのような関数の対を集める。これはホストの水準の概念であり、集合で符号化された対応物は、この後で定義される。
SeqIx : S → Type ℓ
SeqIx A = Σ[ n ∶ ℕ ] Ix A n
小さな定義域の原理は、A の上のすべての有限長の環境グラフを含む、一つの構成可能な集合を与える。これは共通の容器にすぎない。正確な集合は後の分出で刻まれ、この容器がちょうどその像であるとは主張しない。
private
amb : (A : S) → S
amb A = smallDom (SeqIx A) (λ p → envS A (p .snd)) .fst
特定の長さ n と割り当て g に対し、グラフ envS A g は共通の容器に属する。この包含が分出による所属の外側の半分を与え、定義論理式が有限環境であるという正確な条件を与える。
amb-in : (A : S) (p : SeqIx A) → ⟨ (envS A (p .snd)) .fst ∈ˢ (amb A) .fst ⟩
amb-in A = smallDom (SeqIx A) (λ p → envS A (p .snd)) .snd
この一変数論理式は、候補 x が A 上の環境のグラフであり、その定義域が内部の ω のある要素であることを述べる。したがって、有界な証人について最初に分かるのは ω に属すことだけである。そこから実際の自然数の長さを復元するのは後の段階であり、その結果も命題的に切り詰められている。
seqFo : S → Formula S 1
seqFo A = ∃̇∈ (con ωʟ) (∃̇ ( (var zero ≐ con A)
∧̇ envOverAt (suc (suc zero)) (suc zero) zero ))
ここで分出を用いて、共通の容器に含まれる余分な要素を除く。得られる集合 seqL A は、容器の要素のうち有限環境の記述を満たすものをちょうど含む。定義を不透明に保つことは正規化にだけ影響し、数学的内容は続く所属の等式によって完全に定まる。
opaque
seqL : S → S
seqL A = hasSeparationL (amb A) (seqFo A) .fst .fst
ある要素が seqL A に属すのは、それが共通の容器に属し、かつ seqFo A を満たすとき、そしてそのときに限る。容器は集合としての大きさを保証し、論理式は正確さを保証する。どちらか一方だけでは、すべての有限列の集合を特徴づけられない。
seqL-spec : (A x : S) → (x SL.∈ˢ seqL A)
≡ ((x SL.∈ˢ amb A) ⊓ ((x ∷ []) ⊨ seqFo A))
seqL-spec A = hasSeparationL (amb A) (seqFo A) .fst .snd
長さ n の環境集合のすべての要素は seqL A に属する。証明は、その要素の切り詰められた提示を読み、その後に分出された集合の中へ導入する。
seqL-in : (A : S) (n : ℕ) (x : S)
→ ⟨ x .fst ∈ˢ (envSet A n) .fst ⟩ → ⟨ x .fst ∈ˢ (seqL A) .fst ⟩
seqL-in A n x hx = rec₁ ((x .fst ∈ˢ (seqL A) .fst) .snd) from (envSet-out A n x hx)
where
from : Σ[ g ∶ Ix A n ] (x .fst ≡ (envS A g) .fst) → ⟨ x .fst ∈ˢ (seqL A) .fst ⟩
その要素はグラフの形へ運ばれ、界定の記録によって容器の中にある。そして、正準な項目によって記述が充足される。
from (g , e) = subst (λ w → ⟨ w ∈ˢ (seqL A) .fst ⟩) (sym e) canonical
where
canonical : ⟨ (envS A g) .fst ∈ˢ (seqL A) .fst ⟩
canonical = subst ⟨_⟩ (sym (seqL-spec A (envS A g)))
( amb-in A (n , g)
記述の証人は、長さの数項、内部の ω への所属、そして A の上の環境のグラフの関係からなり、すべて切り詰められた存在の中にまとめられる。
, ∣ nn n , (#∈ω n , ∣ A , (refl , envOver A g) ∣₁) ∣₁ )
逆に、seqL A への所属から得られるのは、ある自然数の長さ n が存在し、その要素が envSet A n に属すという命題的に切り詰められた主張だけである。分出の等式のうち容器の成分を捨て、定義論理式から存在情報を読み取るが、すべての要素に対して長さを一様に選ぶわけではない。
seqL-out : (A x : S) → ⟨ x .fst ∈ˢ (seqL A) .fst ⟩
→ ∥ Σ[ n ∶ ℕ ] ⟨ x .fst ∈ˢ (envSet A n) .fst ⟩ ∥₁
seqL-out A x hx = rec₁ squash₁ step1 (subst ⟨_⟩ (seqL-spec A x) hx .snd)
where
step2 : (d : S) (k : ℕ) → # k ≡ d .fst
切り詰められた証人の一つの分岐の中で、定義域の対象 d が数項 # k と、基礎の対象 b が A と同一視され、x が環境条件を満たすとする。これらの固定された証人に対して、復元過程は長さ k の割り当てを構成し、x をそのグラフと同一視する。外側の結果は再び切り詰められるので、この局所的な構成は大域的な復号写像を定めない。
→ Σ[ b ∶ S ] ((b .fst ≡ A .fst)
× ⟨ (b ∷ d ∷ x ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩)
→ ∥ Σ[ n ∶ ℕ ] ⟨ x .fst ∈ˢ (envSet A n) .fst ⟩ ∥₁
step2 d k q (b , eb , hov) =
∣ k , subst (λ w → ⟨ w ∈ˢ (envSet A k) .fst ⟩) (sym R.recovers) (envSet-in A R.g) ∣₁
長さ k を固定すると、環境の各条件がそれぞれの項目を一意に定める。正確な定義域が切り詰められた存在を与え、一価性が項目のファイバーを命題にし、値の制限が復元された値を A の提示に置く。さらに、グラフのすべての要素が対の形をもつという条件も用い、外延性によって集合 x 全体を標準的な環境のグラフと同一視する。
where
module R = Recover A k (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero
(sym q) eb hov using ( g; recovers )
残りの段階は、定義域の ω への所属を消去する。ω の要素は、単に、ある数項である。
step1 : Σ[ d ∶ S ] (⟨ d .fst ∈ˢ ω ⟩
× ∥ Σ[ b ∶ S ] ((b .fst ≡ A .fst)
× ⟨ (b ∷ d ∷ x ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩) ∥₁)
→ ∥ Σ[ n ∶ ℕ ] ⟨ x .fst ∈ˢ (envSet A n) .fst ⟩ ∥₁
step1 (d , d∈ω , h) = rec₁ squash₁
数項が変換の一歩に渡され、読みの方向が完成する。強さに注意してほしい。長さと環境は切り詰めの中でだけ復元され、seqL A から割り当てへの大域的な復号器が作られるわけではない。
(λ { (k , q) → rec₁ squash₁ (step2 d (lower k) q) h }) d∈ω
有限列を一つの順序数コードへ畳み込む
符号化のモジュールは、対の関数のデータを固定する。引数は、順序数 α、α が ω に属さないこと、すなわちこの章が使う形での無限性の仮定、そして構成可能なグラフ F と、一価性・積の上の全域性・単射性という三つの節である。
module Code (α : S) (oα : IsOrd (α .fst)) (α∉ω : ⟨ α .fst ∈ˢ ω ⟩ → ⊥₀)
(F : S)
(sv : ⟨ (F ∷ prodL α ∷ []) ⊨ svAt zero ⟩)
(dm : ⟨ (F ∷ prodL α ∷ []) ⊨ domAt zero (suc zero) ⟩)
(ij : ⟨ (F ∷ prodL α ∷ []) ⊨ injAt zero ⟩)
(ran : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩
→ ⟨ y .fst ∈ α .fst ⟩) where
最後の仮定は、メタレベルの形での値域の条件である。グラフに記録されたすべての値は α に属する。四つの節合わせて、F が積 α × α から α への内部の符号化された単射であることを言う。
入力と値の台は、構成可能な集合と α への所属の対の型である。積の項目も、すべての値も、α の中になければならない。
M : Type (ℓ-suc ℓ)
M = Σ[ v ∶ S ] ⟨ v .fst ∈ˢ α .fst ⟩
数項は台の要素になる。α が ω に属さないため、α の無限性がすべての数項を α の中に置くからである。これが、畳み込みにおける無限性の仮定の唯一の用途である。
num : ℕ → M
num k = nn k , ω⊆ (α .fst) oα α∉ω (# k) (#∈ω k)
α の提示の索引も台の要素になる。構成可能性は α の所属に沿って運ばれ、所属は提示によって証明される。
up : ⟪ α .fst ⟫ → M
up m = (⟪ α .fst ⟫↪ m , isL-trans (member (α .fst) m) (α .snd)) , member (α .fst) m
一価性と正確な定義域の条件を合わせると、グラフ F を prodL α の要素上の実際のホスト関数として読める。定義域への所属から最初に得られる出力は切り詰められているが、可能な出力のファイバーは命題なので、その一意な値を取り出せる。等しい出力から入力の等しさを結論するには、別の仮定 ij がなお必要である。
module E = Extract F (prodL α) sv dm using ( toFun; toFun-graph; toFun-inj )
台の二つの要素の符号化された対は積の中にある。両方の座標が α の中にあり、対の演算がそれを prodL α への所属に変えるからである。
opaque
pairMem : (a u : M) → ⟨ (prʟ (a .fst) (u .fst)) .fst ∈ˢ (prodL α) .fst ⟩
pairMem a u = subst (λ w → ⟨ w ∈ˢ (prodL α) .fst ⟩) (sym (prʟ-fst (a .fst) (u .fst)))
(prodL-in α (a .fst) (u .fst) (a .snd) (u .snd))
prodL α に属すことが分かっている入力 x に対し、val x を F が x に記録する一意な出力と定める。所属の証明も入力データに含めるのは、グラフが全域的であると要求されるのがちょうどこの積の上だけであり、すべての構成可能集合の上ではないからである。
opaque
val : (x : S) → ⟨ x .fst ∈ˢ (prodL α) .fst ⟩ → S
val x mx = E.toFun (x , mx)
グラフの記録は、入力と値の順序対が F に属することを述べる。これが、後の同一視の補題が消費するデータである。
val-graph : (x : S) (mx : ⟨ x .fst ∈ˢ (prodL α) .fst ⟩)
→ ⟨ pr (x .fst) ((val x mx) .fst) ∈ F .fst ⟩
val-graph x mx = E.toFun-graph (x , mx)
グラフは積の上で単射である。同じ値をもつ二つの点は、底の集合が等しくなる。抽出と合わせて、これが対の関数の単射の半分である。
val-inj : (x : S) (mx : ⟨ x .fst ∈ˢ (prodL α) .fst ⟩)
(x' : S) (mx' : ⟨ x' .fst ∈ˢ (prodL α) .fst ⟩)
→ (val x mx) .fst ≡ (val x' mx') .fst → x .fst ≡ x' .fst
val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')
二項演算 app a u は、a と u の内部順序対におけるグラフ F の値を取る。その値はグラフのファイバーから得られるので、すでに構成可能集合である。さらに値域の条件が、その値が α に属すことを証明する。したがって app は台 M 上で閉じている。
opaque
app : M → M → M
app a u = val (prʟ (a .fst) (u .fst)) (pairMem a u)
, ran (prʟ (a .fst) (u .fst)) (val (prʟ (a .fst) (u .fst)) (pairMem a u))
(val-graph (prʟ (a .fst) (u .fst)) (pairMem a u))
値を取り出しても、内部グラフとのつながりは失われない。定理 app-graph は、(a,u) の周囲の対符号を入力とし、app a u を出力とする順序対が F に属すことを記録する。構成可能な対の射影等式が、二つの入力符号の間に必要な同一視を与える。
app-graph : (a u : M)
→ ⟨ pr (pr ((a .fst) .fst) ((u .fst) .fst)) (((app a u) .fst) .fst) ∈ F .fst ⟩
app-graph a u = subst (λ w → ⟨ pr w (((app a u) .fst) .fst) ∈ F .fst ⟩)
(prʟ-fst (a .fst) (u .fst))
(val-graph (prʟ (a .fst) (u .fst)) (pairMem a u))
二つの適用の出力が等しければ、まず F の単射性によって、それらの符号化された対入力が同一視される。次に順序対符号の単射性が、この等しさを二つの第一座標の等しさと二つの第二座標の等しさへ分ける。したがって、F の逆関数を構成せずに、適用を一層ずつ剥がせる。
app-inj : (a u a' u' : M) → ((app a u) .fst) .fst ≡ ((app a' u') .fst) .fst
→ ((a .fst) .fst ≡ (a' .fst) .fst) × ((u .fst) .fst ≡ (u' .fst) .fst)
app-inj a u a' u' e = pr-inj
(sym (prʟ-fst (a .fst) (u .fst))
∙ val-inj (prʟ (a .fst) (u .fst)) (pairMem a u) (prʟ (a' .fst) (u' .fst)) (pairMem a' u') e
対入力の比較では、構成可能な対符号から周囲のクラトフスキー対符号へ移り、さらに戻る。これらの輸送の後、対の単射性が app-inj に必要な二つの成分の等しさをちょうど与える。付随する所属の証明を比較する必要はない。
∙ prʟ-fst (a' .fst) (u' .fst))
対になる一意性の事実は、グラフを順方向に用いる。F が入力対 (a,u) にある値 w を記録しているなら、w はすでに取り出した値 app a u と等しくなければならない。これはグラフの一価性であり、異なる入力の間の単射性とは独立である。
app-uniq : (a u : M) (w : S)
→ ⟨ pr (pr ((a .fst) .fst) ((u .fst) .fst)) (w .fst) ∈ F .fst ⟩
→ w .fst ≡ ((app a u) .fst) .fst
app-uniq a u w h =
svAt-out zero (F ∷ prodL α ∷ []) sv (prʟ (a .fst) (u .fst)) w ((app a u) .fst)
一価性を適用するため、まず与えられた所属を周囲の対符号から val が用いる構成可能な対へ輸送する。次に、それを抽出された値についての標準的な所属 val-graph と比較する。二つの項目は同じ入力をもつので、一価性の条件がそれらの出力を同一視する。
(subst (λ z → ⟨ pr z (w .fst) ∈ F .fst ⟩) (sym (prʟ-fst (a .fst) (u .fst))) h)
(val-graph (prʟ (a .fst) (u .fst)) (pairMem a u))
環境の読みは、数項の上の全域的な関数へ延長される。列の範囲の外では数項のゼロを返す。この既定の値に数学的な意味はなく、後の使用はすべて、長さより下の索引でだけこの延長を読む。
ext : (n : ℕ) → (Fin n → ⟪ α .fst ⟫) → ℕ → M
ext 0 g k = num zero
ext (suc n) g 0 = up (g zero)
ext (suc n) g (suc k) = ext n (λ i → g (suc i)) k
索引についての再帰により、長さより下のどの索引でも、延長は列のその項目をちょうど読み戻す。
ext-at : (n : ℕ) (g : Fin n → ⟪ α .fst ⟫) (i : Fin n) → ext n g (toℕ i) ≡ up (g i)
ext-at (suc n) g zero = refl
ext-at (suc n) g (suc i) = ext-at n (λ j → g (suc j)) i
長さ n と列 g を固定すると、chain n g k は段階数 k についての再帰で定義される。初期値は零の数項であり、k<n を満たす各段階では、対の関数を次の項 g(k) とそれまでの累積値に適用する。したがって chain n g n は列の n 個の項をちょうどすべて消費する。この範囲を越えた後の振る舞いは ext の無意味な既定値だけに依存し、列の符号の数学的内容には含まれない。
chain : (n : ℕ) → (Fin n → ⟪ α .fst ⟫) → ℕ → M
chain n g 0 = num zero
chain n g (suc k) = app (ext n g k) (chain n g k)
長さ n の列では、畳み込みは vₙ = chain n g n で終わる。その符号を F(n,vₙ) と定める。最後の対の第一座標が長さの数項、第二座標が畳み込み値である。n と g が与えられれば、これは実際の値を与える。α のすべての要素が符号であるとも、α 全体上の復号写像があるとも述べていない。
code : (n : ℕ) → (Fin n → ⟪ α .fst ⟫) → M
code n g = app (num n) (chain n g n)
二つの畳み込みの鎖が k 段後に一致すると仮定すると、各位置 j<k の項も一致する。帰納は鎖を後ろ向きにたどる。段階 k+1 での等しさを F の単射性で分けると、段階 k で用いた項の等しさと、一つ前の鎖の値の等しさが得られる。
chain-inj : (n : ℕ) (g g' : Fin n → ⟪ α .fst ⟫) (k : ℕ)
→ ((chain n g k) .fst) .fst ≡ ((chain n g' k) .fst) .fst
→ (j : ℕ) → j < k → ((ext n g j) .fst) .fst ≡ ((ext n g' j) .fst) .fst
chain-inj n g g' 0 e j j<0 = ⊥₀-rec (¬-<-zero j<0)
chain-inj n g g' (suc k) e j j<sk = go (<-split j<sk)
後者段階では、app-inj がこの二つの等しさを与える。j=k なら第一の等しさが求める項の等しさであり、j<k なら第二の等しさによって短い鎖へ帰納仮定を適用できる。これは既知の正しい二つの畳み込みの間の消去論法であり、α の任意の要素を列へ変える手続きではない。
where
q = app-inj (ext n g k) (chain n g k) (ext n g' k) (chain n g' k) e
go : (j < k) ⊎ (j ≡ k) → ((ext n g j) .fst) .fst ≡ ((ext n g' j) .fst) .fst
go (inl j<k) = chain-inj n g g' k (q .snd) j j<k
go (inr j≡k) = subst (λ j → ((ext n g j) .fst) .fst ≡ ((ext n g' j) .fst) .fst) (sym j≡k) (q .fst)
ここで長さのタグが役割を果たす。二つの符号が等しければ、外側の適用の単射性からまず長さの数項が等しく、したがって自然数としての長さも等しいことが分かる。共通の長さへ輸送した後、畳み込みを後ろ向きに消去すると各項が一致し、二つの環境グラフの底集合も等しくなる。ここで述べるのはこの向きだけである。
code-inj : (n : ℕ) (g : Fin n → ⟪ α .fst ⟫) (n' : ℕ) (g' : Fin n' → ⟪ α .fst ⟫)
→ ((code n g) .fst) .fst ≡ ((code n' g') .fst) .fst
→ (envS α g) .fst ≡ (envS α g') .fst
code-inj n g n' g' e = subst P (#-inj′ (q .fst)) same g' (q .snd)
where
対になった結論 q は、符号の等式を数項座標の等しさと終端の畳み込み値の等しさに分ける。族 P m は、長さ m の列について残る主張を正確に記録する。これにより、数項の単射性に沿って第二の列とその畳み込みの等式をもとの長さ n へ輸送できる。
q = app-inj (num n) (chain n g n) (num n') (chain n' g' n') e
P : ℕ → Type (ℓ-suc ℓ)
P m = (h : Fin m → ⟪ α .fst ⟫)
→ ((chain n g n) .fst) .fst ≡ ((chain m h m) .fst) .fst
→ (envS α g) .fst ≡ (envS α h) .fst
長さが一致すれば、環境グラフの等しさは関数外延性から従う。各有限添字 i について、α の提示における対応する二要素を比較する。提示の埋め込みの単射性により、その等しさは二つの鎖から得た底集合の等しさへ帰着する。
same : P n
same h e' = cong (λ (f : Fin n → ⟪ α .fst ⟫) → (envS α f) .fst) (funExt pt)
where
pt : (i : Fin n) → g i ≡ h i
pt i = ↪-inj {a = α .fst}
位置 i での比較では、まず ext-at によって全域関数 ext n g の有界位置での値を本来の項 g i と同一視する。toℕ i<n なので鎖の消去補題から二つの全域関数の値が等しいと分かり、もう一度 ext-at を用いて他方を h i と同一視する。この範囲外での ext の値には数学的な意味を持たせない。
( sym (cong (λ z → (z .fst) .fst) (ext-at n g i))
∙ chain-inj n g h n e' (toℕ i) (toℕ<n i)
∙ cong (λ z → (z .fst) .fst) (ext-at n h i) )
再帰の一回の遷移を意味論的に記述するため、添字対象 i を固定する。StepAt s C i は、j が i の後者であり、列のグラフが s(i)=a、軌跡が C(i)=u と C(j)=w、グラフ F が F(a,u)=w を与えるような対象 j,a,u,w を記録するだけである。このデータ全体は命題的に切り詰められている。
StepAt : (s C i : S) → Type (ℓ-suc ℓ)
StepAt s C i = ∥ Σ[ j ∶ S ] Σ[ a ∶ S ] Σ[ u ∶ S ] Σ[ w ∶ S ]
( (j .fst ≡ sucV (i .fst))
× ⟨ pr (i .fst) (a .fst) ∈ s .fst ⟩
× ⟨ pr (i .fst) (u .fst) ∈ C .fst ⟩
最後の所属の主張は、漸化式をグラフの事実として書いたものである。入力は順序対 (a,u)、出力は w である。したがって StepAt は、後の一階のステップ論理式が表すべきホスト側の意味であり、復号写像や大域的な軌跡の選択を加えるものではない。
× ⟨ pr (j .fst) (w .fst) ∈ C .fst ⟩
× ⟨ pr (pr (a .fst) (u .fst)) (w .fst) ∈ F .fst ⟩ ) ∥₁
DomIs s n は、n が列のグラフ s のちょうど定義域であることを述べる。各 x∈n には (x,y)∈s となる値 y があり、逆に (x,y)∈s なら第一座標 x は n に属する。値の存在は命題的切り詰めのもとでだけ保たれ、一意性が必要な箇所では別の環境条件を用いる。
DomIs : (s n : S) → Type (ℓ-suc ℓ)
DomIs s n = (x : S)
→ (⟨ x .fst ∈ n .fst ⟩ → ∥ Σ[ y ∶ S ] ⟨ pr (x .fst) (y .fst) ∈ s .fst ⟩ ∥₁)
× ((y : S) → ⟨ pr (x .fst) (y .fst) ∈ s .fst ⟩ → ⟨ x .fst ∈ n .fst ⟩)
EnvC m C は、C が α に値を取り、ちょうど m を定義域とする環境であることを述べる。envOverAt には、一価性、定義域の条件、すべての値が α に属すこと、そして C の各要素が順序対であることが含まれる。ここで m は列の長さの後者になるので、軌跡は 0 から n までの位置をもつ。
EnvC : (m C : S) → Type (ℓ-suc ℓ)
EnvC m C = ⟨ (α ∷ m ∷ C ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩
完全な意味論的証人は、数項 n∈ω、その後者 m、軌跡の環境 C から始まる。s の定義域が n、C の定義域が m で値が α に属し、軌跡が C(0)=0 から始まることを要求する。各 i∈n について一つの遷移を与え、最後に C(n) の値を n と対にすると y になることを記録する。この証人は命題的に切り詰められている。
Wit : (y s : S) → Type (ℓ-suc ℓ)
Wit y s = ∥ Σ[ n ∶ S ] Σ[ m ∶ S ] Σ[ C ∶ S ]
( ⟨ n .fst ∈ ω ⟩
× (m .fst ≡ sucV (n .fst))
× DomIs s n
最後の成分は、軌跡の終端値と長さのタグを分けて記録する。ある v について (n,v)∈C かつ F(n,v)=y を与える。遷移の条件が v を n 回の畳み込み後の値として決定し、最後の F の適用が長さを記録するため、長さの異なる列が同じ符号をもつことはない。
× EnvC m C
× ⟨ pr (# zero) (# zero) ∈ C .fst ⟩
× ((i : S) → ⟨ i .fst ∈ n .fst ⟩ → StepAt s C i)
× ∥ Σ[ v ∶ S ] ( ⟨ pr (n .fst) (v .fst) ∈ C .fst ⟩
× ⟨ pr (pr (n .fst) (v .fst)) (y .fst) ∈ F .fst ⟩ ) ∥₁ ) ∥₁
量化子を入れ子にすると、それまで使えた各変数の de Bruijn 位置がずれる。略記 i0,i1,… はこれらの位置を一様に表し、i0 が直前に束縛された変数、後者を一回取るごとに一つ外側の変数を指す。この記法により、以下の論理式は各出現がどの対象を指すかを保ったまま有限軌跡の等式を述べられる。
private
i0 : ∀ {k} → Fin (suc k)
i0 = zero
i1 : ∀ {k} → Fin (suc (suc k))
i1 = suc i0
i0 から i4 までの名前は、現在の添字、その後者、一回の漸化段階で導入される近くの値など、軌跡論理式の浅い部分を扱う。長さについて多相的なので、さらに束縛子を加えた後も同じ位置名を再利用できる。
i2 : ∀ {k} → Fin (suc (suc (suc k)))
i2 = suc i1
i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
i3 = suc i2
i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
次の位置は、いくつかの存在証人を導入した後にも、軌跡の環境ともとの自由変数へ届く。そのため同じ論理式の中で、古い軌跡値、新しい軌跡値、両者を結ぶ列の項を同時に指せる。
i4 = suc i3
i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
i5 = suc i4
i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
i6 = suc i5
ステップ論理式は全部で五つの証人を導入する。後者添字 j、値 a,u,w、そして (a,u) の対の符号である。五つの束縛子の内側では、もとの列変数は位置 i12 まで移る。この深い添字は束縛の深さから生じるもので、新たな数学的仮定ではない。
i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
i7 = suc i6
i8 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))
i8 = suc i7
i12 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))))))
具体的に、i12 は i8 からさらに四回後者を取った位置である。位置名を固定したので、以下の定義では後者構成子を一段ずつ数えず、各変数の数学的役割を追える。
i12 = suc (suc (suc (suc i8)))
論理式 stepFo は StepAt の対象言語での表現である。まず j を選び、それが現在の添字 i の後者であると述べる。次に列の値 a、古い軌跡値 u、新しい軌跡値 w、順序対 (a,u) の符号を選ぶ。
opaque
private
stepFo : Formula S 8
stepFo = ∃̇ (
sucAtL i1 i0
内側の四つの存在量化子は a,u,w とその対の符号を束縛する。最初の三つの適用条件はそれぞれ s(i)=a、C(i)=u、C(j)=w を述べ、対の条件は補助符号を (a,u) と同一視する。これらが論理式の中心にある一つの漸化条件を準備する。
∧̇ (∃̇ (∃̇ (∃̇ (∃̇ (
appAt i12 i5 i3
∧̇ appAt i8 i5 i2
∧̇ appAt i8 i4 i1
∧̇ prAtL i0 i3 i2
最も内側の連言項は、漸化式を表すグラフの事実である。補助的な入力符号に F を適用すると、新しい値 w が得られると述べる。その直前の対の条件が、この補助符号を順序対 (a,u) と同一視する。二つの条件を合わせて、対象言語で畳み込みの等式 F(a,u)=w を表す。
∧̇ appC F i0 i1 ))))))
最終長の論理式はこう言う。符号化された環境の数項の枠に値があり、数項とその値に符号化された対を適用すると出力になる、と。
finFo : Formula S 7
finFo = ∃̇ (∃̇ (
appAt i4 i6 i1
∧̇ prAtL i0 i6 i1
∧̇ appC F i0 i7 ))
本体は軌跡の条件を述べる前に、二つの補助パラメータを明示的に保つ。b を固定したアルファベット α、z を零の数項と同一視し、続いて m が選んだ長さ n の後者であると述べる。これらの等式により、後の一般的な環境と適用の論理式を α と 0 に特殊化できる。
body : Formula S 7
body =
(var i1 ≐ con α)
∧̇ (var i0 ≐ con (nn zero))
∧̇ sucAtL i4 i3
残りの連言項は、定義域の条件、環境の上の条件、零の項目の等式、n 未満のすべての遷移、そして最終長の条件を課す。現在名前の付いている対象について、これらは C が符号化された対を通して初期の零から出力へ至る有限な軌跡であることを述べる。その後で fo の外側の量化子が、そのような長さと軌跡の存在を主張する。
∧̇ domAt i6 i4
∧̇ envOverAt i2 i3 i1
∧̇ appAt i2 i0 i0
∧̇ ∀̇∈ (var i4) stepFo
∧̇ finFo
完全なグラフの論理式は、ωʟ の上の有界量化子で数項を束縛し、つづいて入れ子の存在量化子で四つの補助の対象を束縛して、出力と列の上の二つの枠の論理式を作る。
fo : Formula S 2
fo = ∃̇∈ (con ωʟ) (∃̇ (∃̇ (∃̇ (∃̇ body))))
環境 e7 は、stepFo と finFo の内側の量化子へ入る前に利用できる七つの対象を含む。de Bruijn 順では z,b,C,m,n,y,s であり、位置零は補助的な零、もとの出力と列は最も外側の二位置にある。後の束縛子はこの環境の先頭を拡張する。
private
e7 : S → S → S → S → S → S → S → Vec S 7
e7 y s n m C b z = z ∷ b ∷ C ∷ m ∷ n ∷ y ∷ s ∷ []
stepFo を外向きに読むため、その命題的に切り詰められた証人を命題 StepAt s C i へ除去する。これにより j,a,u,w と補助的な対の符号、さらに後者条件、三つのグラフ適用条件、対の条件、F の適用条件が得られる。補助的な対の符号は、その等式を使った後には残らない。
stepOut : (y s n m C b z i : S)
→ ⟨ (i ∷ e7 y s n m C b z) ⊨ stepFo ⟩ → StepAt s C i
stepOut y s n m C b z i = rec₁ squash₁ (λ { (j , (ej , ha)) →
rec₁ squash₁ (λ { (a , hu) → rec₁ squash₁ (λ { (u , hw) →
rec₁ squash₁ (λ { (w , hp) → rec₁ squash₁ (λ { (p , (h1 , (h2 , (h3 , (h4 , h5))))) →
各妥当性の等式は、一つの充足判断を意図された等式またはグラフ所属へ輸送する。得られた事実は j を i の後者と同一視し、s から a、C から u,w を読み取る。最後の F に関するグラフの事実と合わせると、ちょうど StepAt が要求する意味論的な形になる。
let γ = p ∷ w ∷ u ∷ a ∷ j ∷ i ∷ e7 y s n m C b z in
∣ j , a , u , w
, ( subst ⟨_⟩ (sucAtL-adequate i1 i0 (j ∷ i ∷ e7 y s n m C b z)) ej
, subst ⟨_⟩ (appAt-adequate i12 i5 i3 γ) h1
, subst ⟨_⟩ (appAt-adequate i8 i5 i2 γ) h2
対についての妥当性の等式は、補助対象を順序対 (a,u) と同一視する。その等式に沿って F の適用の事実を輸送すると、漸化式を表す所属 ((a,u),w)∈F が得られる。これで一階のステップ論理式から一回の意味論的遷移への外向きの読み取りが完了する。
, subst ⟨_⟩ (appAt-adequate i8 i4 i1 γ) h3
, subst (λ q → ⟨ pr q (w .fst) ∈ F .fst ⟩)
(subst ⟨_⟩ (prAtL-adequate i0 i3 i2 γ) h4)
(subst ⟨_⟩ (appC-adequate F i0 i1 γ) h5) ) ∣₁ }) hp }) hw }) hu }) ha })
finFo を外向きに読むと、まず軌跡の終端値 v と補助対象 q が得られる。三つの条件は C(n)=v、q=(n,v)、F(q)=y を述べる。目標は命題的に切り詰められているので、二つの存在証人を除去し、Wit に必要な v と二つのグラフの事実だけを残せる。
finOut : (y s n m C b z : S) → ⟨ e7 y s n m C b z ⊨ finFo ⟩
→ ∥ Σ[ v ∶ S ] ( ⟨ pr (n .fst) (v .fst) ∈ C .fst ⟩
× ⟨ pr (pr (n .fst) (v .fst)) (y .fst) ∈ F .fst ⟩ ) ∥₁
finOut y s n m C b z = rec₁ squash₁ (λ { (v , hq) →
rec₁ squash₁ (λ { (q , (h1 , (h2 , h3))) →
妥当性により、三つの条件は C(n)=v と F(q)=y を表す所属、および等式 q=(n,v) へ移される。最後の等式に沿って F への所属を輸送し、q を (n,v) で置き換えると、グラフの形で F(n,v)=y が得られる。
let γ = q ∷ v ∷ e7 y s n m C b z in
∣ v , ( subst ⟨_⟩ (appAt-adequate i4 i6 i1 γ) h1
, subst (λ r → ⟨ pr r (y .fst) ∈ F .fst ⟩)
(subst ⟨_⟩ (prAtL-adequate i0 i6 i1 γ) h2)
(subst ⟨_⟩ (appC-adequate F i0 i7 γ) h3) ) ∣₁ }) hq })
本体には八つの連言項がある。最初の二つは補助対象を b=α、z=0 と同一視し、残る六つは m=n+1、s の正確な定義域、C の環境条件、C(0)=0、n 未満のすべての遷移、最後の長さ付きの値を述べる。別に与えられた n∈ω と合わせると、これらが Wit y s を構成する。
bodyOut : (y s n m C b z : S) → ⟨ n .fst ∈ ω ⟩
→ ⟨ e7 y s n m C b z ⊨ body ⟩ → Wit y s
bodyOut y s n m C b z n∈ω (eb , (ez , (em , (hd , (hE , (h0 , (hS , hF))))))) =
∣ n , m , C
, ( n∈ω
後者論理式の妥当性の等式から m=n+1 が得られ、domAt の二つの読み方から s の正確な定義域について両方向の所属が得られる。さらに b=α を用い、環境の論理式を補助的な基礎集合 b から固定した α へ輸送する。軌跡全体の等しさは必要ない。
, subst ⟨_⟩ (sucAtL-adequate i4 i3 (e7 y s n m C b z)) em
, (λ x → domAt-in i6 i4 (e7 y s n m C b z) hd x
, domAt-out i6 i4 (e7 y s n m C b z) hd x)
, envOverAt-transport (e7 y s n m C b z) (α ∷ m ∷ C ∷ [])
i2 i3 i1 (suc (suc zero)) (suc zero) zero refl refl eb hE
等式 z=0 によって、本体の条件 C(z)=z は初期条件 C(0)=0 へ移される。有界全称の条件は stepOut によって各点で読まれ、finOut がタグ付きの終端値を与える。これらが命題的に切り詰められた証人の残りの成分である。
, subst (λ w → ⟨ pr w w ∈ C .fst ⟩) ez
(subst ⟨_⟩ (appAt-adequate i2 i0 i0 (e7 y s n m C b z)) h0)
, (λ i i∈n → stepOut y s n m C b z i (hS i i∈n))
, finOut y s n m C b z hF ) ∣₁
完全な論理式の外向きの読み出しは、五重の入れ子の存在量化子を一つずつ消去し、それぞれを本体の読み出しに渡して、完全な証人が組み立てられるまで続ける。
fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
fo-out y s = rec₁ squash₁ (λ { (n , (n∈ω , hm)) →
rec₁ squash₁ (λ { (m , hC) → rec₁ squash₁ (λ { (C , hb) →
rec₁ squash₁ (λ { (b , hz) → rec₁ squash₁ (λ { (z , hbody) →
bodyOut y s n m C b z n∈ω hbody }) hz }) hb }) hC }) hm })
逆向きの構成は、命題的に切り詰められた一つの StepAt 証人を stepFo の充足へ写すことから始まる。代表 j,a,u,w に対し、その対の符号と四つの値で環境を拡張する。続く条件が、後者と各グラフに関する主張を対象言語の形で組み立て直す。
private
stepIn : (y s n m C i : S) → StepAt s C i
→ ⟨ (i ∷ e7 y s n m C α (nn zero)) ⊨ stepFo ⟩
stepIn y s n m C i = map₁ (λ { (j , a , u , w , (ej , ha , hu , hw , hF)) →
let γ = prʟ a u ∷ w ∷ u ∷ a ∷ j ∷ i ∷ e7 y s n m C α (nn zero) in
各証人は stepFo が束縛する順序で導入される。後者と適用に関する妥当性の等式を逆向きに用い、意味論的事実 j=i+1、s(i)=a、C(i)=u、C(j)=w を対応する充足判断へ移す。既にある証人を導入するだけで、命題的切り詰めから選択するのではないため、入れ子の切り詰めは保たれる。
j , ( subst ⟨_⟩ (sym (sucAtL-adequate i1 i0 (j ∷ i ∷ e7 y s n m C α (nn zero)))) ej
, ∣ a , ∣ u , ∣ w , ∣ prʟ a u
, ( subst ⟨_⟩ (sym (appAt-adequate i12 i5 i3 γ)) ha
, ( subst ⟨_⟩ (sym (appAt-adequate i8 i5 i2 γ)) hu
, ( subst ⟨_⟩ (sym (appAt-adequate i8 i4 i1 γ)) hw
標準的な構成可能な対 prʟ a u が、補助的な対変数の証人になる。対についての妥当性がその底集合を (a,u) と同一視し、所属 ((a,u),w)∈F を輸送すると、必要な対象言語の適用条件が得られる。これで一回の遷移の内向きの読み取りが完了する。
, ( subst ⟨_⟩ (sym (prAtL-adequate i0 i3 i2 γ)) (prʟ-fst a u)
, subst ⟨_⟩ (sym (appC-adequate F i0 i1 γ))
(subst (λ q → ⟨ pr q (w .fst) ∈ F .fst ⟩) (sym (prʟ-fst a u)) hF) )))) ∣₁ ∣₁ ∣₁ ∣₁ ) })
finFo の内向きの読み取りは、C(n)=v かつ F(n,v)=y を満たす、命題的に切り詰められた終端値 v から始まる。この証人を finFo の二つの存在量化子へ写す。一つは v、もう一つは順序対 (n,v) の明示的な符号を束縛する。
finIn : (y s n m C : S)
→ ∥ Σ[ v ∶ S ] ( ⟨ pr (n .fst) (v .fst) ∈ C .fst ⟩
× ⟨ pr (pr (n .fst) (v .fst)) (y .fst) ∈ F .fst ⟩ ) ∥₁
→ ⟨ e7 y s n m C α (nn zero) ⊨ finFo ⟩
finIn y s n m C = map₁ (λ { (v , (hv , hy)) →
環境を v と標準的な対 prʟ n v で拡張する。適用の妥当性を逆向きに用いて C(n)=v を表し、対の妥当性を逆向きに用いて対の証人を同一視し、定数グラフ F への適用の妥当性を逆向きに用いて F(n,v)=y を表す。
let γ = prʟ n v ∷ v ∷ e7 y s n m C α (nn zero) in
v , ∣ prʟ n v
, ( subst ⟨_⟩ (sym (appAt-adequate i4 i6 i1 γ)) hv
, ( subst ⟨_⟩ (sym (prAtL-adequate i0 i6 i1 γ)) (prʟ-fst n v)
, subst ⟨_⟩ (sym (appC-adequate F i0 i7 γ))
最後の輸送は、周囲の順序対 (n,v) を入力とするグラフ所属を、構成可能な代表 prʟ n v を用いた充足へ移す。したがって、命題的切り詰めが既に保持する証人以外を選ぶことなく、終端条件が再構成される。
(subst (λ q → ⟨ pr q (y .fst) ∈ F .fst ⟩) (sym (prʟ-fst n v)) hy) )) ∣₁ })
本体を再構成するため、六つの実質的な軌跡条件を仮定する。すなわち m=n+1、s の正確な定義域、C の環境条件、初期値、すべての有界な遷移、タグ付きの終端値である。本体に残る二つの連言項は固定された同一視 b=α と z=0 であり、追加の仮定を必要としない。
bodyIn : (y s n m C : S) → m .fst ≡ sucV (n .fst) → DomIs s n → EnvC m C
→ ⟨ pr (# zero) (# zero) ∈ C .fst ⟩
→ ((i : S) → ⟨ i .fst ∈ n .fst ⟩ → StepAt s C i)
→ ∥ Σ[ v ∶ S ] ( ⟨ pr (n .fst) (v .fst) ∈ C .fst ⟩
× ⟨ pr (pr (n .fst) (v .fst)) (y .fst) ∈ F .fst ⟩ ) ∥₁
選んだ七対象の環境では、二つの補助項目は定義上そのまま α と 0 である。したがって本体の最初の二つの連言項は反射律で証明される。残りの証明は、与えられた六つの意味論的条件を残る六つの対象言語の連言項へ移す。
→ ⟨ e7 y s n m C α (nn zero) ⊨ body ⟩
bodyIn y s n m C em hd hE h0 hS hF =
let γ = e7 y s n m C α (nn zero) in
refl
, ( refl
後者についての妥当性を逆向きに用いると、m=n+1 を表す連言項が得られる。domAt の導入方向は DomIs の二方向を組み合わせる。グラフ値の存在が命題的に切り詰められているため一方では命題への除去を用い、他方はもともと直接の含意である。続いて環境条件を選ばれた変数位置へ輸送する。
, ( subst ⟨_⟩ (sym (sucAtL-adequate i4 i3 γ)) em
, ( domAt-intro i6 i4 γ (λ x →
rec₁ ((x .fst ∈ n .fst) .snd) (λ { (yy , p) → hd x .snd yy p })
, hd x .fst)
, ( envOverAt-transport (α ∷ m ∷ C ∷ []) γ
初期の所属 C(0)=0 は、適用の妥当性を通して第六の連言項を与える。n 未満の各遷移は stepIn によって内向きに送られ、finIn が最後のタグ付きの値の条件を再構成する。先の五つの事実と合わせて、有限軌跡の本体にある八つの連言項がすべて完成する。
(suc (suc zero)) (suc zero) zero i2 i3 i1 refl refl refl hE
, ( subst ⟨_⟩ (sym (appAt-adequate i2 i0 i0 γ)) h0
, ( (λ i i∈n → stepIn y s n m C i (hS i i∈n))
, finIn y s n m C hF ))))))
完全な論理式の内向きの読み出しは、切り詰められた証人を消去し、五つの対象を五重の入れ子の存在量化子を通して注入して、グラフの論理式の対象言語の充足を組み立てる。
fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
fo-in y s = rec₁ (((y ∷ s ∷ []) ⊨ fo) .snd)
(λ { (n , m , C , (n∈ω , em , hd , hE , h0 , hS , hF)) →
∣ n , ( n∈ω
, ∣ m , ∣ C , ∣ α , ∣ nn zero
五つの証人は n,m,C,α,0 である。最初のものは ω 上の有界存在量化子、残る四つは通常の存在量化子を通して導入される。固定した α と 0 によって本体の最初の二等式は反射律で成り立ち、bodyIn が後者、定義域、環境、初期値、遷移、終端の条件を与える。したがって fo-in は、切り詰められた証人から大域的に代表を選ぶことなく、完全な充足を再構成する。
, bodyIn y s n m C em hd hE h0 hS hF ∣₁ ∣₁ ∣₁ ∣₁ ) ∣₁ })
次に、この意味論的論理式を実際の有限列に適用する。長さ N、割り当て g : Fin N → α、構成可能集合 s、そして s の底集合を環境グラフ envS α g と同一視する等式を固定する。以下では、この表現された列について論理式の出力が存在し一意であることを示す。
module AtSeq (N : ℕ) (g : Fin N → ⟪ α .fst ⟫) (s : S) (e : s .fst ≡ (envS α g) .fst) where
標準的な環境グラフについて一般的な環境論理式を使うには、基礎集合 α、長さの数項 N、envS α g の三対象で十分である。δ における de Bruijn 順では、グラフが位置二、数項が位置一、基礎集合が位置零に置かれる。
private
δ : Vec S 3
δ = α ∷ nn N ∷ envS α g ∷ []
標準グラフ envS α g は、α に値を取り、N を定義域とする環境であることが既に分かっている。この環境の事実から定義域の条件を取り出すと、その正確な定義域が数項 #N であることが示される。後でこの事実により、同じ列に対するどの別の証人も同じ有限長を使うことが強制される。
dom0 : ⟨ δ ⊨ domAt (suc (suc zero)) (suc zero) ⟩
dom0 = envOver-dom (suc (suc zero)) (suc zero) zero δ (envOver α g)
環境の参照定理を使うには、まず割り当てを V の集合族として見る。写像 gV は各有限添字を、表示要素 g i が名指す底集合へ送る。g i は α の要素を表示しているので、これはその添字に記録される値そのものである。
gV : Fin N → V ℓ
gV i = ⟪ α .fst ⟫↪ (g i)
k < N なら、正準な環境は、第一成分が数項 # k、第二成分が列の第 k 項である順序対を含む。証明では k を Fin N の要素に直し、そこで参照の仕様を適用して、得られた所属を自然数の添字へ戻す。
extMem : (k : ℕ) (p : k < N)
→ ⟨ pr (# k) (((ext N g k) .fst) .fst) ∈ (envS α g) .fst ⟩
extMem k p = subst (λ k → ⟨ pr (# k) (((ext N g k) .fst) .fst) ∈ (envS α g) .fst ⟩)
(toFromId' N k p)
(subst ⟨_⟩ (sym (lookup-spec gV i (((ext N g (toℕ i)) .fst) .fst)))
等式 ext-at は、全域化された参照 ext N g (toℕ i) を本来の項 g i と同一視する。続いて、有界な自然数と Fin N の間の往復等式により、添字と表示された値の両方が元の k に戻る。
(cong (λ z → (z .fst) .fst) (ext-at N g i)))
where
i : Fin N
i = fromℕ' N k p
逆向きの参照は、各有効添字での単値性を表す。k < N のとき環境が (# k,a) を含むなら、a の底集合は実際の第 k 項の底集合に等しく、その添字に別の値を記録することはできない。
s-uniq : (k : ℕ) (p : k < N) (a : S)
→ ⟨ pr (# k) (a .fst) ∈ (envS α g) .fst ⟩
→ a .fst ≡ ((ext N g k) .fst) .fst
s-uniq k p a ha =
subst ⟨_⟩ (lookup-spec gV i (a .fst))
この同一視は、対応する Fin N の添字で行う。参照等式がまず a を決定し、ext-at が全域化された項を元の割り当ての項に戻し、変換の恒等式が結論を k へ運ぶ。
(subst (λ k → ⟨ pr (# k) (a .fst) ∈ (envS α g) .fst ⟩) (sym (toFromId' N k p)) ha)
∙ sym (cong (λ z → (z .fst) .fst) (ext-at N g i))
∙ cong (λ k → ((ext N g k) .fst) .fst) (toFromId' N k p)
where
i : Fin N
ここで i = fromℕ' N k p は、境界 p : k < N によって正当化される有限添字である。この境界を明示することが大切である。全域関数 ext は、この範囲の外では列としての意味をもたない。
i = fromℕ' N k p
畳み込みには、初期値から N 個すべての項を処理した後の状態まで、N + 1 個の状態がある。各状態にはすでに α への所属証明があり、fiber はその所属を表示要素へ変えて、Fin (suc N) で添字づけられた割り当て h を作る。
h : Fin (suc N) → ⟪ α .fst ⟫
h i = fiber (α .fst) ((chain N g (toℕ i)) .snd) .fst
族 hV は表示添字を忘れて、それらが名指す V の底集合へ戻る。後で使うファイバー等式により、これらが h のもとになった畳み込み状態そのものであることが分かる。
hV : Fin (suc N) → V ℓ
hV i = ⟪ α .fst ⟫↪ (h i)
この状態割り当ての環境グラフを C とする。その定義域の長さは N + 1 で、k 番目には列の最初の k 項を処理した後の畳み込み状態が記録される。k = 0 の初期状態と k = N の最終状態も含まれる。
C : S
C = envS α h
各 k < N + 1 に対し、chainMem は期待されるグラフ項 (# k, chain N g k) が C に属することを示す。元の列の場合と同様に、対応する Fin (suc N) の要素へ移り、環境の参照仕様を使う。
chainMem : (k : ℕ) (p : k < suc N)
→ ⟨ pr (# k) (((chain N g k) .fst) .fst) ∈ C .fst ⟩
chainMem k p = subst (λ k → ⟨ pr (# k) (((chain N g k) .fst) .fst) ∈ C .fst ⟩)
(toFromId' (suc N) k p)
(subst ⟨_⟩ (sym (lookup-spec hV i (((chain N g (toℕ i)) .fst) .fst)))
ファイバー等式は h i が名指す値を実際の畳み込み状態と同一視し、toFromId' は元の自然数添字を復元する。この二つの同一視によってグラフへの所属が証明され、N + 1 の外の添字については何も主張しない。
(sym (fiber (α .fst) ((chain N g (toℕ i)) .snd) .snd)))
where
i : Fin (suc N)
i = fromℕ' (suc N) k p
固定した等式 e : s .fst ≡ (envS α g) .fst により、正準な環境についての事実を、表示される列 s に使える。inS は envS α g の正準なグラフ項を s へ運ぶ。
inS : (k : ℕ) (a : S) → ⟨ pr (# k) (a .fst) ∈ (envS α g) .fst ⟩ → ⟨ pr (# k) (a .fst) ∈ s .fst ⟩
inS k a = subst (λ w → ⟨ pr (# k) (a .fst) ∈ w ⟩) (sym e)
逆向きの輸送 outS は、s の任意のグラフ項を envS α g へ戻す。一意性の議論では、任意の証人となる連鎖が与える項を実際の割り当ての項と比較するために、この向きを使う。
outS : (k : ℕ) (a : S) → ⟨ pr (# k) (a .fst) ∈ s .fst ⟩ → ⟨ pr (# k) (a .fst) ∈ (envS α g) .fst ⟩
outS k a = subst (λ w → ⟨ pr (# k) (a .fst) ∈ w ⟩) e
ここで正準な符号がグラフ論理式を満たすことを確かめる。証人には有限長の数項 # N、その後続 #(N+1)、状態環境 C を選ぶ。残りの成分は、s の定義域、α に値をとる状態列、零の初期状態、各遷移、最後の対グラフの適用を証明する。
wit : Wit ((code N g) .fst) s
wit = ∣ nn N , nn (suc N) , C
, ( #∈ω N
, refl
, domIs
最後の存在節は、状態 chain N g N によって証される。この状態は C の添字 N に現れ、長さの数項とこの状態の対に F を適用すると code N g が得られる。存在の主張全体は命題的に切り詰められたままである。
, envOver α h
, chainMem zero (suc-≤-suc zero-≤)
, step
, ∣ (chain N g N) .fst
, ( chainMem N ≤-refl , app-graph (num N) (chain N g N) ) ∣₁ ) ∣₁
s の定義域が # N であることを示すため、まず # N の添字を取る。正準な環境はその添字で単に存在する値を与え、e に沿ってグラフへの所属を運ぶと、その順序対が s に属することが得られる。
where
domIs : DomIs s (nn N)
domIs x =
(λ m → map₁ (λ { (yy , p) → yy , subst (λ w → ⟨ pr (x .fst) (yy .fst) ∈ w ⟩) (sym e) p })
(domAt-in (suc (suc zero)) (suc zero) δ dom0 x m))
逆に、s が第一成分 x の順序対を含むなら、それを正準な環境へ戻す。その環境の既知の定義域から x ∈ # N が従い、定義域の特徴づけの両方向がそろう。
, (λ yy p → domAt-out (suc (suc zero)) (suc zero) δ dom0 x yy
(subst (λ w → ⟨ pr (x .fst) (yy .fst) ∈ w ⟩) e p))
集合論的な添字 i ∈ # N に数項の除去を使うと、その数項が i に等しい自然数 k < N が得られる。遷移の証人には、後続の数項、列の実際の第 k 項、k と k+1 における畳み込み状態を選ぶ。
step : (i : S) → ⟨ i .fst ∈ # N ⟩ → StepAt s C i
step i i∈N = rec₁ squash₁ (λ { (k , p , ei) →
∣ nn (suc k) , (ext N g k) .fst , (chain N g k) .fst , (chain N g (suc k)) .fst
, ( cong sucV (sym ei)
, subst (λ w → ⟨ pr w (((ext N g k) .fst) .fst) ∈ s .fst ⟩) (sym ei)
必要な遷移の事実は、二つの正準な環境と畳み込みの定義式から得られる。列の項は s に属し、隣り合う二状態はともに C に属し、app-graph は項と旧状態の対を F が新状態へ送ることを記録する。輸送は # k を最初に与えられた添字 i へ戻すためだけに使われる。
(inS k ((ext N g k) .fst) (extMem k p))
, subst (λ w → ⟨ pr w (((chain N g k) .fst) .fst) ∈ C .fst ⟩) (sym ei)
(chainMem k (≤-suc p))
, chainMem (suc k) (suc-≤-suc p)
, app-graph (ext N g k) (chain N g k) ) ∣₁ }) (∈#-elim N (i .fst) i∈N)
存在だけでは、まだ fo は関数グラフにならない。定理 only は、Wit y s が認めるどの出力 y も、正準な符号と同じ底集合をもつことを示す。この等式は命題なので、命題的に切り詰められた証人を除去してから一意性の議論を進められる。
only : (y : S) → Wit y s → y .fst ≡ ((code N g) .fst) .fst
only y = rec₁ (setIsSet (y .fst) (((code N g) .fst) .fst))
(λ { (n , m , C' , (n∈ω , em , hd , hE , h0 , hS , hF)) →
Only.final n m C' n∈ω em hd hE h0 hS hF })
where
長さの対象を n、その後続を m、状態環境を C' とする任意の証人を固定する。仮定は、s の定義域が n であること、C' が長さ m で α に値をとる環境であること、初期項が零であること、n より下の各畳み込み段階に従うこと、終状態を n と対にすると y が得られることを述べる。
module Only (n m C' : S) (n∈ω : ⟨ n .fst ∈ ω ⟩) (em : m .fst ≡ sucV (n .fst))
(hd : DomIs s n) (hE : EnvC m C')
(h0 : ⟨ pr (# zero) (# zero) ∈ C' .fst ⟩)
(hS : (i : S) → ⟨ i .fst ∈ n .fst ⟩ → StepAt s C' i)
(hF : ∥ Σ[ v ∶ S ] ( ⟨ pr (n .fst) (v .fst) ∈ C' .fst ⟩
終端節 hF は、状態 v が単に存在し、それが C' の添字 n に記録され、n とともに F で y へ写されることを述べる。終状態を大域的に選ぶものではなく、後では出力の一意性を述べる集合の等式へだけ除去する。
× ⟨ pr (pr (n .fst) (v .fst)) (y .fst) ∈ F .fst ⟩ ) ∥₁)
where
証人の長さ n は、集合として正準な数項 # N に等しくなければならない。どちらも同じ列 s の定義域を表し、hd は任意の証人から、dom0 は選んだ表示 s = envS α g からその記述を与える。外延性により、この等式は所属の二つの含意へ帰着する。
n≡ : n .fst ≡ # N
n≡ = cong (λ p → p .fst) (extensionalL {a = n} {b = nn N} (λ x → ⇔toPath (fwd x) (bwd x)))
where
fwd : (x : S) → ⟨ x .fst ∈ n .fst ⟩ → ⟨ x .fst ∈ # N ⟩
fwd x x∈n = rec₁ ((x .fst ∈ # N) .snd)
順方向では、x ∈ n と hd から、第一成分が x である順序対が s に単に存在することが得られる。その対を正準な環境へ運び、既知の定義域を読むと x ∈ # N が従う。
(λ { (yy , p) → domAt-out (suc (suc zero)) (suc zero) δ dom0 x yy
(subst (λ w → ⟨ pr (x .fst) (yy .fst) ∈ w ⟩) e p) })
(hd x .fst x∈n)
bwd : (x : S) → ⟨ x .fst ∈ # N ⟩ → ⟨ x .fst ∈ n .fst ⟩
bwd x x∈N = rec₁ ((x .fst ∈ n .fst) .snd)
逆方向では、x ∈ # N から正準な環境の項が得られる。それを s へ運ぶと、hd の逆向きの部分から x ∈ n が従う。したがって、各列の表示を選ぶことなく、その定義域から長さを復元できる。
(λ { (yy , p) → hd x .snd yy (subst (λ w → ⟨ pr (x .fst) (yy .fst) ∈ w ⟩) (sym e) p) })
(domAt-in (suc (suc zero)) (suc zero) δ dom0 x x∈N)
C' は環境条件を満たすので単値である。したがって、C' に属する二つの順序対の第一成分が同じなら、第二成分の底集合は等しくなる。この事実を用いて、C' が記録する任意の状態を、畳み込み方程式が定める状態と比較する。
svC : (x v v' : S) → ⟨ pr (x .fst) (v .fst) ∈ C' .fst ⟩ → ⟨ pr (x .fst) (v' .fst) ∈ C' .fst ⟩
→ v .fst ≡ v' .fst
svC = svAt-out (suc (suc zero)) (α ∷ m ∷ C' ∷ [])
(envOver-sv (suc (suc zero)) (suc zero) zero (α ∷ m ∷ C' ∷ []) hE)
中心となる帰納命題は、各 k < N + 1 について、C' が添字 k に記録するどの値も正準な畳み込み状態 chain N g k に等しいというものである。k = 0 では、初期節と C' の単値性により、両方の値が零に定まる。
entry : (k : ℕ) → k < suc N → (v : S)
→ ⟨ pr (# k) (v .fst) ∈ C' .fst ⟩ → v .fst ≡ ((chain N g k) .fst) .fst
entry 0 p v hv = svC (nn zero) v (nn zero) hv h0
entry (suc k) p v hv = rec₁ (setIsSet (v .fst) (((chain N g (suc k)) .fst) .fst))
(λ { (j , a , u , w , (ej , ha , hu , hw , hFw)) →
後続の場合、遷移の証人は列の項 a、旧状態 u、新状態 w を与える。正準な列の参照によって a は第 k 入力に等しく、帰納法の仮定によって u は正準な旧状態に等しくなる。すると F の機能性から、w は正準な新状態に等しいと分かる。
let ea : a .fst ≡ ((ext N g k) .fst) .fst
ea = s-uniq k p' a (outS k a ha)
eu : u .fst ≡ ((chain N g k) .fst) .fst
eu = entry k (≤-suc p') u hu
ew : w .fst ≡ ((chain N g (suc k)) .fst) .fst
後続添字の境界から k < N が得られるので、段階の節を使える。この節は w を C' の後続添字に置く。単値性がまず最初に与えられた値 v を w と同一視し、先の適用についての議論が w を chain N g (suc k) と同一視する。
ew = app-uniq (ext N g k) (chain N g k) w
(subst (λ q → ⟨ pr q (w .fst) ∈ F .fst ⟩) (cong₂ pr ea eu) hFw)
in svC (nn (suc k)) v w hv
(subst (λ z → ⟨ pr z (w .fst) ∈ C' .fst ⟩) ej hw) ∙ ew })
(hS (nn k) (subst (λ z → ⟨ # k ∈ z ⟩) (sym n≡) (#mono k N p')))
前者の境界は帰納法に必要な小さな算術事実である。suc k < suc N から k < N を得る。これにより、第 k 入力が実際の項であり、k での畳み込み段階が列の範囲内にあることが保証される。
where
p' : k < N
p' = pred-≤-pred p
残るのは、与えられた出力 y を決定することである。命題的に切り詰められた終端の証人を除去すると、証人の長さ n に記録された状態 v が得られる。底集合の等式 n≡ : n .fst ≡ # N でこの所属を添字 N へ運ぶと、帰納法の結論が v を正準な最終畳み込み状態と同一視する。
final : y .fst ≡ ((code N g) .fst) .fst
final = rec₁ (setIsSet (y .fst) (((code N g) .fst) .fst))
(λ { (v , (hv , hy)) →
let hv' : ⟨ pr (# N) (v .fst) ∈ C' .fst ⟩
hv' = subst (λ z → ⟨ pr z (v .fst) ∈ C' .fst ⟩) n≡ hv
終端節はさらに、F が n .fst と v .fst からなる対を y の底集合 y .fst へ写すことを述べる。これらの入力を # N と正準な最終状態に置き換えると、F の機能性から y .fst ≡ ((code N g) .fst) .fst が得られる。これはグラフ論理式を満たす出力の一意性だけを示し、α の任意の要素に対する復号関数を定義するものではない。
ev : v .fst ≡ ((chain N g N) .fst) .fst
ev = entry N ≤-refl v hv'
in app-uniq (num N) (chain N g N) y
(subst (λ q → ⟨ pr q (y .fst) ∈ F .fst ⟩) (cong₂ pr n≡ ev) hy) })
hF
述語 Mem s は、s が seqL α に属するという意味である。したがって、以後の構成の対象は有限な α 値環境グラフに限られ、周囲の宇宙の任意の要素ではない。
Mem : S → Type (ℓ-suc ℓ)
Mem s = ⟨ s .fst ∈ˢ (seqL α) .fst ⟩
s の表示とは、自然数の長さ n、割り当て g : Ix α n、s が g の環境グラフに等しいことが、単に存在するという内容である。命題的切り詰めによって、どの表示がデータを与えたかは意図的に忘れられ、長さや割り当てを大域的に選ぶことはない。
Rep : S → Type (ℓ-suc ℓ)
Rep s = ∥ Σ[ n ∶ ℕ ] Σ[ g ∶ Ix α n ] (s .fst ≡ (envS α g) .fst) ∥₁
s ∈ seqL α から、seqL-out はまず、s が対応する環境集合に属するような有限長が単に存在することを与える。その環境集合の逆向きの特徴づけから、割り当てと必要なグラフ等式が単に存在することが得られ、Rep s が成立する。
rep : (s : S) → Mem s → Rep s
rep s m = rec₁ squash₁
(λ { (n , hn) → map₁ (λ { (g , e) → n , g , e }) (envSet-out α n s hn) })
(seqL-out α s m)
これでグラフ論理式から seqL α 上の関数を得られる。具体的な各表示 (n,g,e) から、候補 (code n g) .fst と、それが s 上のグラフのファイバーを一意に占めることの証明が得られる。切り詰められた表示を、この命題的に切り詰められた一意存在の主張へ写せば、mereFunct への入力になる。mereFunct は優先する表示を選ぶことなく、それを必要な可縮性へ変換する。
R : Recursion
R = record
{ dom = seqL α
; graph = fo
; funct = λ s m → mereFunct fo s (map₁ (λ { (n , g , e) →
各表示について、fo-in は正準な符号がグラフのファイバーに属することを示す。別の y' も同じファイバーに属するなら、fo-out がその充足証明を証人へ変え、AtSeq.only が正準な符号と同一視する。構成可能性の証明は命題なので、底集合の等式から証明つき要素の等式が得られる。
(code n g) .fst
, ( fo-in ((code n g) .fst) s (AtSeq.wit n g s e)
, λ y' h → Σ≡Prop (λ v → (isL v) .snd) (AtSeq.only n g s e y' (fo-out y' s h)) ) })
(rep s m)) }
定義可能な関数的関係についての一般定理から、一意な値を与える演算が得られる。ここでは関数値と、fo を満たすどの出力もその値に等しいという原理を取り出す。内部単射の構成に必要なのはこの二つである。
module T = Of R using ( funct; val; val-uniq )
列の要素 s に対するこの一意な値を fn s m と定める。記法には所属証明 m が含まれるが、所属は命題値なので、数学的な値は異なる証明の選び方に依存しない。
fn : (s : S) → Mem s → S
fn = T.val
s が長さ n の割り当て g で表示されるなら、S の要素としての符号値 (code n g) .fst は fo を満たす。したがってグラフ値の一意性から fn s m ≡ (code n g) .fst が得られる。この比較は与えられたどの表示についても成り立つので、優先する表示を選ぶ必要はない。
fn-code : (s : S) (m : Mem s) (n : ℕ) (g : Ix α n) → s .fst ≡ (envS α g) .fst
→ fn s m ≡ (code n g) .fst
fn-code s m n g e = T.val-uniq s m ((code n g) .fst) (fo-in ((code n g) .fst) s (AtSeq.wit n g s e))
fn の値は α の内部にとどまる。目標となる所属は命題なので、命題的に切り詰められた表示を除去できる。各代表 (n,g) については、code n g の第二成分が α への所属を証し、fn-code がその事実を fn s m へ運ぶ。
into : (s : S) (m : Mem s) → ⟨ (fn s m) .fst ∈ˢ α .fst ⟩
into s m = rec₁ (((fn s m) .fst ∈ˢ α .fst) .snd)
(λ { (n , g , e) → subst (λ w → ⟨ w .fst ∈ˢ α .fst ⟩) (sym (fn-code s m n g e)) ((code n g) .snd) })
(rep s m)
これらの事実から、seqL α から α への DefinableMap が得られる。このレコードは、ホスト側の関数と、その値が終域に属することの証明を一階論理式 fo とともに保持する。defines は選ばれた値が論理式を満たすことを示し、only は論理式を満たすどの出力もその値であることを示す。続いて単射性を証明すると、Inj の構成がこの定義可能性のデータを用いて、L の中に実際の関数グラフを作る。
D : DefinableMap
D = record
{ dom = seqL α ; cod = α ; fn = fn ; into = into ; graph = fo
; defines = λ s m → T.funct s m .fst .snd
; only = λ s m y h → sym (T.val-uniq s m y h) }
単射性を示すため、二つの列の要素が同じ fn の値をもつと仮定する。それぞれの表示は命題的に切り詰められているが、求める底集合の等式も命題なので、両方の切り詰めを除去して任意の代表 (n,g) と (n',g') を比較できる。
inj : (s : S) (m : Mem s) (s' : S) (m' : Mem s')
→ (fn s m) .fst ≡ (fn s' m') .fst → s .fst ≡ s' .fst
inj s m s' m' e = rec2 (setIsSet (s .fst) (s' .fst))
(λ { (n , g , es) (n' , g' , es') →
es
等式 fn-code により、二つの fn の値の等しさは二つの正準な符号の等しさへ変わる。先に示した code-inj から対応する環境グラフの等しさが得られ、二つの表示等式と合成すると s .fst ≡ s' .fst となる。これは正しい符号どうしを比較する証明であり、α 全体で定義された復号演算ではない。
∙ code-inj n g n' g'
(sym (cong (λ p → p .fst) (fn-code s m n g es)) ∙ e ∙ cong (λ p → p .fst) (fn-code s' m' n' g' es'))
∙ sym es' })
(rep s m) (rep s' m')
定義可能な写像と先の単射性証明から、seqL α から α への内部単射が得られる。結論 InjL は、適切なグラフが L に存在するという命題的に切り詰められた主張である。この写像の全射性も、α の任意の要素を有限列として復号できることも主張しない。
injL : InjL (seqL α) α
injL = Inj.injL D inj
有限列を無限順序数へ単射する
最後の定理では、α 上の対の単射があらかじめ与えられているという一時的な仮定を取り除く。内部単射 prodL α ↪ α を構成すると、その命題的に切り詰められたグラフの証人から、畳み込みに必要な単値性、正確な定義域、単射性、値域の事実が得られ、L の内部で seqL α ↪ α が従う。
seq-count :
(α : SL.S) → IsOrd (α .fst) → (⟨ α .fst ∈ˢ ω ⟩ → ⊥₀)
→ InjL (seqL α) α
seq-count α oα α∉ω = rec₁ squash₁
(λ { (F , sv , dm , ij , ran) → Code.injL α oα α∉ω F sv dm ij ran }) pairing
対の単射を作るため、cardOf α oα が与える基数代表 μ を局所的にだけ取る。この代表は命題的切り詰めのもとで得られるが、目標 InjL (prodL α) α も命題なので、大域的な選択をせず任意の代表について構成できる。
where
pairing : InjL (prodL α) α
pairing = rec₁ squash₁ build (cardOf α oα)
where
build : Σ[ μ ∶ S ]
代表 μ は順序数であり内部の基数でもあり、α と μ の間には両方向の内部単射がある。cardOf は包含 μ ⊆ α も与えるが、この構成では使わない。二つの単射は濃度を両方向から比較するが、μ と α を定義的に同一視するものではない。
( IsOrd (μ .fst) × IsCardinalL μ
× ((z : V ℓ) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩)
× InjL α μ × InjL μ α )
→ InjL (prodL α) α
build (μ , oμ , cardμ , _ , α↪μ , μ↪α) =
必要な対の単射は、合成 α² ↪ μ² ↪ μ ↪ α である。最初の矢印は α ↪ μ を両座標に適用し、中央の矢印は無限な内部基数 μ に対する平方律で、最後の矢印が α へ戻す。したがって平方律は、任意の無限順序数に直接ではなく、基数代表に適用される。
injl-trans (prodL α) (prodL μ) α (prod-inj α μ α↪μ)
(injl-trans (prodL μ) μ α
(WF.WFI.induction regularityV {P = Goal} Step.result (μ .fst) (μ .snd) oμ cardμ μ∉ω)
μ↪α)
where
最後に、平方律が必要とする意味で μ が無限であることを示す。もし μ ∈ ω なら μ は有限順序数であるが、与えられた内部単射 α ↪ μ は無限順序数 α をそこへ単射することになる。no-fin は、α と μ の順序数性および α の無限性を用いてこれを排除する。
μ∉ω : ⟨ μ .fst ∈ˢ ω ⟩ → ⊥₀
μ∉ω h = no-fin α μ oα α∉ω oμ h α↪μ
{-# OPTIONS --cubical --safe --guardedness #-}open import Base.Preludeopen import Base.Classical using ( LEM )open import FOL.ZFStructure using ( module hPropView )open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_; ∀̇∈; ∃̇∈ )import FOL.Absolutenessopen import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV )open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd )open import L.Ordinal {ℓ} using ( #∈ω; ∈#-elim )open import L.Axioms.Basic {ℓ} using ( extensionalL )open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOver-sv; envOver-dom; envOverAt-transport )open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate )open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract )open import L.Coding.Environment {ℓ} using ( lookup-spec )open import L.Coding.EnvironmentSet {ℓ} lem
using ( Ix; envS; envOver; envSet; envSet-in; envSet-out; module Recover )open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct; smallDom )open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )open import L.InjectionComposition {ℓ} lem using ( injl-trans )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )open import L.GCH.CardinalSquareLaw {ℓ} lem
using ( prodL; prodL-in; Goal; module Step; prod-inj; no-fin; ω⊆ )