Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ宇宙レベル ℓ と、構成可能な台に必要なレベルでの排中律の実例を固定する。このモジュール以後の構成はすべて、この一つの古典的パラメータを受け継ぐ。排中律が公理として隠されているわけではない。
module L.GCH.OrderType {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
L で符号化された関係の要素を小さな型で表示すれば、整礎関係を崩壊できる。さらに推移性があれば、個々の崩壊値は順序数となり、したがって L の要素になる。本章はそれらの値を正確な値域 otL に集め、グラフ colTable を別に集めるが、otL の順序数性を定理としてまとめてはいない。三分法を追加して初めて、このグラフは元の領域からその値域への符号化された単射になる。
古典的仮定を明示するのは、後の存在証明で、候補となる点が現在扱う点に先行するかどうかを判定する必要があるからである。整礎再帰そのものはこの判定を必要としない。排中律が使われるのは、関係が成り立つ場合と成り立たない場合に分けて一つの置換関数を定める箇所である。
崩壊は集合論の一階言語の論理式によって特徴づけられる。順序対の所属と等号が原子的な判定を与え、連言、選言、含意、否定、および非有界量化子が表の条件を表す。「すべての先行者について」のような制限は、関係の原子論理式を含意の前件に置いて表し、有界量化子の構成子は使わない。
構成の全体を通して、二つの表示を対応させる必要がある。整礎再帰を使うために D の要素は小さな表示を通して扱い、グラフの項目は累積階層の中で順序対として符号化された集合のまま扱う。表示と順序対符号化の単射性により、後の証明でこれらの表示から元の要素と二つの座標へ戻れる。
証明では、再帰的に定めた値を、L の内部で充足できる論理式へ結び付ける必要がある。整礎再帰が崩壊を作り、再帰グラフがその値と順序対を集合へ集め、符号化の論理式がそれらの対を適用として解釈する。最後に段階についての定理が、各順序数である崩壊値を L の中に置く。
集められたグラフには、二段階の目標がある。まず崩壊を D 上の全域的な一価関係として表さなければならない。その後、三分法のもとで初めて、内部単射に必要な入力の一意性も満たせる。順序対の論理式がグラフを表し、単射の四条件はそれぞれ証明された後に初めて単射符号へまとめられる。
後の一意性証明では、構成可能な集合をその要素によって繰り返し比較する。外延性は所属の点ごとの同値を基礎集合の等しさに変え、命題値の証拠によって、対として作られた構成可能な対象の等しさは証明の取り方に依存しない。そのため、切り詰められた場合分けから恒久的な選択を取り出さずに、等しさを結論できる。
累積階層は、周囲の集合と、その各集合の要素の小さな表示を同時に与える。したがって D の要素は、周囲の集合としても小さな添字としても見ることができ、所属によって二つの見方の間で必要な構成可能性の証拠を渡せる。階層の集合に対する後続操作は、後で順序数である崩壊値をその順序数の次の段階に位置付けるために使われる。
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 )
整礎性は、崩壊を定義して調べるための帰納原理を与える。空の型は不可能な関係の場合を排除し、命題的切り詰めは、後の議論が特定の証人ではなく先行者や表項目の存在だけを必要とするとき、その存在を記録する。
open import Cubical.Induction.WellFounded using ( WellFounded )
構成可能構造の台を S と書く。構造の所属 _∈ˢ_ は L の要素間の所属を表し、後で周囲の階層にある集合の表示を読むために使う小さな所属 _∈ₛ_ とは異なる。
open hPropView 𝒮ʟ using ( S; _∈ˢ_ )
論理式は L が担う構造で解釈する。記法 Vec S n は n 個の構成可能集合からなる環境を表し、γ ⊨ φ は、制限された構成可能構造の内部で環境 γ が論理式 φ を満たすことを表す。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )
階層と構成可能性の述語に isSetClass を適用し、台 S が h-集合であることを得る。これにより、後の切り詰められた場合分けを台の要素の等式へ除去できる。
isSetS : isSet S
isSetS = isSetClass setIsSet (λ v → (isL v) .snd)
符号化されたグラフは、底の集合の上で読まれる。底の要素の順序対が F の底の集合に属するとき、F は x と y について成立すると書く。以下のすべての節が、この形を読む。
Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩
構成可能集合 D と、順序対を符号化する構成可能集合 R を固定する。仮定 Rsub が述べるのは、R に実際に現れる各順序対の二つの端点が D に属することだけである。崩壊を作る段階で整礎性と推移性を加え、さらに後で単射性を証明するときに三分法を加える。この章では関係の外延性を仮定しない。
module Collapse (D R : S)
(Rsub : (y x : S) → Holds R y x
→ ⟨ y .fst ∈ D .fst ⟩ × ⟨ x .fst ∈ D .fst ⟩) where
D への所属は、台の上の一項の述語として述べられる。
Mem : S → Type (ℓ-suc ℓ)
Mem x = ⟨ x .fst ∈ D .fst ⟩
この述語は命題である。提示された集合の底の集合への所属だからである。この命題性は後で重要になる。ある構成が所属の証明に依存しても、それで選択のデータを運ぶことはないのである。
isPropMem : (x : S) → isProp (Mem x)
isPropMem x = (x .fst ∈ D .fst) .snd
D の要素は、小さな型、すなわち提示の添字型によって提示される。
Dom : Type ℓ
Dom = ⟪ D .fst ⟫
提示は、その索引を周囲の階層の中へ埋め込む。
↪ : Dom → V ℓ
↪ = ⟪ D .fst ⟫↪
索引は構成可能な集合へ戻される。埋め込まれた要素には、D への所属に沿って、構成可能性の推移性によって運ばれた構成可能性の証明が対にされる。
up : Dom → S
up m = ↪ m , isL-trans {x = D .fst} {y = ↪ m} (member (D .fst) m) (D .snd)
作り直された構成可能な集合は D の要素である。これは、提示自身の所属の記録によるものである。
up-mem : (m : Dom) → Mem (up m)
up-mem m = member (D .fst) m
この表示には重複する添字がない。埋め込まれた二つの要素が等しければ、その添字も等しくなる。後で既知の要素 up b から添字を復元するとき、復元された添字を b 自身と同一視できるため、集めたグラフが期待する対 (↪ b, col b) を含むことが分かる。崩壊関数の単射性は別の結果であり、三分法を必要とする。
Dom≡ : {a b : Dom} → ↪ a ≡ ↪ b → a ≡ b
Dom≡ {a} {b} e = ↪-inj {a = D .fst} {m = a} {n = b} e
逆に、D の要素とその所属の証明からは、提示のその要素における繊維を取ることで、提示の索引が復元される。
toDom : (x : S) → Mem x → Dom
toDom x mx = (fiber (D .fst) mx) .fst
復元された索引は、与えられた要素をちょうど提示する。繊維が、埋め込まれた索引とその要素の同一視を運ぶからである。
toDom-val : (x : S) (mx : Mem x) → ↪ (toDom x mx) ≡ x .fst
toDom-val x mx = (fiber (D .fst) mx) .snd
符号 R は小さな表示の上に関係を誘導する。a ≺ b とは、表示された要素 ↪ a と ↪ b の順序対が R に属することである。整礎再帰はこの関係に沿って進む。続く二つの補題が、この関係を構成可能集合上の Holds R (up a) (up b) と両方向に結び付ける。
opaque
_≺_ : Dom → Dom → Type ℓ
a ≺ b = ⟨ pr (↪ a) (↪ b) ∈ₛ R .fst ⟩
添字 a と b を固定すると、関係の型 a ≺ b は階層内の集合への所属を述べる命題である。したがって、この関係が記録するのは辺の有無だけであり、特定の証明が担う追加のデータではない。この命題性だけでは辺の有無を判定できず、その判定が実際に必要となる後の箇所で初めて排中律を使う。
isProp≺ : (a b : Dom) → isProp (a ≺ b)
isProp≺ a b = (pr (↪ a) (↪ b) ∈ₛ R .fst) .snd
符号化された関係の中の所属は、小さな関係を与える。L の中に記録された順序対が、二つの所属の関係をつなぐ橋によって認められるのである。
≺-in : (a b : Dom) → Holds R (up a) (up b) → a ≺ b
≺-in a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = R .fst} .fst
逆に、小さな関係は R の本当の対を記録するので、関係の二つの読みは両方向で一致する。
≺-out : (a b : Dom) → a ≺ b → Holds R (up a) (up b)
≺-out a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = R .fst} .snd
関係 _≺_ の整礎性は、col を定義する再帰と帰納を与える。推移性の役割は別である。先行者の列が上端の点より下にとどまることを保証し、各崩壊値が推移的で順序数になることを証明するために使われる。この二つの仮定だけでは、崩壊の単射性も、関係が整列順序であることも得られない。
module Col (wf : WellFounded _≺_)
(≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where
Mostowski の構成は、col p を先行者 r ≺ p の値 col r からなる集合として定める。計算規則 col-eq は、再帰的な値をこの明示的な先行者像と同一視する。所属の補題は、指定された先行者から col r ∈ col p を与えるが、逆に任意の要素から得る先行者は命題的に切り詰められた存在にとどまる。col-ord は個々の col p が順序数であることを証明する。
open Mostowski Dom _≺_ wf ≺-trans public
using ( module W; col; col-eq; col-in; col-out; col-ord )
すべての崩壊値は構成可能である。まず補題 col-ord が col p は順序数であることを示し、次に段階の補題がこの順序数をその後続で添字づけられた段階に置くことで、col-isL p が得られる。
opaque
col-isL : (p : Dom) → ⟨ isL (col p) ⟩
col-isL p = Lset→isL (sucV (col p)) (suc-ord (col-ord p)) (col p)
(ord∈Lset-suc (col p) (col-ord p))
それぞれの崩壊の値は、その構成可能性の証明とともに、構成可能な集合として包まれる。崩壊が産み出すのは、周囲の集合だけではなく、構成可能宇宙の実際の要素である。
colʟ : Dom → S
colʟ p = col p , col-isL p
崩壊表を記述する論理式
x の各 R-先行者 y に対して表 F が何らかの値 u を記録するとき、F は x で完全である。u の存在は命題的に切り詰められている。完全性が保つのは項目が存在するという事実だけで、特定の項目を選ばず、値の一意性もまだ主張しない。
Complete : S → S → S → Type (ℓ-suc ℓ)
Complete F R x = (y : S) → Holds R y x → ∥ Σ[ u ∶ S ] Holds F y u ∥₁
述語 Src F R x w は、x のある R-先行者において F が w を値として記録することを表す。その先行者と表項目はともに命題的切り詰めの中にとどまる。後の議論が使うのは、そこから得られる所属の事実だけだからである。
Src : S → S → S → S → Type (ℓ-suc ℓ)
Src F R x w = ∥ Σ[ y ∶ S ] (Holds R y x × Holds F y w) ∥₁
値 v が x に対して正しいのは、その要素がちょうど源となる値であるときである。v の中の所属から源が得られ、すべての源が要素である。二つの方向合わせて、v が記録された先行者の値の集合であることを、所属だけを通して言っている。
ValueIs : S → S → S → S → Type (ℓ-suc ℓ)
ValueIs F R x v = (w : S) → (⟨ w .fst ∈ v .fst ⟩ → Src F R x w)
× (Src F R x w → ⟨ w .fst ∈ v .fst ⟩)
表が実際に含む各順序対について、その入力で完全性が成り立ち、出力が先行者の値だけからなるとき、その表を正しいという。この条件は領域を指定しないので、D 全体の項目を要求せず、D の外の項目も禁止しない。後の一意性定理が記録された値を崩壊値と同一視するのは、記録された入力が D の要素である場合だけである。
Correct : S → S → Type (ℓ-suc ℓ)
Correct F R = (x v : S) → Holds F x v → Complete F R x × ValueIs F R x v
論理式 completeAt f R x は、候補となる先行者 y を非有界全称量化子で導入する。含意によって、R が対 (y,x) を記録する y だけに条件を課し、その結論では非有界存在量化子で値 u を導入して、F が (y,u) を記録することを要求する。存在量化子の内側では u が新しい第零スロットを占め、それまでの変数は一つずつずれる。
opaque
completeAt : ∀ {n} → Fin n → S → Fin n → Formula S n
completeAt f R x =
∀̇ ( appC R zero (suc x)
⇒̇ ∃̇ (appAt (suc (suc f)) (suc zero) zero) )
この論理式をホスト側の完全性として読むには、先行者 y と、R が (y,x) を記録する証明を固定する。appC の妥当性を表すパスがこの前提を、充足の証明 h が要求する含意の前件へ変える。h を適用すると命題的に切り詰められた候補値が得られる。map₁ は切り詰めを保ったまま、appAt の妥当性を表すパスによって、そのグラフ原子を Holds F y u へ変える。
complete-out : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : Vec S n)
→ ⟨ γ ⊨ completeAt f R x ⟩
→ Complete (lookup f γ) R (lookup x γ)
complete-out f R x γ h y p = map₁
(λ { (u , q) → u , subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ)) q })
この向きの最後の適用は、上で述べた最初の変換を行う。与えられた関係の事実を appC-adequate に沿って運び、その結果を h y に渡す。得られるものは、対象言語の意味論が作る切り詰められた存在のままである。前の行の写像は、その切り詰めの中身だけを変える。
(h y (subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p))
逆に、ホスト側の完全性を仮定する。論理式の前件を満たす候補の先行者について、まず appC-adequate がその前件を Holds R y x に変える。完全性は命題的に切り詰められた値 u を与え、map₁ がそれに伴う Holds F y u を、存在結論が要求する適用原子の充足へ戻す。
complete-in : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : Vec S n)
→ Complete (lookup f γ) R (lookup x γ)
→ ⟨ γ ⊨ completeAt f R x ⟩
complete-in f R x γ h y p = map₁
(λ { (u , q) → u , subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ))) q })
この行は、充足された関係原子を Holds R y x へ変換し、x における完全性を候補の先行者 y に適用する。この適用が切り詰められた値を与え、外側の写像がそれを対象言語の存在量化子が求める証人へ変換する。
(h y (subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p))
論理式 srcAt f R x w は非有界存在量化子を使い、ある y が x の R-先行者であると同時に、F が入力 y で w を記録することを述べる。先行者への制限は最初の連言肢で表し、有界存在量化子は使わない。
opaque
srcAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
srcAt f R x w = ∃̇ ( appC R zero (suc x) ∧̇ appAt (suc f) zero (suc w) )
意味論上の存在はすでに命題的に切り詰められている。src-out を定める写像はその切り詰めを保ち、内部の仮の証人 y を変換する。appC-adequate が最初の連言肢を Holds R y x として読み、appAt-adequate が第二の連言肢を Holds F y w として読む。
src-out : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : Vec S n)
→ ⟨ γ ⊨ srcAt f R x w ⟩
→ Src (lookup f γ) R (lookup x γ) (lookup w γ)
src-out f R x w γ = map₁ (λ { (y , (p , q)) → y
, ( subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p
先行者のグラフへの所属が、読みを閉じる。
, subst ⟨_⟩ (appAt-adequate (suc f) zero (suc w) (y ∷ γ)) q ) })
源の埋めはその逆である。先行者を存在量化子の中に導入し、二つのアトムをそれぞれの妥当性の補題に逆らって運ぶ。
src-in : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : Vec S n)
→ Src (lookup f γ) R (lookup x γ) (lookup w γ)
→ ⟨ γ ⊨ srcAt f R x w ⟩
src-in f R x w γ = map₁ (λ { (y , (p , q)) → y
, ( subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p
グラフのアトムが最後に書き込まれ、埋めが完成する。
, subst ⟨_⟩ (sym (appAt-adequate (suc f) zero (suc w) (y ∷ γ))) q ) })
論理式 valueAt f R x v は任意の集合 w を量化し、w ∈ v と srcAt f R x w の間の二つの含意をともに述べる。したがって、v を外延的に特徴づけている。つまり v の要素は、x の先行者で記録された値にちょうど一致する。定義では srcAt を展開し、この特徴づけを一つの一階論理式として表す。
opaque
unfolding srcAt
valueAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
valueAt f R x v =
∀̇ ( ((var zero ∈̇ var (suc v)) ⇒̇ srcAt (suc f) R (suc x) zero)
同値はその二つの方向の連言であり、源の論理式はどちらの方向でも展開されている。
∧̇ (srcAt (suc f) R (suc x) zero ⇒̇ (var zero ∈̇ var (suc v))) )
valueAt を外向きに読むとき、その全称量化子を各 w で具体化する。前向きの含意はまず v への所属を出所の論理式の充足へ変え、次に src-out がその充足を Src F R x w として読む。これにより ValueIs の前向きの半分が得られる。
value-out : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : Vec S n)
→ ⟨ γ ⊨ valueAt f R x v ⟩
→ ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
value-out f R x v γ h w =
(λ w∈ → src-out (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))
逆方向は、源の埋めを通して対称的に読まれる。こうして、この論理式は、v が源となる値を集めていることをちょうど述べており、これが後の一意性の議論が消費する読みである。
, (λ s → h w .snd (src-in (suc f) R (suc x) zero (w ∷ γ) s))
valueAt の前向きの含意を示すため、候補となる値 v の要素 w を取る。ホストレベルの値の方程式は、w が x のある R-先行者で記録された値として単に現れることを述べる。この出所の主張を内向きに読むと、w で拡張した環境において、対象言語の論理式が求める存在証人が得られる。
value-in : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : Vec S n)
→ ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
→ ⟨ γ ⊨ valueAt f R x v ⟩
value-in f R x v γ h w =
(λ w∈ → src-in (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))
逆向きの含意では、まず出所の論理式の充足を、表の値が w となる先行者が単に存在することとして読む。次に ValueIs の逆向きの半分から、w が記録された値に属することが従う。したがって valueAt が表すのは候補となる表についての再帰方程式そのものであり、その値を Mostowski 崩壊と同定するには、後で整礎帰納が必要である。
, (λ s → h w .snd (src-out (suc f) R (suc x) zero (w ∷ γ) s))
正しさが検査されるのは、候補となる表が実際に項目をもつ点だけである。二つの全称量化子は入力 x と値 v を動き、表が順序対 (x,v) を含むなら、その項目が再帰の一段として正しいための二条件を要求する。
opaque
unfolding completeAt valueAt
correctAt : ∀ {n} → Fin n → S → Formula S n
correctAt f R =
∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero
二つの条件は、存在と値の方程式を分けて述べる。完全性は x の各 R-先行者に表の項目があることを述べ、値の条項は v の要素がそれらの先行者で記録された値とちょうど一致することを述べる。この論理式は、表にすでに現れる項目以外について定義域を指定しない。
⇒̇ ( completeAt (suc (suc f)) R (suc zero)
∧̇ valueAt (suc (suc f)) R (suc zero) zero ) ))
論理式を外向きに読むには、まず表の実際の項目 (x,v) を取る。appAt の妥当性によって、その所属証明は論理式の前件へ移される。二つの量化子を x と v で具体化すると、x での完全性と対応する値の方程式が得られ、この行では完全性の側をホストレベルの述語へ読み戻す。
correct-out : ∀ {n} (f : Fin n) (R : S) (γ : Vec S n)
→ ⟨ γ ⊨ correctAt f R ⟩ → Correct (lookup f γ) R
correct-out f R γ h x v p =
let (c , w) = h x v (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ))) p)
in complete-out (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c
第二成分を value-out で読むと、v への所属と、x のある R-先行者で値として現れることとの同値が得られる。これを完全性と組にすれば、選んだ項目がホストレベルで正しいことが示される。同じ構成は表の各項目に適用できるので、Correct F R が従う。
, value-out (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w
逆に、表がホストレベルで正しいとする。入力 x、値 v、項目 (x,v) を選ぶと、appAt の妥当性によって対象言語の含意の前件が対応するホストレベルの項目へ移る。正しさから、その項目の完全性と値の方程式が得られ、この行では完全性の側を論理式へ入れる。
correct-in : ∀ {n} (f : Fin n) (R : S) (γ : Vec S n)
→ Correct (lookup f γ) R → ⟨ γ ⊨ correctAt f R ⟩
correct-in f R γ h x v p =
let (c , w) = h x v (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ)) p)
in complete-in (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c
値の方程式を value-in で入れると、項目 (x,v) に必要な連言が完成する。選んだ二要素について抽象すれば、二つの全称量化子が得られる。したがって correct-in と correct-out は、correctAt とホストレベルの述語 Correct の正確な対応を与える。
, value-in (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w
次の論理式では関係 R を固定するが、証人となる表は存在量化されたままである。この区別により、定義域全体を覆う一つの表を構成する前でも、ある正しい表を使って値を局所的に認識できる。
module ColFo (R : S) where
環境 (z ∷ p ∷ []) で、この論理式は、R に対して正しく項目 (p,z) を含む集合 F が単に存在することを述べる。表は存在量化されているので、これは p での値を局所的に特徴づけるだけであり、一つの固定された表が定義域全体で同時に働くとはまだ述べていない。
opaque
unfolding correctAt
colFo : Formula S 2
colFo = ∃̇ ( correctAt zero R
∧̇ appAt zero (suc (suc zero)) (suc zero) )
colFo を外向きに読むとき、表の証人を包む命題的切り詰めは保たれる。存在量化子が表 F を与え、同じ切り詰めの内側で、連言が F は R に対して正しいという証拠と、項目 (p,z) を表す対象言語の適用原子式を与える。
colFo-out : (z p : S) → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
→ ∥ Σ[ F ∶ S ] (Correct F R × Holds F p z) ∥₁
colFo-out z p = map₁ (λ { (F , (hc , ha)) → F
, ( correct-out zero R (F ∷ z ∷ p ∷ []) hc
, subst ⟨_⟩ (appAt-adequate zero (suc (suc zero)) (suc zero)
appAt の妥当性は、残った適用原子式を Holds F p z へ変換する。したがって得られるのは、正しい表と必要な項目が単に存在するという、論理式のホストレベルでの読みそのものである。
(F ∷ z ∷ p ∷ [])) ha ) })
内向きには、明示的に与えられた、(p,z) を含む正しい表 F を存在証人とする。正しさの証明は correct-in によって論理式へ移され、残る仕事は与えられた表の項目を適用原子式で表すことである。
colFo-in : (z p F : S) → Correct F R → Holds F p z
→ ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
colFo-in z p F hc hp = ∣ F
, ( correct-in zero R (F ∷ z ∷ p ∷ []) hc
, subst ⟨_⟩ (sym (appAt-adequate zero (suc (suc zero)) (suc zero)
appAt の妥当性を逆向きに用いると、Holds F p z はその原子式の充足へ移る。表の証人、その正しさ、この項目を存在量化の切り詰めに包むことで、(z,p) における colFo の充足が得られる。
(F ∷ z ∷ p ∷ []))) hp ) ∣₁
後では、colFo のような各点での値の論理式から、順序対の集合を定める必要がある。一般的な構成 PairFo は、z が p で与えられた論理式を満たすとき、かつそのときに限って順序対 (p,z) を認識する。これにより、局所的な崩壊の論理式を、以下で構成する再帰の値関係として使える。
一意性、存在、崩壊表
内部の構成は、符号化された定義域 D と関係 R から始まる。最初の付帯条件は、R に属する各順序対の両成分が D に属することだけである。整礎性と推移性はこのモジュールの境界では仮定されず、崩壊の議論を始めるときに別々に与えられる。
module Internal (D R : S)
(Rsub : (y x : S) → Holds R y x
→ ⟨ y .fst ∈ D .fst ⟩ × ⟨ x .fst ∈ D .fst ⟩) where
定義域の表示と符号化された関係を共通の土台として、二つの論理式を用意する。CF は R に対する局所的な崩壊値の論理式であり、PF は入力と、その論理式を満たす値との順序対を認識する。この時点では、どちらも崩壊値の存在や一意性を主張しない。
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 における等しさが従う。
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 を結びつけるのは、この置換である。
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 の端点条件からはどちらも従わない。
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 についてではない。
open Col wf ≺-trans public
整礎性はループ a ≺ a を排除する。帰納段階でそのようなループがあると、先行者についての帰納仮定を a 自身に適用できる。同じループが、a が自分自身より小さいことの証拠と、帰納仮定から矛盾を得るための入力の両方になる。
≺-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 に関する整礎帰納で進み、表示された等式を帰納的述語とする。
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 での完備さと、値の条項という二つの補助の事実が取り出される。
→ (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 への所属と先行者の値として現れることを同定する。続く外延性の議論の二方向では、この二つを逆の順で用いる。
val : ValueIs F R (up a) v
val = hc (up a) v hv .snd
第一の包含を示すため、記録された値 v の要素 w を取る。v は構成可能であり、その要素 w も構成可能なので、台の要素 wS として組にできる。すると val の前向きの半分から、a のある R-先行者 y で表が wS を記録することが、命題的切り詰めのもとで得られる。
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)
出所の項目は、必要な二つの事実に変換される。載せられた先行者と入力の間の関係と、載せられた先行者での表の項目である。先行者は、その内部の添字に復号される。
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 の崩壊の同定を記録する。これは次に証明される。
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 に等しくなる。
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 とできる。
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 と比較することである。
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 にする。
∣ 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) と同定される。
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) })
崩壊の論理式の外向きの読み出しが、正しい表と表の項目を供給する。それらは、一意性の補題の二つの入力である。
(CF.colFo-out v q h)
局所表のモジュールは、定義域の入力 a と、より小さい入力ごとに崩壊の論理式を供給する帰納の仮定によってパラメータづけられる。a のために、実際の先行者での項目が崩壊値を記録し、それ以外の項目が既定の対を記録する表を作る。
module Approx (a : Dom)
(IH : (b : Dom) → b ≺ a → ⟨ (colʟ b ∷ up b ∷ []) ⊨ CF.colFo ⟩) where
既定の項目 ea は、載せられた入力とその自身の崩壊の順序対で、台の要素として提示される。
ea : S
ea = prʟ (up a) (colʟ a)
局所の論理式の本体は、二つの選言肢をもつ。左は、q が a の実際の先行者であり、z が q と、崩壊の論理式を満たす値とを対にすること。右は、q が先行者ではなく、z が既定の項目であること。この場合分けは排中律で決定される。
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 からなる順序対を関係検査に使う必要がある。対の式は、局所的な論理式の二つの自由な枠において、この項を一様に与える。
module PE = PairExpression
式 image は順序対 (q,up a) を表す。第一成分は入力の枠から取り、第二成分は a を表す台の要素をリテラルとして置く。したがって image が R に属することは、ちょうど q が a の R-先行者であることを述べ、局所表の項目を記述するものではない。
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 に等しいことを要求する。どちらの分岐を選ぶかという古典的な判定は後の関数性証明で使われるのであり、選言そのものに含まれるわけではない。
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 の反証へ変換する必要がある。
ψ-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 を既定の項目と同定する等式はすでに必要なホストレベルの形なので、そのまま保たれる。
((λ k → lower (h1 (PE.member-in image (con R) (z ∷ q ∷ []) k))) , h2) })
内向きの読み出しは、左の分岐を、対の式の導入と対のグラフの導入を通して注入し、切り詰められた値を、命題値の充足の中へ消去する。
ψ-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)) =
右の分岐は、ホスト側の反駁を対象言語へ持ち上げ、既定の等式を運ぶ。どちらの分岐も、論理式の切り詰められた選言へ注入される。
∣ inr ((λ k → lift (h1 (PE.member-out image (con R) (z ∷ q ∷ []) k))) , e) ∣₁
補助の b≺a-of は、ホスト側の関係の所属を、内部の比較へ復号する。q が a と関係するなら、q の内部の添字は a より下である。復号は、所属を下降して添字を取り出すことによって行われる。
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 へ輸送する。
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 は、この切り詰められた一意存在を可縮性へ変換する。
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 を使う。局所的な判定の補題は、どちらの場合にも論理式を満たす出力が一つあり、それを満たすほかの出力はすべてその出力に等しいことを、命題的切り詰めのもとで示す。
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 と矛盾する。
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 を選ぶ、先行者でない場合が別に始まり、その一意性証明は次のコードブロックへ続く。
(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 へ持ち上がる。
, ( ψ-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 である。ψ とこの一意性証明に置換を適用すると、得られる値が一つの構成可能集合に集められる。
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) にちょうど限られることが分かる。
Fa : S
Fa = T.table
Below b は、添字 b が現在のもの以下であることを述べる。真に下か、等しいかのいずれかである。この二つの述語が、局所的な表の導入と正しさの両方を支える。
Below : Dom → Type ℓ
Below b = (b ≺ a) ⊎ (b ≡ a)
b が a 以下なら、Fa-in は入力 up b と値 colʟ b からなるグラフの項を Fa に入れる。狭義の比較の場合は帰納仮定によって ψ の第一の選言肢を満たし、等式 b ≡ a の場合はこの順序対を ea と同一視して既定の分岐を使う。
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 に沿う輸送が対象の順序対を既定の順序対と同一視する。
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) と同一視する等式が単に得られる。添字は命題的切り詰めの中にあるため、この結論は代表を選ばない。
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 自身を添字とする順序対である。
(λ { (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 は、どちらも命題的に切り詰められた証人だけを返す。目標も命題的に切り詰められているので、どちらの証人も大域的に選ぶことなく、外側、内側の順に切り詰めを除去できる。
(ψ-out y q hψ) })
(T.table-out y hy)
直前の結果を x と v の順序対符号に適用すると、その二つの座標を復元できる。したがってグラフの項 Holds Fa x v からは、x .fst ≡ ↪ b かつ v .fst ≡ col b を満たすある b ≤ a が単に得られる。
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
輸送は等式を内部の対に向け直し、補助が順序対の単射性を通してそれを、添字の名指しの等式と崩壊の値の名指しの等式に分ける。
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 は二つの成分の等式を反転してから返す。
q = pr-inj (sym (prʟ-fst x v) ∙ e)
c ≺ b かつ b ≺ a なら、推移性から c ≺ a が従う。一方 b ≡ a なら、この等式を c ≺ b に代入して同じ結論を得る。これが Below b の二つの場合である。
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 はともに命題なので、その連言へ切り詰めを除去できる。
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 と対になっていることとの同値を示す。
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 と比較できる添字を復元する。
where
y R x から端点の包含仮定によって y ∈ D が得られるので、toDom y my は添字 c を定める。y と x の表示等式に沿って関係の証拠を輸送すると c ≺ b が従い、第二成分には ↪ c が y の基礎集合であることが記録される。
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 への所属は命題なので、この根拠を使っても表示の選択が新たに加わることはない。
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 より真に下にある。
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 へ運ぶ輸送を与える。
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 に対応させる表の項が構成できる。
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
二つの所属は添字の等式と狭義の比較に沿って輸送され、関係と表の所属の両方が名指された先行者のところに置かれる。
, ( 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 は命題なので、出所の証人と表の読み出しに含まれる命題的切り詰めを順にそこへ除去できる。
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 へ輸送する。
→ Σ[ 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 の間の狭義の比較は、二つの名指しの等式と関係の証人から満たされ、先行者のデータがそろう。
cb : c ≺ b
cb = ≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ R .fst ⟩) (sym ey) (sym ex) hy)
局所的な表は頂点の要素でグラフの論理式を満たし、既定の項目が値の節の証人になる。これがこの節の帰納の段階である。
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 自体がすでに順序数と同一視されていることは必要ない。
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 のもとの要素へ輸送する。
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 で論理式を満たすことが示される。
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 の等式へ、最後にファイバーの要素全体の等式へ持ち上がる。
; 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 のある入力から生じる。
module OT = Of otR using ( table; table-in; table-out )
otL は otR の置換による値域であり、したがって L の要素である。その基礎集合はすべての b : Dom に対する崩壊値 col b を集めるが、それらの値が互いに異なる添字から来る必要はない。ここではこの正確な値域の記述だけを用い、値域全体の順序数性はさらに導くべき結論として残す。
otL : S
otL = OT.table
各 b : Dom について、近似補題は colʟ b が up b における otR の値であることを示す。したがって置換の導入方向から col b ∈ otL .fst が得られる。
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 が単に存在する。結論には意図的に命題的切り詰めが残されているため、各要素の原像を選ぶことなく正確な値域を記述している。
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 の構成可能性から、構成可能性の下方閉性がこの組を与える。
yS = y , isL-trans {x = otL .fst} {y = y} hy (otL .snd)
再帰グラフの構成を otR に適用すると、裸の値ではなく順序対が集められる。D の各入力について、その入力と一意に定まる崩壊値を記録し、対応する内向きと外向きの読み、一価性、そして定義域が正確に D であることを与える。
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 自体は外部の小さな表示に属する添字のままである。
colTable : S
colTable = CT.F
標準的な代表 up b において、再帰グラフが最初に記録する値は col (toDom (up b) (up-mem b)) である。表示等式から、この復元された添字と b との等式が得られる。その col による像に沿って第二座標を輸送すると、主張された順序対 pr(↪ b,col b) が得られる。
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) が単に成り立つと述べる。その添字は命題的切り詰めの中にあるため、この外向きの読みはグラフを特徴づけるが、各要素を表示する添字を選ばない。
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 の提示する添字の崩壊の値であることを述べ、提示の所属をデータとして伴う。
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 が集合であるため命題である。したがって、この依存和は追加の選択データをもたない。
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 が命題であるため、グラフの読み出しに含まれる切り詰めを除去できる。
colTable-pair : (x v : S) → Holds colTable x v → Fib x v
colTable-pair = CT.pair-out
符号化された単射としてのグラフ
崩壊グラフがいつ単射を符号化するかを調べるため、D、R、および端点条件 Rsub を固定する。この条件が述べるのは、R に記録された各辺の両端点が D に属することだけである。整礎性、推移性、三分法は別々の仮定として残る。
module Code (D R : S)
(Rsub : (y x : S) → Holds R y x
→ ⟨ y .fst ∈ D .fst ⟩ × ⟨ x .fst ∈ D .fst ⟩) where
ここでも、先に用いた小さい表示 Dom、その符号化された関係 _≺_、および D の要素と添字との間の変換を使う。以下の符号化の議論は同じ崩壊構成に基づき、別の関係を導入しない。
open Internal D R Rsub public
仮定の役割はそれぞれ異なる。整礎性は再帰によって col を定義し、推移性は各崩壊値が順序数であり、したがって構成可能であることを示す。局所表の組み立てでは、この章の古典的な引数 lem も使う。これらを合わせて正確な値域 otL とグラフ colTable を構成し、一価性、正確な定義域、すべてのグラフ値が otL に属することを得る。三分法は次のモジュールで初めて加えられ、単射性の証明に使われる。
module Conjuncts (wf : WellFounded _≺_)
(≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where
この二つの仮定を固定すると、先のグラフ構成から col、otL、colTable と、それぞれの所属の特徴づけが得られる。この段階では、同じ入力には同じ値が記録されるが、記録された値の等しさから入力の等しさを復元できることはまだ示されていない。
open Graph wf ≺-trans public
二つのスロットをもつ環境 γ では、スロット 0 に colTable、スロット 1 に D が置かれる。したがって、一価性と正確な定義域の論理式は、これらの固定位置によってグラフとその意図された定義域を参照できる。
γ : Vec S 2
γ = colTable ∷ D ∷ []
第一の条件は一価性である。colTable が同じ入力に対して値 y と y' をもつ二つの順序対を含むなら、y .fst ≡ y' .fst が成り立つ。これは再帰値の一意性から従うものであり、各入力が値をもつこと自体は主張しない。
sv : ⟨ γ ⊨ svAt zero ⟩
sv = CT.sv
定義域条件は同値である。ある入力が colTable で何らかの値をもつことと、その入力が D に属することとは同値である。したがって、この条件は D の外の項を排除すると同時に、D の各要素上での全域性も述べる。後者の方向での値の存在は命題的に切り詰められたままである。
dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
dm = CT.dm
値域条件はグラフの対の読み出しから従う。x から y への項は、x が定義域に属する証拠を与え、y .fst を対応する崩壊値と同一視する。その崩壊値は otL-in によって otL に属する。ここで示したのはグラフの値が otL に入ることだけであり、colTable の単射性には次に導入する三分法の仮定がなお必要である。
ran : (x y : S) → Holds colTable x y → ⟨ y .fst ∈ otL .fst ⟩
ran x y h = subst (λ t → ⟨ t ∈ otL .fst ⟩) (sym ((colTable-pair x y h) .snd))
(otL-in (toDom x ((colTable-pair x y h) .fst)))
崩壊表はすでに D 上で全域的かつ一価であり、その値は正確な値域 otL に属している。符号化された単射を得るために残る条件は、入力の一意性である。そこで小さな定義域上の三分法を仮定する。任意の a と b に対して、a ≺ b、a ≡ b、b ≺ a のいずれかが成り立つという仮定である。外側のモジュールですでに固定された整礎性と推移性にこの比較を合わせると、崩壊値の等しさから添字の等しさを導ける。
module Inj (tri : (a b : Dom) → (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a))) where
col の単射性を示すため、col a ≡ col b を満たす a と b を固定し、両者の三分法で場合分けする。等しい場合は、それ自体が求める結論である。二つの狭義の場合には、崩壊値の間に実際に成り立つ所属を、その等しさに沿って自己所属へ移せるので、この不可能な所属を反駁すれば十分である。
col-inj : (a b : Dom) → col a ≡ col b → a ≡ b
col-inj a b e = go (tri a b)
where
go : (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a)) → a ≡ b
go (inl k) = ⊥₀-rec (∈-irrefl (col b)
左の場合、a は b に先行するので col a は col b の要素である。値の等式に沿って輸送すると col b が自分自身の要素になり、非反射性で反駁される。中間の場合は等式をそのまま返す。右の場合は対称的に、col a が自分自身の要素になる。
(subst (λ t → ⟨ t ∈ col b ⟩) e (col-in b a k)))
go (inr (inl q)) = q
go (inr (inr k)) = ⊥₀-rec (∈-irrefl (col a)
(subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b k)))
対象言語の条項 injAt は、同じ出力をもつ二つのグラフ項目が同じ入力をもつことを要求する。p と q を colTable-pair で読むと、二つの入力が D に属することを示す m と m'、および共通の出力 y を、復元された二つの崩壊値のそれぞれと同一視する等式が得られる。その二つの等式を合成すれば、col-inj に必要な仮定になる。
ij : ⟨ γ ⊨ injAt zero ⟩
ij = injAt-in zero γ (λ y x x' p q →
let (m , e) = colTable-pair x y p
(m' , e') = colTable-pair x' y q
in sym (toDom-val x m)
復元された添字は col-inj によって等しく、往復の補題がその等しさを、もとの台の要素の基礎の集合へ運び戻す。三つの等式が合成されて、必要な等しさになる。
∙ cong ↪ (col-inj (toDom x m) (toDom x' m') (sym e ∙ e'))
∙ toDom-val x' m')
四つのフィールドは、それぞれ異なる議論から得られる。再帰グラフが一価性と正確な定義域の条項を与え、colTable-pair と otL-in が値域の上界を与え、三分法が残っていた単射性の条項を与える。これらの証明をまとめると InjCode colTable D otL が得られる。したがって colTable が符号化された単射になるのは tri をもつモジュールの内部だけである。また、このレコードは otL の順序数性が本章で定理としてまとめられたとは主張しない。
code : InjCode colTable D otL
code = sv , dm , ij , ran
逆向きの構成は、選んだ始域 X と終域 Y に限って行う。各 x ∈ X に対し、pre は col b ≡ x .fst を満たす添字 b : Dom を選ばなければならない。これは崩壊の原像であり、関係のある固定した点の先行者であるとは限らない。第二の引数 bound は、表示された元の入力 ↪ b が Y に属することを証明する。逆向きのインターフェースを使うたびにこれらのデータを別途与える必要があり、otL-out だけから自動的に得られるものではない。
module Inverse (X Y : S)
(pre : (x : S) → ⟨ x .fst ∈ X .fst ⟩ → Σ[ b ∶ Dom ] (col b ≡ x .fst))
(bound : (x : S) (mx : ⟨ x .fst ∈ X .fst ⟩) → ⟨ ↪ (pre x mx .fst) ∈ Y .fst ⟩) where
源の集合への所属は型として記録され、議論が、写す各要素とともにそれを運べるようにする。
SourceMem : S → Type (ℓ-suc ℓ)
SourceMem x = ⟨ x .fst ∈ X .fst ⟩
x ∈ X に対し、b を pre が選んだ崩壊の原像とする。逆関数は up b、すなわち元の定義域で表示された要素 ↪ b を基礎集合にもつ構成可能な台の要素を返す。選ばれる原像は x が指定された始域に属する証拠に依存しうるため、証明引数 mx が必要である。
fn : (x : S) → SourceMem x → S
fn x mx = up (pre x mx .fst)
定義する論理式は、既存の表を逆向きに読む。環境 y ∷ x ∷ [] では、y が逆写像の候補となる出力、x がその入力であり、appC colTable zero (suc zero) は元の表項目 Holds colTable y x を主張する。新しい崩壊表を仮定するのではなく、古いグラフの二つの座標に逆向きの役割を与えている。
opaque
graph : Formula S 2
graph = appC colTable zero (suc zero)
妥当性の等式が、入れ替えたグラフの論理式の充足を、崩壊の表での対の所属と同一視する。だから表の二つの読み出しは相互に代用できる。
at : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ ≡ Holds colTable y x
at y x = cong ⟨_⟩ (appC-adequate colTable zero (suc zero) (y ∷ x ∷ []))
次に、逆向きの論理式が選ばれた値だけをもつことを示す。Holds colTable y x から、colTable-pair は候補出力 y を表示する添字と、その添字の崩壊値が逆写像の入力 x に等しいという等式を復元する。pre が選んだ添字も x へ崩壊する。したがって col-inj が二つの添字を同一視し、up-toDom がその添字の等しさを y ≡ fn x mx へ戻す。
only : (x : S) (mx : SourceMem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x mx
only x mx y hy = sym (up-toDom y my)
∙ cong up (col-inj (toDom y my) (pre x mx .fst) (sym (f .snd) ∙ sym (pre x mx .snd)))
where
f = colTable-pair y x (transport (at y x) hy)
f の第一射影は所属の証明 my : Mem y である。この証拠によって、復元される添字 toDom y my を作り、往復の補題を適用できる。my 自体がその添字なのではない。
my = f .fst
これらの材料から、X から Y への DefinableMap を作る。その外部関数は fn であり、bound が終域のフィールドを与える。定義の条項では、選んだ原像 b に対する colTable-in b から始める。出力の座標を col b ≡ x .fst に沿って置き換え、最後に at を逆向きに使って、得られた表への所属を逆向きのグラフ論理式の充足へ変える。
M : DefinableMap
M = record
{ dom = X ; cod = Y ; fn = fn ; into = bound ; graph = graph
; defines = λ x mx → transport (sym (at (fn x mx) x))
(subst (λ w → ⟨ pr (↪ (pre x mx .fst)) w ∈ colTable .fst ⟩)
フィールド defines は正準な項目 colTable-in b から始め、その出力座標を原像の等式 col b ≡ x .fst に沿って輸送する。妥当性の等式 at がその表への所属を逆向きのグラフ論理式の充足へ変え、only が必要な値の一意性を与える。
(pre x mx .snd)
(colTable-in (pre x mx .fst)))
; only = only }
逆関数の単射性には直接の理由がある。fn x mx と fn x' mx' の基礎集合が等しいなら、それらは pre が選んだ添字 b と b' に対する ↪ b と ↪ b' である。表示の単射性 Dom≡ によって b ≡ b' が得られる。この等式に col を作用させ、pre が保持する二つの等式と合成すれば、x .fst ≡ x' .fst が従う。この証明が Dom≡ で使うのは小さな表示の単射性である。col-inj は先に逆向きの論理式の値の一意性を示すために使われたが、この等式の列には現れない。
inj : (x : S) (mx : SourceMem x) (x' : S) (mx' : SourceMem x')
→ (fn x mx) .fst ≡ (fn x' mx') .fst → x .fst ≡ x' .fst
inj x mx x' mx' e = sym (pre x mx .snd) ∙ cong col (Dom≡ e) ∙ pre x' mx' .snd
一般の定義可能単射の構成を M と inj に適用すると、この制限された逆向きの写像が InjL X Y、すなわち符号化された単射の存在を命題的に切り詰めた主張としてまとめられる。その範囲は与えたデータによって正確に限られている。X の各要素には選ばれた崩壊の原像があり、表示された元の入力は Y に属する。これは otL 全体に対する無条件の逆写像も、全単射のレコードも与えない。
injL : InjL X Y
injL = DefinableInj.injL M inj