Bedrock符号化された単射の合成と包含
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ本章は、L の内部で符号化された単射の構成を二つ発展させ、一つの排除を証明します。第一に、二つの符号化された単射の合成です。ある中間の y が (x, y) を最初のグラフに、(y, z) を第二のグラフに持つとき、合成のグラフは x を z に関係付けます。第二に、集合の包含は、小さい方の集合上の恒等写像によって符号化されます。そのグラフは、等号で定義される順序対の集合、すなわち y = x を満たす対 (x, y) の全体です。最後に、ω から有限順序数の平方への単射は存在しません。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.InjectionComposition {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
グラフの性質と適用は、モデル言語の論理式によって表されます。各変数の枠は要素の列に対して読まれ、充足が構造の意味論となります。二つの構造が現れます。周囲の階層が集合を供給し、構成可能構造がグラフの住み、読まれる台を供給します。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _≐_; _∧̇_; ∃̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
周囲の集合の順序対は、二つの成分が復元できる対の演算で符号化されます。等しい符号は等しい成分をもちます。小さな集合には提示が伴い、階層へ埋め込まれた索引型によって、提示された要素についての事実が索引についての事実へ移ります。構成可能性は、所属に沿って下方閉な述語です。構成可能な集合の要素は構成可能です。
open import V.Coding {ℓ} using ( pr; pr-inj ) open import V.Presentation {ℓ} using ( member; fiber; ↪-inj ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd )
四つの材料が本章を支えます。序数 ω と、その要素がちょうど数項であるという事実。数項と有限集合の間の有限の対応辞と、その抽象的な追跡論法。小さな定義域の原理、すなわち構成可能集合の小さな族を一つの段階で抑えるもの。そして L 内部の分出であり、任意の複雑さの論理式に使えるので、以下のどの関係も共有の上界から刻み出されます。
open import L.Ordinal {ℓ} using ( ω-ord; #∈ω ) import L.Ordinal.SquareLaw {ℓ} lem as SQ open SQ using ( module FiniteBase ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
L の内部では、言語の適用のアトムは定数のもとで読まれます。グラフに引数を適用したものは再び論理式であり、この読みは忠実です。単射の三つの論理条件は、これらのアトムのもとでそれぞれ導入と除去の形をもちます。符号化された単射は、定義域と終域の提示の間の本物の関数として読み戻すこともできます。
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro ) open import L.Coding.Model {ℓ} using ( appC; appC-adequate ) public open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-out; injAt-in; module Small )
単射の符号とは、グラフに四条件のすべてを合わせたものです。すなわち、定義域の上で読まれる論理式としての一価性・定義域の全域性・単射性と、メタ言語で述べられる値域の条項です。内部単射の関係 InjL は、そのようなグラフと四条件が、単に、存在すると主張します。定義可能な単射の構成は、定義の論理式とともに与えられた写像をそのような符号へ変えます。
open import L.Cardinal {ℓ} lem using ( InjCode; InjL ) open import L.DefinableInjection {ℓ} lem using ( DefinableMap ) renaming ( module Inj to DefinableInj )
内部の存在は命題的切り詰めによって主張されます。主張は証人を選ばずに成り立ち、切り詰められた主張は命題へしか消去できません。空の型と自然数が、後の有限の議論を両側から抑えます。
import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.Data.Nat using ( ℕ ) open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
一つの証明が対の両成分を同時に動かすことがあり、二項の輸送がこれに仕えます。二つの集合の提示型の間では、同値が関数と単射を運び、集合の間のパスがそのような同値を与えます。周囲の階層は、本章のすべての所属の主張が読まれる台です。
open import Cubical.Foundations.Prelude using ( subst2 ) import Cubical.Foundations.Equiv as Equiv open Equiv using ( equivFun; invEq; retEq; _≃_ ) open import Cubical.Foundations.Univalence using ( pathToEquiv ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
階層は後続も極限も同じように構成します。後続の演算は集合に一つの要素を加え、無限集合 ω は数項、有限順序数ごとに一つを集めます。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) module IS = InfinitySet {ℓ} open IS using ( sucV; #_; ω )
提示は索引型と階層への埋め込みを対にし、その繊維が要素と索引の間で事実を運びます。命題値の存在量化子が、合成が使う定義域の条件を述べます。
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ ) open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
構成可能な台は、本章のすべての集合の住む名前で開かれます。絶対性の展開からは二つの読みが来ます。構成可能構造での充足、これを局所の使用のために改名したもの、そしてその持ち上げられた形、すなわちアトムを定数の列のもとで評価する形です。以下のグラフの適用はすべて、この持ち上げられた読みを通します。
open hPropStructure 𝒮ʟ using ( S ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
有限の側は、数項の対応辞と抽象的な追跡を開きます。どちらも、本章が具体化するだけの形で述べられています。
open FiniteBase using ( ω-mem→numeral; toFin; toFin-inj; fromFin; fromFin-inj ) open FiniteBase using ( module AbstractChase )
共通の構成可能な上界
分出で関係を刻むには、候補となる要素が一つの構成可能集合の中になければなりません。共有の装置は任意の小さな添字族 g : I → S を受け取り、各 g i を含む構成可能集合を返します。後の PairBound で初めて、選んだ定義域と終域から生じる順序対に具体化します。
module StageBound (I : Type ℓ) (g : I → S) where opaque bnd : S bnd = smallDom I g .fst
読み手は上界の目的をそのまま述べます。族の各構成員は、周囲の要素として読めば上界に属します。後で Relation に入れられる各対は、この読み手を通して上界に入ります。
below : (i : I) → ⟨ fst (g i) ∈ fst bnd ⟩ below = smallDom I g .snd
有限な終域の排除
後に使う有限の排除は次の形を取ります。ω から有限順序数の平方への単射は存在しません。道は ω の内部の所属をほとんど避けます。使うのは、ω の各要素が単にある数項であること、各数項が有限集合を提示し対応辞が両方向で単射であること、そして抽象的な追跡です。各有限の提示から固定された型への単射と、その固定型からある有限の提示の平方への単射が与えられれば、大きい有限集合から小さい有限集合への単射が導かれます。
ω 自身についての事実であり、所属の述語が支える強さでのものです。ω の要素は、単に、ある数項であり、数項 n の後続は再び数項、したがって再び要素です。γ とその数項の同一視は後続に沿って輸送されます。
ω-limit : (γ : V ℓ) → ⟨ γ ∈ ω ⟩ → ⟨ sucV γ ∈ ω ⟩ ω-limit γ γ∈ω = PT.rec (snd (sucV γ ∈ ω)) go (ω-mem→numeral γ γ∈ω) where go : Σ[ n ∈ ℕ ] (γ ≡ # n) → ⟨ sucV γ ∈ ω ⟩ go (n , p) = subst (λ w → ⟨ sucV w ∈ ω ⟩) (sym p) (#∈ω (suc n))
数項は ω の提示へ埋め込まれます。道すじは直接です。数項 m の提示の索引は、その数項の要素を名指します。その数項は ω に属し、ω の推移性により、名指された要素も ω に属します。ω の提示のその要素での繊維を取れば、それを提示する ω の提示の索引が得られます。
numeral-into-ω : (m : ℕ) → ⟪ # m ⟫ → ⟪ ω ⟫ numeral-into-ω m i = fiber ω (ω-ord .fst (member (# m) i) (#∈ω m)) .fst
埋め込みは単射です。同じ数項の二つの索引が ω の提示の中で等しい値をもつなら、二つの繊維の同一視が、像の等しさをその数項の内部の提示された要素の等しさへ変えます。そして数項自身の提示は単射なので、二つの索引は一致します。
numeral-into-ω-inj : (m : ℕ) (i₁ i₂ : ⟪ # m ⟫) → numeral-into-ω m i₁ ≡ numeral-into-ω m i₂ → i₁ ≡ i₂ numeral-into-ω-inj m i₁ i₂ e = ↪-inj {a = # m} (sym (fiber ω (ω-ord .fst (member (# m) i₁) (#∈ω m)) .snd) ∙ cong (⟪ ω ⟫↪) e
ω の側で使われる単射の事実は、数項の提示の単射性だけです。
∙ fiber ω (ω-ord .fst (member (# m) i₂) (#∈ω m)) .snd)
追跡は、提示の索引型についてのメタ理論の主張であり、内部の単射の関係ではありません。仮定は二つです。第一に、各数項 n について、提示の型 ⟪ # n ⟫ と有限集合 Fin n の間に両方向の単射があり、それぞれの向きがそれ自身として単射であること。第二に、すべての ⟪ # m ⟫ から固定された型 ⟪ ω ⟫ への単射があること。結論は、⟪ ω ⟫ から ⟪ # n ⟫ × ⟪ # n ⟫ への単射は不可能だ、ということです。
no-inj-finite-ω : (n : ℕ) → (f : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫) → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥ no-inj-finite-ω n f finj =
抽象的な議論が消費するのは、対応辞と、固定型への単射の族です。その中心は鳩の巣の数え上げです。Fin (suc (n · n)) から Fin (n · n) への単射は存在せず、追跡は仮定された単射をまさにその形へ帰着させます。
AbstractChase.NoInj.no-inj (λ n → ⟪ # n ⟫) toFin toFin-inj fromFin fromFin-inj (⟪ ω ⟫)
本章が渡すべきは、数項の対応辞と ω の提示への埋め込みだけです。
(numeral-into-ω) (numeral-into-ω-inj) n f finj
この条項は排除を任意の有限順序数へ持ち上げます。しかも追跡の形のまま、提示の索引型の水準にとどまります。ここで固定された型は ⟪ ω ⟫、有限の提示は诸 ⟪ # n ⟫ です。
finite-excl-ω : (β : V ℓ) → IsOrd β → ⟨ β ∈ ω ⟩ → (f : ⟪ ω ⟫ → ⟪ β ⟫ × ⟪ β ⟫) → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥ finite-excl-ω β oβ β∈ω f finj = PT.rec Empty.isProp⊥ go (ω-mem→numeral β β∈ω)
β を ω の順序数の要素とし、ω の提示から β の提示の平方への関数が単射だとします。主張は矛盾であり、
where
β の ω への所属は、β と同一視される数項を単に与えます。したがって数項の場合を反証すれば十分で、切り詰めは空の型へ消去されます。空の型は命題です。
go : Σ[ n ∈ ℕ ] (β ≡ # n) → Empty.⊥ go (n , p) = no-inj-finite-ω n f' finj' where
この同一視は集合の間のパスであり、パスを平方すると二つの平方の提示の間の同値が得られます。仮定された関数はこの同値と合成され、その単射性は同値の単位則に沿って移ります。輸送された関数が二つの入力を同一視するなら、元の関数も同一視します。
e : ⟪ β ⟫ × ⟪ β ⟫ ≃ ⟪ # n ⟫ × ⟪ # n ⟫ e = pathToEquiv (cong (λ w → ⟪ w ⟫ × ⟪ w ⟫) p) f' : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫ f' x = equivFun e (f x) finj' : (x y : ⟪ ω ⟫) → f' x ≡ f' y → x ≡ y
こうして追跡は数項に適用され、その矛盾は述べた鳩の巣の形、すなわち Fin (suc (n · n)) から Fin (n · n) への単射です。
finj' x y e' = finj x y (sym (retEq e (f x)) ∙ cong (invEq e) e' ∙ retEq e (f y))
有界な順序対グラフとしての関係
L の二つの集合の間の関係は、符号化された順序対の集合になります。上界はどの論理式が現れるより先に、対を数え上げます。索引型は、定義域からの提示の索引と終域からの索引の積です。
module PairBound (D C : S) where Ix : Type ℓ Ix = ⟪ fst D ⟫ × ⟪ fst C ⟫
各提示の索引は台の要素として実現されます。それは提示された集合であり、構成可能な集合 D または C の要素なので、所属に沿って構成可能性が降ろされます。
private toD : ⟪ fst D ⟫ → S toD m = ⟪ fst D ⟫↪ m , isL-trans {x = fst D} {y = ⟪ fst D ⟫↪ m} (member (fst D) m) (snd D) toC : ⟪ fst C ⟫ → S
それぞれの側で、索引ごとに一つの L 要素です。
toC k = ⟪ fst C ⟫↪ k , isL-trans {x = fst C} {y = ⟪ fst C ⟫↪ k} (member (fst C) k) (snd C)
この族は、索引の各対を、実現された二要素の符号化された順序対へ送ります。共有の上界の装置がこの族に一度だけ施され、一つの構成可能集合が D と C から生じうるすべての符号化された対を含みます。
pw : Ix → S pw (m , k) = prʟ (toD m) (toC k) module SB = StageBound Ix pw
上界は装置から読み出され、以降は所属を通してのみ使われます。以下でその構成は必要とされません。
bnd : S bnd = SB.bnd
読み手は上界を提示の外へ広げます。D の任意の要素 x と C の任意の要素 z は、索引で与えられなくても、その符号化された対が上界の中にあります。以降のどの構成も、この形で上界に触れます。
below : (x z : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst z ∈ fst C ⟩ → ⟨ pr (fst x) (fst z) ∈ fst bnd ⟩ below x z mx mz = subst (λ w → ⟨ w ∈ fst bnd ⟩) pa (SB.below i) where
D と C は提示されているので、二つの要素はそれぞれ繊維をもちます。提示された集合がその要素と同一視される索引です。二つの繊維は独立に取られます。
fD : Σ[ m ∈ ⟪ fst D ⟫ ] (⟪ fst D ⟫↪ m ≡ fst x) fD = fiber (fst D) mx fC : Σ[ k ∈ ⟪ fst C ⟫ ] (⟪ fst C ⟫↪ k ≡ fst z) fC = fiber (fst C) mz
二つの索引は上界の族の一つの索引となり、その索引での族の値は提示された要素たちの符号化された対で、二つの繊維のパスに沿って x と z の符号化された対と等しくなります。その等しさに沿って所属を輸送すれば、読み手は完了します。
i : Ix i = fD .fst , fC .fst pa : fst (pw i) ≡ pr (fst x) (fst z) pa = prʟ-fst (toD (fD .fst)) (toC (fC .fst)) ∙ cong₂ pr (fD .snd) (fC .snd)
上界から関係を刻むのに三つのデータが要ります。三つの枠をもつ論理式と、対の上の述語 P、そして両方向の妥当性です。論理式の読みの順は値、添字、対です。環境 y ∷ x ∷ e のもとで、論理式は P x y として読まれます。
module Relation (D C : S) (φ : Formula S 3) (P : S → S → hProp (ℓ-suc ℓ)) (read : (x y e : S) → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩ → ⟨ P x y ⟩) (fill : (x y e : S) → ⟨ P x y ⟩ → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩) where
刻むための論理式は、二つの枠を存在量化し、さらに与えられた論理式に加えて、第三の枠が最初の二つの順序対を符号化することを対象言語の中で主張します。共有の上界での分出をこの一枠の論理式に施すと、関係が L の要素として返ります。
opaque fo : Formula S 1 fo = ∃̇ (∃̇ (prAtL (suc (suc zero)) (suc zero) zero ∧̇ φ)) rel : S rel = hasSeparationL (PairBound.bnd D C) fo .fst .fst
逆の読みは、所属を一つの対についての切り詰められたデータへ変えます。関係の要素 e は分出の仕様により刻むための論理式を満たします。二つの存在量化が解けて成分 x と y が現れ、e がその対を符号化することの証明が、妥当性によって符号化の演算自身の形に戻され、論理式の部分は P x y へ読み替えられます。
out : (e : S) → ⟨ fst e ∈ fst rel ⟩ → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] ((fst e ≡ pr (fst x) (fst y)) × ⟨ P x y ⟩) ∥₁ out e h = PT.rec squash₁ (λ { (x , hx) → PT.map (λ { (y , q , hy) → x , y , subst ⟨_⟩ (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ e ∷ [])) q
すべて切り詰められており、この関係が後に消費される形と一致します。
, read x y e hy }) hx }) (subst ⟨_⟩ (hasSeparationL (PairBound.bnd D C) fo .fst .snd e) h .snd)
順方向は述語から所属を作ります。
into : (x y : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst y ∈ fst C ⟩ → ⟨ P x y ⟩ → ⟨ pr (fst x) (fst y) ∈ fst rel ⟩ into x y mx my h = subst (λ w → ⟨ w ∈ fst rel ⟩) (prʟ-fst x y) (subst ⟨_⟩ (sym (hasSeparationL (PairBound.bnd D C) fo .fst .snd (prʟ x y))) ( subst (λ w → ⟨ w ∈ fst (PairBound.bnd D C) ⟩) (sym (prʟ-fst x y))
x と y の符号化された対は、上界の読み手によって共有の上界に入ります。論理式の符号化の条項は符号化の演算の計算で成り立ち、与えられた論理式は妥当性で成り立ちます。分出が所属を証明し、符号化の定義的な等しさに沿って輸送されます。
(PairBound.below D C x y mx my) , ∣ x , ∣ y , subst ⟨_⟩ (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ prʟ x y ∷ []))) (prʟ-fst x y) , fill x y (prʟ x y) h ∣₁ ∣₁ ))
x と y の本来の符号化された対に対しては、逆の読みは切り詰めのない結論へ鋭くなります。
pair-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst rel ⟩ → ⟨ P x y ⟩ pair-out x y h = PT.rec (snd (P x y)) (λ { (x' , y' , q , h') → subst2 (λ a b → ⟨ P a b ⟩) (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .fst)))
その証人は e をある x' と y' の符号化された対として提示します。符号化の単射性により、x' の底の要素は x のそれと、y' の底の要素は y のそれと同一視されます。さらに構成可能性は命題なので、これらの底の等しさは台の要素の等しさへ持ち上がります。述語は、ちょうど P x y の場所へ輸送されます。
(Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .snd))) h' }) (out (prʟ x y) (subst (λ w → ⟨ w ∈ fst rel ⟩) (sym (prʟ-fst x y)) h))
符号化された単射の合成
最初の終域が第二の定義域であるとき、二つの符号化された単射は合成できます。合成物もまたグラフであり、その検証は置換をやり直しません。二つの入力グラフはすでに集合として存在し、合成物は共有の上界の中で分出された一つの関係です。モジュールは二つのグラフと、それぞれ三つの読みの条件を受け取ります。
module Comp (D E C F H : S) (svF : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩) (dmF : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) (ijF : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩)
三つの読みの条件に加えて、各グラフは値域の条項をモジュールの独立な仮定として運びます。最初のグラフの各符号化された対の値は中間の集合にあり、第二のグラフの各対の値は最終の終域にあります。
(ranF : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst E ⟩) (svH : ⟨ (H ∷ E ∷ []) ⊨ svAt zero ⟩) (dmH : ⟨ (H ∷ E ∷ []) ⊨ domAt zero (suc zero) ⟩) (ijH : ⟨ (H ∷ E ∷ []) ⊨ injAt zero ⟩)
この二つの条項は、論理式としてではなくメタ言語で述べられます。
(ranH : (y z : S) → ⟨ pr (fst y) (fst z) ∈ fst H ⟩ → ⟨ fst z ∈ fst C ⟩) where
「符号と定義域」の各対は、三つの論理条件が要求する二枠の環境にすぎません。枠 0 にグラフ、枠 1 に定義域です。環境はグラフごとに一つです。
private γF : S ^ 2 γF = F ∷ D ∷ [] γH : S ^ 2 γH = H ∷ E ∷ []
結びの関係は次を言います。対象言語が中間の y で、(x, y) が最初のグラフに、(y, z) が第二のグラフにあるものを生み出せるなら、x と z は関係します。その切り詰めは存在量化子の意味論から受け継がれます。量化子は命題値であり、論理式の充足が運ぶ証人は、量化子に組み込まれた切り詰めの分だけです。
private Chain : S → S → Type (ℓ-suc ℓ) Chain x z = ∥ Σ[ y ∈ S ] (⟨ pr (fst x) (fst y) ∈ fst F ⟩ × ⟨ pr (fst y) (fst z) ∈ fst H ⟩) ∥₁
刻むための論理式には、中間の値の上の一つの存在量化だけがあります。その内側で二つの適用のアトムが連言されます。最初のグラフは、値の枠に中間値、添字の枠に x を置いて読まれ、第二のグラフは、値の枠に z、添字の枠に中間値を置いて読まれます。これが (x, y) ∈ F と (y, z) ∈ H の対象言語としての形です。
opaque body : Formula S 3 body = ∃̇ (appC F (suc (suc zero)) zero ∧̇ appC H zero (suc zero))
適用アトムの妥当性が、各連言を本来の所属へ運びます。第一は (x, y) における最初のグラフへの所属へ、第二は (y, z) における第二のグラフへの所属へ。残るのは、切り詰められた形の結びの証人です。
read : (x z p : S) → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩ → Chain x z read x z p = PT.map (λ { (y , hf , hh) → y , subst ⟨_⟩ (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ [])) hf , subst ⟨_⟩ (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ [])) hh })
逆方向は、結びの証人を同じ妥当性を逆にたどって対象言語へ戻します。二つの向きは、論理式と結びの関係が互いを表現することを言います。
fill : (x z p : S) → Chain x z → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩ fill x z p = PT.map (λ { (y , hf , hh) → y , subst ⟨_⟩ (sym (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ []))) hf , subst ⟨_⟩ (sym (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ []))) hh })
有界関係の装置は一度だけ具体化され、その述語として結びの関係が与えられます。以下のすべてはこの一つの実例から読み出されます。
module Composite = Relation D C body (λ x z → Chain x z , squash₁) read fill
合成のグラフは、分出された関係そのものです。
K : S K = Composite.rel K-out : (x z : S) → ⟨ pr (fst x) (fst z) ∈ fst K ⟩ → ∥ Σ[ y ∈ S ] (⟨ pr (fst x) (fst y) ∈ fst F ⟩ × ⟨ pr (fst y) (fst z) ∈ fst H ⟩) ∥₁
逆の読みはそのまま引き継がれます。合成の中の符号化された対は、単に、(x, y) が最初のグラフに、(y, z) が第二のグラフにあるような中間の y を与えます。以下の四つの検証はすべて、この一つの読み手が駆動します。
K-out = Composite.pair-out
順方向の読みは合成の法則です。二つの対がそれぞれ二つのグラフにある中間の y が与えられれば、切り詰められた証人が装置に渡され、装置は x と z の符号化された対を合成の中に置きます。
K-in : (x y z : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst z ∈ fst C ⟩ → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ pr (fst y) (fst z) ∈ fst H ⟩ → ⟨ pr (fst x) (fst z) ∈ fst K ⟩ K-in x y z mx mz hf hh = Composite.into x z mx mz ∣ y , hf , hh ∣₁
合成は次に、四条件を自分の力で満たさねばなりません。環境は合成のグラフと最初の定義域を対にします。まず一価性です。
γK : S ^ 2 γK = K ∷ D ∷ [] svK : ⟨ γK ⊨ svAt zero ⟩
合成が x を二つの値 y と y' に対にするとします。切り詰められた二つの結びを解くと中間の w と w' が現れ、(x, w) と (x, w') が最初のグラフにあります。
svK = svAt-in zero γK (λ x y y' p q → PT.rec (setIsSet (fst y) (fst y')) (λ { (w , (hf , hh)) → PT.rec (setIsSet (fst y) (fst y')) (λ { (w' , (hf' , hh')) → svAt-out zero γH svH w y y' hh
最初のグラフの一価性が w と w' を同一視し、その同一視は第二のグラフの対へ輸送され、第二の一価性が y と y' を同一視します。目標は h-集合の中のパス、すなわち命題なので、二度の切り詰めの消去は正当です。
(subst (λ t → ⟨ pr t (fst y') ∈ fst H ⟩) (sym (svAt-out zero γF svF x w w' hf hf')) hh') }) (K-out x y' q) }) (K-out x y p))
次に単射性を検証します。ここで二つのグラフの使う順序が重要です。第二のグラフの単射性を先に使い、最初のグラフの単射性を後に使います。
ijK : ⟨ γK ⊨ injAt zero ⟩
合成が y に x と x' の両方を送るとします。切り詰められた二つの結びが中間の w と w' を与えます。(x, w) と (x', w') は最初のグラフにあり、(w, y) と (w', y) は第二のグラフにあります。
ijK = injAt-in zero γK (λ y x x' p q → PT.rec (setIsSet (fst x) (fst x')) (λ { (w , (hf , hh)) → PT.rec (setIsSet (fst x) (fst x')) (λ { (w' , (hf' , hh')) → injAt-out zero γF ijF w x x' hf
共通の値 y における第二のグラフの単射性が w と w' を同一視し、今や共通の中間における最初のグラフの単射性が x と x' を同一視します。
(subst (λ t → ⟨ pr (fst x') t ∈ fst F ⟩) (sym (injAt-out zero γH ijH y w w' hh hh')) hf') }) (K-out x' y q) }) (K-out x y p))
合成の定義域における全域性は同値です。x が最初の定義域に属するのは、合成の値をもつとき、そのときに限ります。二つの向きが導入の形に渡されます。
dmK : ⟨ γK ⊨ domAt zero (suc zero) ⟩ dmK = domAt-intro zero (suc zero) γK (λ x → fwd x , bwd x)
一つの向きは、最初のグラフの定義域の条件をそのまま消去します。
where fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst K) ⟩ → ⟨ fst x ∈ fst D ⟩ fwd x = PT.rec (snd (fst x ∈ fst D)) (λ { (y , p) → PT.rec (snd (fst x ∈ fst D))
x が合成の値をもつなら、結びの証人が中間の w を示し、(x, w) が最初のグラフにあります。定義域のアトム自身の消去をその対に施せば、x が D の中に置かれます。この向きで第二のグラフは役に立ちません。
(λ { (w , (hf , _)) → domAt-out zero (suc zero) γF dmF x w hf }) (K-out x y p) })
もう一つの向きは、二つの導入をつなぎます。D の x が与えられると、最初のグラフの定義域の導入が中間の w を与え、(x, w) が最初のグラフにあり、その値域の条項が w を中間の集合に置きます。
bwd : (x : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst K) ⟩ bwd x mx = PT.rec squash₁ (λ { (w , hf) → PT.rec squash₁ (λ { (z , hh) → ∣ z , K-in x w z mx (ranH w z hh) hf hh ∣₁ })
第二のグラフの定義域の導入は w で (w, z) をもつ z を産み、第二のグラフの値域の条項が z を C に置きます。そして合成の法則が x と z の対を合成の中に置きます。どちらの段階も切り詰められ、結論もそうです。
(domAt-in zero (suc zero) γH dmH w (ranF x w hf)) }) (domAt-in zero (suc zero) γF dmF x mx)
値域の条件は、第二のグラフの値域の条項を中間の値に適用したものです。合成の対を解けば結びの証人が現れ、その第二成分が第二のグラフの中で中間と z を対にするので、条項が z を C の中に置きます。
ranK : (x z : S) → ⟨ pr (fst x) (fst z) ∈ fst K ⟩ → ⟨ fst z ∈ fst C ⟩ ranK x z h = PT.rec (snd (fst z ∈ fst C)) (λ { (w , (_ , hh)) → ranH w z hh }) (K-out x z h)
三つの読みの条件と値域の条項が揃うのは、符号化された単射を提示の間の関数として読み戻すための条件にちょうど合います。したがって合成もこの読みを認めます。このモジュールがそれを非公開で担います。公開されて渡るのはグラフと四条件だけなので、この読みにそれ以外は要りません。
private module Sm = Small K D C svK dmK ijK ranK
包含の符号化
包含には新しい構成は要りません。D が C に含まれるなら、D 上の恒等写像はもともと C への写像です。符号化されるのはその写像のグラフであり、対象言語では値の枠と添字の枠の間の等号として書かれます。モジュールは二つの集合と点ごとの包含を受け取ります。
module InclGraph (D C : S) (sub : (z : V ℓ) → ⟨ z ∈ fst D ⟩ → ⟨ z ∈ fst C ⟩) where
定義可能な写像のレコードは、定義域上の恒等で満たされます。
private M : DefinableMap M = record { dom = D ; cod = C ; fn = λ x _ → x
関数は各要素を自分自身へ送り、点ごとの包含がすべての値が C に着地することを証明します。
; into = λ x mx → sub (fst x) mx
グラフの論理式は二つの枠の間の等号であり、それが関数自身の値について成り立つことは定義的です。解の一意性には、等号の底の等しさを使います。どんな解も等式を満たしますが、それは底の要素の間の等しさであり、構成可能性が命題なので、この底の等しさは台の要素の等しさへ持ち上がります。関数の値と無関係な解が除かれるのは、このためです。
; graph = var zero ≐ var (suc zero) ; defines = λ _ _ → refl ; only = λ _ _ _ h → Σ≡Prop (λ w → snd (isL w)) h }
共有の構成はこの写像を三つの読みの条件をもつグラフへ変えますが、底の関数が単射であることの証明を外部から要求します。恒等写像の場合これは直接です。仮定は二つの入力の像を等しくしますが、恒等写像のもとで像の等しさは入力の等しさです。したがって、等式をそのまま返す渡された継続が、求める証明にちょうどなります。
module I = DefinableInj M (λ _ _ _ _ e → e) using ( F; code ) opaque G : S G = I.F
グラフと四条件のすべてが、D から C への単射の符号として一緒に渡されます。利用者は包みを一つの単位として受け取り、開く必要はありません。
opaque unfolding G code : InjCode G D C code = I.code
同じグラフが、共有の読みを通して、D と C の提示の間の関数として読み戻されます。この読みは非公開のモジュールが担います。公開されて渡る結果はグラフとその四条件であり、この読みに必要なのはそれだけです。
private module Sm = Small G D C (code .fst) (code .snd .fst) (code .snd .snd .fst) (code .snd .snd .snd)
導かれた関数は incl と名付けられ、その道すじが重要です。D の提示の索引は底の要素を名指し、その要素は D に属し、したがって包含によって C に属します。関数は次に、C 自身の提示のその要素での繊維を取ります。すなわち、その要素を提示する C の索引です。索引を直接輸送するのではなく、要素と繊維を通して取り戻します。
opaque incl : ⟪ fst D ⟫ → ⟪ fst C ⟫ incl = Sm.small
内部存在の水準における包含と合成
これまでの構成はグラフを産みます。内部の単射関係が要求するのは、グラフが存在することだけです。持ち上げは直接です。包含は恒等グラフを証人として与え、主張はその周りで切り詰められます。基数の議論が包含を受け取るのは、この形です。
inclusion-coded : (a b : S) → ((z : V ℓ) → ⟨ z ∈ fst a ⟩ → ⟨ z ∈ fst b ⟩) → InjL a b inclusion-coded a b sub = ∣ I.G , I.code ∣₁ where module I = InclGraph a b sub
合成も同様に持ち上がります。PT.rec2 は二つの証人を局所的に取り出して合成を作り、結果を再び切り詰めるので、代表を大域的に選ぶ必要はありません。
injl-trans : (a b c : S) → InjL a b → InjL b c → InjL a c injl-trans a b c = PT.rec2 PT.squash₁ step where
二重の消去は、二つの証人を局所的に解きほぐし、検証済みの構成で合成を組み立て、結果を改めて切り詰めます。代表の大域的な選択は行いません。二つの証人は、構成の仮定として存在するだけで、保持されることはありません。
step : Σ[ F ∈ S ] InjCode F a b → Σ[ H ∈ S ] InjCode H b c → InjL a c step (F , svF , dmF , ijF , ranF) (H , svH , dmH , ijH , ranH) = ∣ K.K , (K.svK , K.dmK , K.ijK , K.ranK) ∣₁
合成のモジュールが検証のすべてを担うので、この水準では合成の法則は一行です。
where module K = Comp a b c F H svF dmF ijF ranF svH dmH ijH ranH
主要な実例は、順序数 C の要素 D から始まります。仮定は D が順序数 C に属することだけです。C の推移性により、D の各要素が C の要素であることが従い、これが符号化の必要とする点ごとの包含にほかなりません。モジュールはこの対に対して包含の構成を開くので、そのグラフ・符号・導かれた写像が一つの名のもとで使えます。
module OrdIncl (C : S) (oC : IsOrd (fst C)) (D : S) (D∈C : ⟨ fst D ∈ fst C ⟩) where open InclGraph D C (λ _ z∈D → oC .fst z∈D D∈C) public
まとめ
三つの結果が内部の基数の議論に仕えます。有限の排除は、ω から任意の有限順序数の平方への単射が存在しないことを示します。ω の要素は単に数項であり、提示の型 ⟪ # n ⟫ と有限集合 Fin n の間には両方向それぞれに単射があり、抽象的な追跡は、有限の平方への単射の存在を仮定すると、大きい有限集合から小さい有限集合への単射を導きます。合成は二つの符号化された単射を一つにし、結びの関係を通して一価性・定義域における全域性・単射性・値域の条項を検証します。包含は恒等グラフによって点ごとの包含を符号化された単射へ変えます。存在の水準では、どちらの操作も切り詰められた内部の関係へ持ち上がるので、基数の上界の構成と比較を、L の中に住むグラフだけを通して行えます。