無限な構成可能段階を数える道具

無限順序数 δ の段階 Lset δ を L の内部で数えるには、二つの材料が要ります。基底の単射 Lω ↪ ω と、単射を有限環境へ持ち上げる方法です。この章はその両方を供給します。ここで証明されることは、すべて本文で名指しされた構成についてのものです。

{-# OPTIONS --cubical --safe --guardedness #-}

本章では、固定した宇宙レベルにおける排中律を仮定します。この仮定は章全体で用いる構成に受け継がれます。本章内でとくに明瞭な役割は、有限段階の一覧から名前を探索することと、順序数の三分律によって崩壊値を ω と比較することです。

open import Base.Prelude
open import Base.Classical using ( LEM )

したがって、すべての構成はただ一つの仮定 lem : LEM (ℓ-suc ℓ) を共有します。とくに、後の有限探索は排中律から得られるものであり、選択原理を用いるものではありません。

module L.GCH.StageCountingTools {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

以下で使う内部グラフは、L 自身が解釈できる論理式で記述する必要があります。等号、所属、連言、含意、有界量化子と非有界量化子によって、関係が全域的で一価な単射であることと、その有限環境への作用を表します。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _≐_; _∈̇_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

議論では一貫して二つの水準のデータを扱います。累積階層の集合には、その要素を名指す小さな提示があり、L の要素には構成可能性の証明も添えられています。この二つの水準を行き来することで、内部グラフを提示のインデックス上の通常の関数として働かせられます。

open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Model {ℓ} using ( ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset→isL )

順序数の構造は二度使われます。数項は環境の有限な定義域を識別し、構成可能段階の順序は後で Lset ω の標準的な整列順序を与えます。その後、三岐性によって順序数崩壊の各値が ω に対してどこに位置するかを判定します。

open import L.Ordinal {ℓ} using ( ∈#-elim; mem-ord; ω-ord; numeral-ord; #∈ω )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )

符号化された単射は順序対の集合で表されます。その四つの条件は、グラフが一価であること、定義域が指定された集合とちょうど一致すること、入力について単射であること、値が指定された目標に属すことです。章の前半では、このように実際に与えられた符号化グラフから出発します。

open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-in; injAt-out; module Small )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )

各自然数 n について、A に値を取る長さ n の環境には具体的な提示があります。集合 seqL A はすべての有限な長さをまとめたものです。したがって、成分ごとに作用して長さを保つ写像こそ、A 上のすべての有限列を B 上の有限列へ送るために必要な操作です。

open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envSet-in; envSet-out; envOver; module Recover )
open import L.Choice.NameComparison {ℓ} lem using ( domAt-numeral; domAt-fill )
open import L.Choice.StageOrders {ℓ} lem
  using ( carry; memOf; orderAt; orderAt-step; relOf

後半では、Lset ω の要素をまず誕生段階で並べ、誕生段階が等しいときにはその段階の局所的な順序で並べます。この区別は欠かせません。前者が後者の前者であっても誕生段階が同じ場合がありますが、それでも各前者はその共通段階の後続段階に属します。

        ; birth-mem; module Family )
  renaming ( Mem to MemOf )
open import L.Choice.OrderTable {ℓ} lem using ( Related; IsRel; ixRel-rep; ixRel-fill )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-spec )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}

この整列順序を崩壊させると、Lset ω の各要素に順序数が割り当てられます。次の課題は、すべての崩壊値が ω に属すことを示すことです。証明では前者切片を一つずつ有限な構成可能段階で抑え、ω からその段階への単射を排除します。

  using ( SWO; lt; eq; gt ) renaming ( Tri to TriW )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )

有限列の符号化と崩壊の議論は、後の基数計算で合流します。前者はすでに与えられた符号化単射を成分ごとに移し、後者は基礎となる結論 Lset ω ↪ ω を与えます。どちらも全単射を主張せず、任意の無限列を数えるものでもありません。

open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seqL-out )
open import L.Ordinal.SquareLaw {ℓ} lem using ( module FiniteBase )
open FiniteBase using ( fromFin; fromFin-inj )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; ω-limit; finite-excl-ω )

有限段階には、その全要素を列挙する有限な名簿があります。重複していてもよいので、この名簿は全単射ではなく、全射的に名前を与えるものです。それで十分です。排中律を使った有界探索により、与えられた各要素の名前を一つ見つけられます。

open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( Tally; StageOrder; stageOrder; finiteStage )  -- lint-agda: keep (StageOrder used as the projection qualifier)
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )

見つけた名簿のインデックスによって、有限段階の各要素を有限順序数の提示へ送れます。ω からの単射があると仮定してこの命名写像と合成し、得られた値を対角線上で二重にすると、有限平方の排除定理に反します。

open import Cubical.Data.Nat.Order using ( _<_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.FinSet using ( DecΣ )
open import Cubical.Relation.Nullary using ( decRec; yes; no )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId'; inj-toℕ )

後で現れるいくつかの等しさは、第二成分が証明である依存対についてのものです。その成分は命題なので、底の集合の等しさから包装された要素の等しさが決まります。これにより、L の要素、その提示、グラフの符号の間を円滑に行き来できます。

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ2; isPropΠ3 )

数項には、環境の長さを示す以外にも役割があります。周囲の集合が ω に属すという主張は、それが何らかの数項に等しいことだけを述べ、自然数による大域的に選ばれた表示を保持しません。後の消去もこの命題性を守ります。

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 ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

同じ区別は最後の数え上げにも当てはまります。InjL A B が保持するのは、A から B への単射を符号化する構成可能グラフが存在するという命題だけであり、大域的に選ばれた台の水準の関数を公開しません。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

これに対して、列の構成は特定のグラフ E と完全なデータ InjCode E A B から始まります。したがって、そのグラフから台の水準の関数を読み取り、成分ごとに用いた後、得られたグラフを InjL によって再び隠せます。

module SV = hPropStructure 𝒮ᵥ using ()

構成可能集合の要素から読み取った各項目は、L の推移性によってそれ自身も構成可能です。この基本的な事実により、有限環境とそのグラフに現れる順序対を内部モデルの対象として扱えます。

module SL = hPropStructure 𝒮ʟ using ( S )
open SL using ( S )

充足の記法は、論理式の水準でのグラフの記述を、これらの周囲の所属の事実と結び付けます。妥当性補題を両方向に用いることで、具体的なグラフのデータから内部論理式を満たし、後でその論理式からデータを読み戻せます。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

自然数 k に対し、nn k は数項 # k とその構成可能性の証明を組にします。この包装された数項を、充足の環境における有限な定義域の対象として用います。

nn : ℕ → S
nn k = # k , numL k

後のグラフ論理式では、束縛子が何重にも入れ子になります。i0、i1 などの名前は対応する De Bruijn 位置の略記であり、i0 は常に最も新しく束縛された変数を表します。

private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0

束縛子が一つ加わるたびに、それまでの変数は一つ後の位置へ移ります。型の付いた略記がその移動をまとめて記録するので、長い後続式を繰り返さずに論理式の数学的な形を示せます。

  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)))))

i6 までの位置があれば、入力環境 s、その像 y、共通の定義域 n、インデックス i、そして E で結ばれる二つの項目を同時に参照できます。

  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

後で符号化された単射を表す論理式では、さらに深い位置もいくつか必要になります。同じ命名法を延長しておけば、追加の束縛子を導入しても記法の約束を変えずに済みます。

  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
  i9 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc k))))))))))

最後の略記で、このモジュールに必要な位置がすべてそろいます。これらの名前は数学的な仮定を何も加えず、変数位置の管理を読みやすくするだけです。

  i9 = suc i8

環境の長さと外延性

最初の剛性の事実は、二つの符号化された環境の長さを比較します。一つの底の集合が env h とも env h' とも等しく、各項目が構成可能なら、二つの長さは等しくなります。符号化された環境の定義域はその長さの数項であり、同じ集合の二つの読みが数項の射影で同一視されるのです。

env-len : (E : S) {n n' : ℕ} (h : Fin n → V ℓ) (h' : Fin n' → V ℓ)
        → ((i : Fin n) → ⟨ isL (h i) ⟩) → ((i : Fin n') → ⟨ isL (h' i) ⟩)
        → fst E ≡ env h → fst E ≡ env h' → n ≡ n'
env-len E {n} {n'} h h' cg cg' q q' =
  #-inj′ (domAt-numeral (suc zero) zero (nn n ∷ E ∷ []) n' h' cg' q'

証明は、最初の提示の定義域を n の数項で埋め、同じ定義域を n' の数項として読み戻し、数項の単射性を適用します。結論は長さの等式だけであり、二つの提示の関数の等式ではありません。

            (domAt-fill (suc zero) zero (nn n ∷ E ∷ []) n h cg q refl))

二つ目の剛性の事実では、二つの列の長さがすでに同じで、符号化されたグラフも等しいと仮定します。両方のグラフでインデックスに対応する数項のキーを参照すると、対応する項目の等しさが得られます。逆向き、すなわち各点の等しさからグラフの等しさを作る方向は、後で必要になる箇所で証明します。

env-pt : {n : ℕ} (h h' : Fin n → V ℓ) → env h ≡ env h' → (i : Fin n) → h i ≡ h' i
env-pt h h' q i = subst ⟨_⟩ (lookup-spec h' i (h i))
  (subst (λ w → ⟨ pr (# (toℕ i)) (h i) ∈ w ⟩) q
    (subst ⟨_⟩ (sym (lookup-spec h i (h i))) refl))

符号化された単射を有限列へ持ち上げる

持ち上げのモジュールは、構成可能なグラフ E に対して四つのデータとともに述べられます。一価性、A の上の全域性、A の上の単射性、そして B の中の値です。これらはちょうど、A から B への符号化された単射の四つの条項です。

module SeqMap (A B E : S)
              (sv : ⟨ (E ∷ A ∷ []) ⊨ svAt zero ⟩)
              (dm : ⟨ (E ∷ A ∷ []) ⊨ domAt zero (suc zero) ⟩)
              (ij : ⟨ (E ∷ A ∷ []) ⊨ injAt zero ⟩)
              (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst E ⟩

最後の値域条件が述べるのは、E に現れるすべての値が B に属すことだけです。B の各要素が像になることは要求しないので、このデータが表すのは単射であり、全射や全単射ではありません。

                   → ⟨ fst y ∈ fst B ⟩) where

抽出の仕組みは、内部のグラフを、A と B の提示の間の実際の関数として読みます。一価性により各値の繊維は命題になるので、選択の原理なしに値を復元できます。

  module Sm = Small E A B sv dm ij ran using ( at; fib; small; small-inj; module E )

抽出された関数は不透明に保たれます。後の議論は、そのグラフと単射性を通してだけそれを使います。

  opaque
    f : ⟪ fst A ⟫ → ⟪ fst B ⟫
    f = Sm.small

グラフの記録は、索引の提示された要素と提示された像の順序対が E に属することを述べます。これは、項代数自身のグラフの記録から、提示された値の同一視に沿って運ばれます。

    f-graph : (m : ⟪ fst A ⟫)
            → ⟨ pr (⟪ fst A ⟫↪ m) (⟪ fst B ⟫↪ (f m)) ∈ fst E ⟩
    f-graph m = subst (λ w → ⟨ pr (⟪ fst A ⟫↪ m) w ∈ fst E ⟩)
      (sym (Sm.fib m .snd)) (Sm.E.toFun-graph (Sm.at m))

抽出された関数は A の提示の上で単射です。これが、列の持ち上げが成分ごとに受け継ぐ、各点の単射性です。

    f-inj : (m n : ⟪ fst A ⟫) → f m ≡ f n → m ≡ n
    f-inj = Sm.small-inj

A の環境の項目は、提示の埋め込みを通して周囲の集合として読まれます。

  vA : {n : ℕ} → Ix A n → Fin n → V ℓ
  vA g i = ⟪ fst A ⟫↪ (g i)

B の環境の項目についても同様です。

  vB : {n : ℕ} → Ix B n → Fin n → V ℓ
  vB h i = ⟪ fst B ⟫↪ (h i)

持ち上げられた割り当ては、抽出された関数を項目ごとに適用します。A の長さ n の環境の像は B の長さ n の環境であり、長さは変わりません。

  fg : {n : ℕ} → Ix A n → Ix B n
  fg g i = f (g i)

A の環境のどの項目も構成可能です。A への所属を、構成可能性の推移性に沿って運ぶからです。

  isLA : {n : ℕ} (g : Ix A n) (i : Fin n) → ⟨ isL (vA g i) ⟩
  isLA g i = isL-trans (member (fst A) (g i)) (snd A)

B の環境の項目についても同様です。

  isLB : {n : ℕ} (h : Ix B n) (i : Fin n) → ⟨ isL (vB h i) ⟩
  isLB h i = isL-trans (member (fst B) (h i)) (snd B)

インデックス対象 i に対し、Ent y s i は、s(i)=u、y(i)=v であり、グラフ E が u を v へ送るような模型の要素 u と v がもっぱら存在することを述べます。これらの証人と三つのグラフ所属の事実は、すべて命題的切り詰めの下に保たれます。

  Ent : (y s i : S) → Type (ℓ-suc ℓ)
  Ent y s i = ∥ Σ[ u ∈ S ] Σ[ v ∈ S ]
      ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
      × ⟨ pr (fst i) (fst v) ∈ fst y ⟩
      × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ ) ∥₁

台の水準での読み Wit y s は、ある対象 n が s の定義域であり、y が固定された目標 B 上で同じ n を定義域にもつ環境であり、すべての i∈n が Ent y s i を満たすことを、もっぱら存在する形で述べます。したがって y は s と同じ有限な形をもち、その各項目は s の項目の E による像です。

  Wit : (y s : S) → Type (ℓ-suc ℓ)
  Wit y s = ∥ Σ[ n ∈ S ]
      ( ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      × ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      × ((i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) ) ∥₁

項目の論理式は、Ent に含まれる三つの等式をそのまま表します。存在量化された二つの値 u と v が s(i)=u、y(i)=v、E(u)=v を満たします。変数位置には、周囲の引数と二つの新しい証人がともに数えられています。

  opaque
    private
      entFo : Formula S 
      entFo = ∃̇ (∃̇ ( appAt i6 i2 i1 ∧̇ appAt i5 i2 i0 ∧̇ appC E i1 i0 ))

論理式全体は、まず共通の定義域 n を束縛し、次に対象 b を束縛して、それが固定した定数 B に等しいことを要求します。そして y が定義域 n をもつ b 上の環境であり、すべての i∈n で項目の論理式が成り立つと述べます。等式 b=B により、これは意図した目標上の環境になります。

    fo : Formula S 
    fo = ∃̇ ( domAt i2 i0
           ∧̇ ∃̇ ( (var i0 ≐ con B)
                ∧̇ envOverAt i2 i1 i0
                ∧̇ ∀̇∈ (var i1) entFo ) )

論理式から項目を読み取るため、証明は入れ子になった二つの存在証人 u と v を順に消去します。Ent y s i 自体が命題的切り詰めによって命題になっているので、この消去は正当です。

    private
      entOut : (y s n b i : S) → ⟨ (i ∷ b ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩ → Ent y s i
      entOut y s n b i = PT.rec squash₁ (λ { (u , hv) →
        PT.rec squash₁ (λ { (v , (h1 , (h2 , h3))) →
          let γ = v ∷ u ∷ i ∷ b ∷ n ∷ y ∷ s ∷ [] in

二つの環境の適用とグラフ E の適用についての妥当性法則により、論理式の充足を三つの周囲の所属へ変換します。読み戻した u、v とこれらの所属を組にすると、必要な切り詰められた項目が得られます。

          ∣ u , v
          , ( subst ⟨_⟩ (appAt-adequate i6 i2 i1 γ) h1
            , subst ⟨_⟩ (appAt-adequate i5 i2 i0 γ) h2
            , subst ⟨_⟩ (appC-adequate E i1 i0 γ) h3 ) ∣₁ }) hv })

逆方向では、切り詰められた項目を論理式の充足へ写します。同じ三つの妥当性の等しさを逆向きに用い、周囲のグラフ所属を二つの環境適用の条項と E の適用の条項へ変換します。

      entIn : (y s n i : S) → Ent y s i → ⟨ (i ∷ B ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩
      entIn y s n i = PT.map (λ { (u , v , (h1 , h2 , h3)) →
        let γ = v ∷ u ∷ i ∷ B ∷ n ∷ y ∷ s ∷ [] in
        u , ∣ v , ( subst ⟨_⟩ (sym (appAt-adequate i6 i2 i1 γ)) h1
                  , subst ⟨_⟩ (sym (appAt-adequate i5 i2 i0 γ)) h2

二つの証人を入れ子の存在量化子の下へ戻すと、E のグラフ所属の条項によって項目の論理式の充足が完成します。こうして entOut と entIn は、各インデックスで必要となる正確な対応を与えます。

                  , subst ⟨_⟩ (sym (appC-adequate E i1 i0 γ)) h3 ) ∣₁ })

本体の読み取りは、外側の論理式から現れる三つの成分を受け取ります。n は s の定義域であり、補助対象 b の底の集合は B の底の集合と等しく、y は定義域 n をもつ b 上の環境で、その各インデックスが項目の論理式を満たします。これらを Wit y s へ変換することが目標です。

      bodyOut : (y s n b : S)
              → ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
              → fst b ≡ fst B
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ ∀̇∈ (var i1) entFo ⟩

b と B の底の集合の等しさに沿って、b 上の環境であるという主張を固定された目標 B へ移します。各有界インデックスでの項目の論理式を entOut で読み戻し、共通の定義域とこれら二つの成分を命題的切り詰めの下にまとめます。

              → Wit y s
      bodyOut y s n b hd eb he hS =
        ∣ n , ( hd
              , envOverAt-transport (b ∷ n ∷ y ∷ s ∷ []) (B ∷ n ∷ y ∷ s ∷ [])
                  i2 i1 i0 i2 i1 i0 refl refl eb he

有界全称の節は各点で用います。各 i∈n について、entOut がその充足の証明を Ent y s i へ変換します。これらの項目を、定義域の等式および移送した環境条件と合わせると、切り詰められた証人 Wit y s の三成分が得られます。

              , λ i i∈n → entOut y s n b i (hS i i∈n) ) ∣₁

グラフ論理式全体を外向きに読むには、まず切り詰められた証人 n を除去し、次に切り詰められた証人 b を除去します。それらに伴う節から、定義域条件、等式 fst b ≡ fst B、環境条件、有界ステップ条件が得られ、bodyOut がちょうどこれらを Wit y s に変えます。Wit y s 自体が命題的に切り詰められているので、この二つの除去は正当です。

    fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
    fo-out y s = PT.rec squash₁ (λ { (n , (hd , hb)) →
      PT.rec squash₁ (λ { (b , (eb , (he , hS))) → bodyOut y s n b hd eb he hS }) hb })

逆に、ホスト側の証人は外側の存在量化に n を、内側の存在量化に固定された要素 B を与えます。反射律がこの要素は必要な目標を表すことを示し、entIn が各点の項目を有界論理式へ戻します。したがって fo-out と fo-in は、Wit に対する fo の妥当性を両方向から確立します。

    fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
    fo-in y s = PT.rec (snd ((y ∷ s ∷ []) ⊨ fo))
      (λ { (n , (hd , he , hS)) →
        ∣ n , ( hd , ∣ B , ( refl , he , λ i i∈n → entIn y s n i (hS i i∈n) ) ∣₁ ) ∣₁ })

A 上の長さ N の列 g、台の要素 s、および s の底の集合を g の環境グラフと同一視する等式を固定します。この具体的な表示から成分ごとの像を構成し、同じグラフ論理式を満たす任意の出力が同じ底の集合をもつことを示せます。

  module AtSeq (N : ℕ) (g : Ix A N) (s : S) (e : fst s ≡ fst (envS A g)) where

意図する出力は、成分ごとの像 fg g の環境グラフです。添字 j での値は f (g j) なので、源の列と目標の列は同じ有限長をもち、対応する項は入力グラフ E によって関係づけられます。

    y₀ : S
    y₀ = envS B (fg g)

次の補題は、この証人を構成するために必要な基本的な所属の事実を与えます。各座標の対は環境グラフに属します。この補題が局所的なのは、この小節で公開する結論が像の環境全体の存在と一意性だからです。

    private

項目の補題は、関数の符号化されたグラフが、それぞれの自然数の添字とその値の順序対を含むと言います。証明は、環境の構成子の仕様から来ます。その対は定義によってそこにあるのです。

      at : {k : ℕ} (h : Fin k → V ℓ) (j : Fin k)
         → ⟨ pr (# (toℕ j)) (h j) ∈ env h ⟩
      at h j = subst ⟨_⟩ (sym (lookup-spec h j (h j))) refl

標準的な像はホスト側の述語 Wit を満たします。数項 nn N が共通の定義域を記録し、he が y₀ は長さ N の B 上の環境であることを記録し、step が N 未満の各添字で関係を確かめます。最後にこの三つの節を命題的切り詰めの中へ入れ、後の議論が特定の分解に依存しない形で存在だけを残します。

    wit : Wit y₀ s
    wit = ∣ nn N , ( hd , he , step ) ∣₁
      where
      hd : ⟨ (nn N ∷ y₀ ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      hd = domAt-fill i2 i0 (nn N ∷ y₀ ∷ s ∷ []) N (vA g) (isLA g) e refl

事実 envOver B (fg g) は、初めは B、nn N、y₀ だけを含む短い環境について述べられています。移送補題は同じ論理式を、さらに s を含む長い割当てへ移します。三つの反射律の証明は、論理式が使う各位置にまったく同じ要素が残っていることを示します。したがって、使われない源の列を加えても環境についての主張は変わりません。

      he : ⟨ (B ∷ nn N ∷ y₀ ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      he = envOverAt-transport (B ∷ nn N ∷ y₀ ∷ []) (B ∷ nn N ∷ y₀ ∷ s ∷ [])
             i2 i1 i0 i2 i1 i0 refl refl refl (envOver B (fg g))

それぞれの位置でのステップの条項は、数項の所属を有界の自然数へ消去することで証明されます。消去されたデータが、両方の列で値の得られる具体的な添字を名指します。

      step : (i : S) → ⟨ fst i ∈ # N ⟩ → Ent y₀ s i
      step i i∈N = PT.map atIndex (∈#-elim N (fst i) i∈N)
        where
        atIndex : Σ[ k ∈ ℕ ] ((k < N) × (fst i ≡ # k))
                → Σ[ u ∈ S ] Σ[ v ∈ S ]

復元された有限添字 j に対し、必要な項目は源の値 vA g j、目標の値 vB (fg g) j、および三つのグラフ所属からなります。源の環境は j に前者を、目標の環境は同じ位置に後者を格納し、E は前者を後者に関係づけます。構成可能性の証明により、二つの値はいずれも台 S の要素になります。

                    ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
                    × ⟨ pr (fst i) (fst v) ∈ fst y₀ ⟩
                    × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
        atIndex (k , p , ei) =
            (vA g j , isLA g j) , (vB (fg g) j , isLB (fg g) j)

環境の項目補題が最初の二つの所属を与え、それらを、与えられた位置と j の数項を同一視する等式に沿って移送します。源の環境については、さらに提示の等式 e に沿って移送します。三つ目の所属はグラフ定理 f-graph から得られます。有限添字 j は、直前に得た有界自然数からすぐ下で定義されます。

          , ( subst2 (λ a w → ⟨ pr a (vA g j) ∈ w ⟩) (sym qi) (sym e) (at (vA g) j)
            , subst (λ a → ⟨ pr a (vB (fg g) j) ∈ fst y₀ ⟩) (sym qi) (at (vB (fg g)) j)
            , f-graph (g j) )
          where
          j : Fin N

内部の添字 j は、有界の自然数の有限の復号から構成され、数項の等式は、所属の輸送と添字の値の復元を合成したものです。

          j = fromℕ' N k p
          qi : fst i ≡ # (toℕ j)
          qi = ei ∙ cong #_ (sym (toFromId' N k p))

一意性の証明では、Wit y s を満たす任意の候補 y から始め、その基礎にある集合が y₀ のものと等しいことを目標とします。累積階層の等しさは命題なので、切り詰められた証人を除去できます。三つの節を取り出した後、局所モジュール Only がそれらから必要な等式を導きます。

    only : (y : S) → Wit y s → fst y ≡ fst y₀
    only y = PT.rec (setIsSet (fst y) (fst y₀))
      (λ { (n , (hd , he , hS)) → Only.final n hd he hS })
      where
      module Only (n : S)

内側のモジュールは、証人の三つの条項を集めます。定義域の条件、環境の上の条件、そしてすべての位置でのステップの条項です。

                  (hd : ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩)
                  (he : ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩)
                  (hS : (i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) where

数項の等式が、定義域の符号化の妥当性によって、未知の長さを既知の長さ N と同一視します。

        qn : fst n ≡ # N
        qn = domAt-numeral i2 i0 (n ∷ y ∷ s ∷ []) N (vA g) (isLA g) e hd

環境条件と復元された長さから、候補 y を環境グラフとして表示する添字関数 gR : Ix B N が定まります。この定義は、切り詰められたデータを除去して構成されるため不透明です。以後はその除去を展開せず、述べられた等式を通して復元関数を使います。

        opaque
          gR : Ix B N
          gR = Recover.g B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he

復元はさらに、y の基礎にある集合が gR から生成される環境グラフであることを示します。この等式によって、証人に含まれる任意の提示を固定長の座標表示へ置き換えられるので、一意性を座標ごとに確かめられます。

          gR-eq : fst y ≡ fst (envS B gR)
          gR-eq = Recover.recovers B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he

各添字 j で、ステップの節は命題的切り詰めのもとに、源の値、候補となる目標値、および両者を結ぶ三つのグラフ所属を与えます。目標の等式は命題なので、PT.rec はこれらのデータを read に渡せます。この補題が表示された二つの値の等しさを示し、B の表示の単射性から gR j ≡ fg g j が従います。

        pt : (j : Fin N) → gR j ≡ fg g j
        pt j = ↪-inj {a = fst B} (PT.rec (setIsSet _ _) read (hS (nn (toℕ j)) j∈n))
          where
          j∈n : ⟨ # (toℕ j) ∈ fst n ⟩
          j∈n = subst (λ w → ⟨ # (toℕ j) ∈ w ⟩) (sym qn) (#mono (toℕ j) N (toℕ<n j))

読み出しの補題は、ステップの条項が供給するものを述べます。二つの要素と三つの所属であり、源の列の中の引数、未知の環境の中の値、そして符号化された対でそれらを結ぶ関係の事実を同定します。

          read : Σ[ u ∈ S ] Σ[ v ∈ S ]
                   ( ⟨ pr (# (toℕ j)) (fst u) ∈ fst s ⟩
                   × ⟨ pr (# (toℕ j)) (fst v) ∈ fst y ⟩
                   × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
               → vB gR j ≡ vB (fg g) j

源の引数の等式は、源の環境の参照の仕様によって復元され、同定の等式に沿って運ばれます。

          read (u , v , (hu , hv , hE)) = sym qv ∙ qv'
            where
            qu : fst u ≡ vA g j
            qu = subst ⟨_⟩ (lookup-spec (vA g) j (fst u))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst u) ∈ w ⟩) e hu)

候補値 v には二つの記述があります。復元された環境から読み取ると fst v ≡ vB gR j が得られます。一方、hE は、E が復元された源の引数を v に関係づけることを述べます。その引数を vA g j と同一視した後、E の一価性によってこの辺を f-graph (g j) と比較し、fst v ≡ vB (fg g) j を得ます。

            qv : fst v ≡ vB gR j
            qv = subst ⟨_⟩ (lookup-spec (vB gR) j (fst v))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst v) ∈ w ⟩) gR-eq hv)
            qv' : fst v ≡ vB (fg g) j
            qv' = svAt-out zero (E ∷ A ∷ []) sv u v (vB (fg g) j , isLB (fg g) j) hE

最後の等式が、関数のグラフの事実と逆向きの引数の等式を合成して、二つの像の値の同定を完成させます。

                    (subst (λ w → ⟨ pr w (vB (fg g) j) ∈ fst E ⟩) (sym qu) (f-graph (g j)))

残るのは、座標ごとの一致を二つの環境グラフの等しさへ高めることです。必要なパスは y の復元された提示から始まり、標準グラフ y₀ に至ります。

        final : fst y ≡ fst y₀

関数外延性により、pt は二つの添字関数の等しさになります。そのパスに沿って envS B を動かすと二つの環境グラフが同一視され、これを gR-eq と合成して fst y ≡ fst y₀ を得ます。ここでのパスラムダは、この等しさに沿う環境グラフの cubical な作用を直接表しています。

        final = gR-eq ∙ λ i → fst (envS B (funExt pt i))

列の集合への所属は型として記録され、議論が、写す各要素とともにそれを運べるようにします。

  Mem : S → Type (ℓ-suc ℓ)
  Mem s = ⟨ fst s ∈ˢ fst (seqL A) ⟩

表示とは、長さ、添字の関数、そして二つの提示を同一視する等式の、切り詰められた記録です。切り詰められた形こそ、seqL-out が供給するものです。

  Rep : S → Type (ℓ-suc ℓ)
  Rep s = ∥ Σ[ n ∈ ℕ ] Σ[ g ∈ Ix A n ] (fst s ≡ fst (envS A g)) ∥₁

seqL A への所属から、seqL-out は命題的切り詰めのもとで長さ n と、対応する固定長環境集合への所属を与えます。その n に対して envSet-out は、切り詰められた添字関数と提示の等式を与えます。これらを写し、切り詰められた目標にだけ除去することで、大域的な表示を選ばずに二段階を合成できます。

  rep : (s : S) → Mem s → Rep s
  rep s m = PT.rec squash₁
    (λ { (n , hn) → PT.map (λ { (g , e) → n , g , e }) (envSet-out A n s hn) })
    (seqL-out A s m)

再帰の構造は seqL A を定義域、fo をグラフとします。各要素 s の切り詰められた表示から標準的な像の環境が定まり、AtSeq.wit はその像がグラフを満たすことを、AtSeq.only はほかのどの充足値も同じ基礎の集合をもつことを示します。したがって、このグラフは mereFunct が要求する意味で全域的かつ一価です。

  R : Recursion
  R = record
    { dom   = seqL A
    ; graph = fo
    ; funct = λ s m → mereFunct fo s (PT.map (λ { (n , g , e) →

具体的な表示 (n , g , e) に対する関数性の証人は、標準的な像 AtSeq.y₀、それが fo を満たす証明、およびほかのどの充足する台の要素もそれに等しいという証明からなります。構成可能性の証明は命題値のファイバーをなすので、Σ≡Prop は基礎にある集合の等しさを S での等しさへ持ち上げます。続いて PT.map が構成全体を切り詰めの中に保ちます。

        AtSeq.y₀ n g s e
        , ( fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e)
          , λ y' h → Σ≡Prop (λ v → snd (isL v)) (AtSeq.only n g s e y' (fo-out y' s h)) ) })
        (rep s m)) }

再帰の表の機構が開かれ、実際の関数、その値、そして値の一意性を供給します。

  module T = Of R using ( funct; val; val-uniq )

得られる値 fn s m は、s において fo を満たす一意な台の要素です。その構成は s の切り詰められた表示から始まりますが、一意性により、どの長さと添字関数でその列を表示しても値は変わりません。

  fn : (s : S) → Mem s → S
  fn = T.val

s が長さ n と添字関数 g で表示されるとき、計算された値 fn s m は標準的な成分ごとの像 AtSeq.y₀ n g s e に等しくなります。両方が s における再帰グラフを満たすので、一意性定理 T.val-uniq がこの等しさを与えます。この等式により、以後の証明では s について手元にあるどの表示からでも推論できます。

  fn-code : (s : S) (m : Mem s) (n : ℕ) (g : Ix A n) (e : fst s ≡ fst (envS A g))
          → fn s m ≡ AtSeq.y₀ n g s e
  fn-code s m n g e =
    T.val-uniq s m (AtSeq.y₀ n g s e) (fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e))

目標の列の集合への所属は、符号の等式に沿って運び、目標の列の集合の内向きの読み出しを適用することで証明されます。

  into : (s : S) (m : Mem s) → ⟨ fst (fn s m) ∈ˢ fst (seqL B) ⟩
  into s m = PT.rec (snd (fst (fn s m) ∈ˢ fst (seqL B)))
    (λ { (n , g , e) → subst (λ w → ⟨ fst w ∈ˢ fst (seqL B) ⟩) (sym (fn-code s m n g e))
           (seqL-in B n (envS B (fg g)) (envSet-in B (fg g))) })
    (rep s m)

以上の事実から seqL A から seqL B への写像が定まります。fo がそのグラフを、fn が各始域要素での一意な値を与え、into はその値が再び B 上の有限列であることを示します。残る課題は、二つの値が等しければ元の列も等しいと示すことです。

  D : DefinableMap
  D = record
    { dom = seqL A ; cod = seqL B ; 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) }

単射性を示すには、まず標準的な表示どうしを比較すれば十分です。表示上の長さが異なるかもしれない二つの成分ごとの像の環境が等しいと仮定します。補助補題 same は長さの等しさを復元し、二つ目の源の列を共通の有限添字型へ移送した後、各座標で f の単射性を使って源の環境グラフの等しさを示します。

  private
    same : (n : ℕ) (g : Ix A n) (n' : ℕ) (g' : Ix A n')
         → fst (envS B (fg g)) ≡ fst (envS B (fg g'))
         → fst (envS A g) ≡ fst (envS A g')
    same n g n' g' q =

二つの目標環境グラフの等しさから、env-len によって有限長の等しさが定まります。環境の符号化された定義域が、その長さを表す数項だからです。この等しさに沿って置換すると、問題は同じ Fin n で添字づけられた二つの列の比較に帰着し、局所的な型族 P が整列後に残る主張を記録します。

      subst P (env-len (envS B (fg g)) (vB (fg g)) (vB (fg g')) (isLB (fg g)) (isLB (fg g')) refl q)
        base g' q
      where
      P : ℕ → Type (ℓ-suc ℓ)
      P k = (h : Ix A k) → fst (envS B (fg g)) ≡ fst (envS B (fg h))

長さが共通になれば、env-pt は目標グラフの等しさを各添字での値の等しさとして読みます。B の表示の単射性により、これは f (g j) ≡ f (h j) となり、f-inj から g j ≡ h j が復元されます。関数外延性が源の添字関数を同一視し、したがってその環境グラフも同一視します。

          → fst (envS A g) ≡ fst (envS A h)
      base : P n
      base h q' = λ i → fst (envS A (funExt (λ j →
        f-inj (g j) (h j) (↪-inj {a = fst B} (env-pt (vB (fg g)) (vB (fg h)) q' j))) i))

任意の要素 s と s' について、その表示は命題的切り詰めのもとでしか得られません。累積階層の値は集合をなすため、目標の等式 fst s ≡ fst s' は命題です。そこで PT.rec2 により、各入力の表示を局所的に一つずつ取り出し、標準表示どうしの比較に渡せます。

  inj : (s : S) (m : Mem s) (s' : S) (m' : Mem s')
      → fst (fn s m) ≡ fst (fn s' m') → fst s ≡ fst s'
  inj s m s' m' q = PT.rec2 (setIsSet (fst s) (fst s'))
    (λ { (n , g , e) (n' , g' , e') →
        e

二つの符号等式は、実際の出力 fn s m と fn s' m' を、それぞれの標準的な像の環境と同一視します。これらを仮定された出力の等しさと合成すると same が必要とする前提が得られ、最後に提示の等式 e と e' が源の環境グラフの等しさを fst s ≡ fst s' へ戻します。

      ∙ same n g n' g'
          (sym (cong fst (fn-code s m n g e)) ∙ q ∙ cong fst (fn-code s' m' n' g' e'))
      ∙ sym e' })
    (rep s m) (rep s' m')

いま示した単射性により、この定義可能な写像は内部の符号化された単射 seqL A ↪ seqL B になります。そのグラフは同じ成分ごとの作用を記録しますが、結論に残るのは適切な符号の命題的な存在だけです。

  injL : InjL (seqL A) (seqL B)
  injL = Inj.injL D inj

公開される定理は、A から B への単射を証明する実際の符号化グラフ E から始めます。このグラフは一価で、定義域が A であり、単射的で、値域が B に含まれます。これら四つの成分を SeqMap に渡すと、seqL A から seqL B への符号化された単射の命題的に切り詰められた存在が得られます。この結果が扱うのは任意の長さの有限列であり、無限列ではありません。

seq-map : (A B E : S) → InjCode E A B → InjL (seqL A) (seqL B)
seq-map A B E (sv , dm , ij , ran) = SeqMap.injL A B E sv dm ij ran

量化変数を定数に固定する

釘づけの論理式は、一つの存在量化子を束縛して、自由な枠を選んだ定数に固定します。ある値が定数に等しく、内側の論理式を満たす、と言うだけです。

pinAt : ∀ {n} → S → Formula S (suc n) → Formula S n
pinAt c φ = ∃̇ ((var zero ≐ con c) ∧̇ φ)

内向きの読み出しは、定数を証人として示し、拡張された環境での本体の充足を与えます。

pin-in : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
       → ⟨ (c ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ pinAt c φ ⟩
pin-in c φ γ h = ∣ c , (refl , h) ∣₁

外向きには、存在量化から台の要素 z、その基礎にある集合と c のものとの等しさ、および z で本体が成り立つ証明を得ます。構成可能性は命題値なので、Σ≡Prop は基礎の集合の等しさを S における等式 z ≡ c へ持ち上げます。これに沿って移送すれば、固定された環境での充足が得られます。論理式の充足は命題なので、命題的切り詰めからのこの除去は正当です。

pin-out : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
        → ⟨ γ ⊨ pinAt c φ ⟩ → ⟨ (c ∷ γ) ⊨ φ ⟩
pin-out c φ γ = PT.rec (snd ((c ∷ γ) ⊨ φ))
  (λ { (z , (ez , h)) → subst (λ v → ⟨ (v ∷ γ) ⊨ φ ⟩) (Σ≡Prop (λ v → snd (isL v)) ez) h })

固定した終域への符号化された単射の論理式

InjCode F a b は四つの命題値の条件からなります。F の一価性、その定義域が a であること、グラフの単射性、そして値が b に含まれることです。論理式の充足は命題値であり、最後の条件は所属命題を値とする依存関数なので、それらの入れ子の積も命題になります。

isPropInjCode : (F a b : S) → isProp (InjCode F a b)
isPropInjCode F a b =
  isProp× (snd ((F ∷ a ∷ []) ⊨ svAt zero))
    (isProp× (snd ((F ∷ a ∷ []) ⊨ domAt zero (suc zero)))
      (isProp× (snd ((F ∷ a ∷ []) ⊨ injAt zero))

残る値域条件は、引数、値、およびグラフが両者を関係づける証明を順に量化します。その結論は値が b に属するという命題です。したがって依存関数を繰り返しても命題性が保たれ、InjCode が命題であることの証明が完成します。

        (isPropΠ3 (λ _ y _ → snd (fst y ∈ fst b)))))

InjCode がグラフ引数と定義域引数について参照するのは、それらが表示する基礎の集合だけです。構成可能性の証明は命題なので、等式 fst F ≡ fst F' と fst a ≡ fst a' は S での等式へ一意に持ち上がります。続いて二変数の置換により、目標 b を固定したまま、単射の符号を (F , a) から (F' , a') へ移送します。

injcode-resp : (F F' a a' b : S) → fst F ≡ fst F' → fst a ≡ fst a'
             → InjCode F a b → InjCode F' a' b
injcode-resp F F' a a' b qF qa = subst2 {x = F} {y = F'} {z = a} {w = a'}
  (λ E A → InjCode E A b)
  (Σ≡Prop (λ v → snd (isL v)) qF) (Σ≡Prop (λ v → snd (isL v)) qa)

論理式 injFo b f B は、位置 f のグラフと位置 B の定義域を使って、単射の符号の四条件を表します。グラフは一価で、定義域がちょうど指定された集合であり、単射的です。さらに、グラフが引数を値に関係づけるなら、その値は固定された目標 b に属します。最後の節が表すのは値域の包含であり、b への全射性ではありません。

injFo : ∀ {n} → S → Fin n → Fin n → Formula S n
injFo b f B = svAt f ∧̇ domAt f B ∧̇ injAt f
            ∧̇ ∀̇ (∀̇ (appAt (suc (suc f)) i1 i0 ⇒̇ (var i0 ∈̇ con b)))

injFo の読み出し則を示すため、目標 b、関係する二つの位置 f と B、および割当て γ を固定します。局所名 F と A は、それぞれの位置にある台の要素を表します。これにより、後の議論では変数参照の処理を数学的な主張から切り離し、結論を直接 InjCode F A b と述べられます。

module InjFo {n : ℕ} (b : S) (f B : Fin n) (γ : S ^ n) where
  private
    F A : S
    F = lookup f γ
    A = lookup B γ

読み取りの補題は、単射論理式の充足を単射符号の四つの条件へ変換します。定義域の条件では、入力に対するグラフの証人を命題的切り詰めから「その入力が A に属する」という命題へ除去します。逆に、A への所属から必要な定義域の証人が得られます。

  read : ⟨ γ ⊨ injFo b f B ⟩ → InjCode F A b
  read (sv , dm , ij , ran) =
      svAt-in zero (F ∷ A ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
    , domAt-intro zero (suc zero) (F ∷ A ∷ []) (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))

一価性と単射性については、それぞれの意味論的な条件を γ で読み取り、二項環境 (F,A) に対する対応する条件を組み立て直します。値域の条件では、適用の妥当性によって F のグラフ所属を論理式が要求する適用原子へ変換し、最後の条項から値が固定された目標 b に属することを得ます。

                   (λ { (y , p) → domAt-out f B γ dm x y p }) h)
        , (λ hx → domAt-in f B γ dm x hx))
    , injAt-in zero (F ∷ A ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ))) p)

埋めの補題は逆向きの構成です。符号化された単射の四つのデータから、単射の論理式の充足を作ります。今度は、論理式が述べられている構造のもとですべてのアトムを読みます。

  fill : InjCode F A b → ⟨ γ ⊨ injFo b f B ⟩
  fill (sv , dm , ij , ran) =
      svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ A ∷ []) sv x y y' p q)
    , domAt-intro f B γ (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))

全域性については、切り詰められたグラフの証人を「入力が A に属する」という命題にだけ除去し、逆向きには A への所属から証人を与えます。残りの条項は γ で一価性と単射性を組み立て直し、適用の妥当性によって値域の仮定を論理式の最後の条項へ変換します。したがって read と fill は、論理式の充足と単射符号の四条件の間の両方向を与えます。

                   (λ { (y , p) → domAt-out zero (suc zero) (F ∷ A ∷ []) dm x y p }) h)
        , (λ hx → domAt-in zero (suc zero) (F ∷ A ∷ []) dm x hx))
    , injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ A ∷ []) ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ)) p)

無限段階の計数を L_ω に帰着する

無限順序数 ω における段階は、構成可能な集合として提示されます。順序数の段階 Lset ω とその順序数性が、段階の提示によってまとめられます。

Lω : S
Lω = LsetS ω ω-ord

この節の目標は、型として述べられます。Lset ω の構成可能な提示から内部の ω への、符号化された内部単射です。これが、より大きな段階の数え上げが依拠する基底の場合です。

LimitStageCounted : Type (ℓ-suc ℓ)
LimitStageCounted = InjL Lω ωʟ

移送の補題は、始域と目標の底の集合の等しさに沿って、内部の符号化された単射を移します。始域の等しさから新しい始域 a' を古い始域 a へ含め、与えられた単射を適用した後、目標の等しさから古い目標 b を新しい目標 b' へ含めます。この三つの単射の合成によって InjL a' b' が得られます。

move : (a a' b b' : S) → fst a ≡ fst a' → fst b ≡ fst b' → InjL a b → InjL a' b'
move a a' b b' qa qb h =
  injl-trans a' a b' (inclusion-coded a' a (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym qa) hz))
    (injl-trans a b b' h (inclusion-coded b b' (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) qb hz)))

基底の計数：L_ω を ω へ単射する

排除の議論は、Lset (# n) の形の有限段階を扱い、そのような有限段階の名簿を取ることから始まります。すなわちその要素の、索引づけられた列挙です。

private
  module FinNo (n : ℕ) where
    t : Tally (finiteStage n)
    t = StageOrder.tally (stageOrder n)

名簿は、その大きさ、各索引での要素、そしてすべての要素がある索引に現れるという覆いの事実を供給します。

    open Tally t using ( size; item; onto )

探索の補題は要素に名前を与えます。有限段階の各要素 x に対して、有限の索引の上で判定可能な探索を走らせ、排中律で各項目を x と比較し、その項目が x に等しい索引を返します。探索が返すのはある索引であって、それが一意だとは主張しません。これは有限の族の上の有限の判定であり、選択の原理への訴えではありません。

    named : (x : V ℓ) → ⟨ x ∈ˢ finiteStage n ⟩ → Σ[ i ∈ Fin size ] (item i ≡ x)
    named x hx = decRec (λ q → q) (λ nq → Empty.rec (PT.rec Empty.isProp⊥ nq (onto x hx)))
      (DecΣ size (λ i → item i ≡ x)
        (λ i → Sum.rec yes no (lem ((item i ≡ x) , setIsSet (item i) x))))

f が ω の提示を有限段階へ単射すると仮定します。各値 f x には名簿のインデックス q x を割り当てられ、そのインデックスを二つ並べた写像 x ↦ (q x,q x) が有限性による排除定理の入力になります。この対が等しければ対応する f の値が等しくなり、さらに f の単射性から元の入力が等しくなります。

    noinj : (f : ⟪ ω ⟫ → ⟪ Lset (# n) ⟫)
          → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
    noinj f finj = finite-excl-ω (# size) (numeral-ord size) (#∈ω size)
      (λ x → q x , q x) (λ x y e → finj x y (qq x y (cong fst e)))
      where

補助の写像は、f のそれぞれの値を周囲の要素として読み、それが有限の段階に属することを証明し、先ほど見つかった有限の索引で名前を与えます。

      vl : ⟪ ω ⟫ → V ℓ
      vl x = ⟪ Lset (# n) ⟫↪ (f x)
      mm : (x : ⟪ ω ⟫) → ⟨ vl x ∈ˢ finiteStage n ⟩
      mm x = member (Lset (# n)) (f x)
      q : ⟪ ω ⟫ → ⟪ # size ⟫

写像 q は、選ばれた名簿のインデックスを有限順序数の提示 ⟪# size⟫ の対応する要素へ変換します。その二つの名前が等しければ、この提示の単射性によって自然数インデックスが等しくなり、二つの名簿項目も等しくなります。最後に Lset (# n) の提示が、この周囲での等しさを f の二つの値の等しさへ戻します。

      q x = fromFin size (toℕ (named (vl x) (mm x) .fst) , toℕ<n (named (vl x) (mm x) .fst))
      qq : (x y : ⟪ ω ⟫) → q x ≡ q y → f x ≡ f y
      qq x y e = ↪-inj {a = Lset (# n)}
        (sym (named (vl x) (mm x) .snd)
          ∙ cong item (inj-toℕ (cong fst (fromFin-inj size _ _ e)))

同一視の連鎖は、二つ目の点の名指しされた項目で閉じます。名前が等しければ値が等しい、という証明がこれで完成します。

          ∙ named (vl y) (mm y) .snd)

任意の添字 w に対して、NoInto w は ω の提示から Lset w の提示への周囲の水準での単射が存在しないという命題です。次の補題では、w が ω に属するという追加の仮定のもとで、この命題を証明します。

  NoInto : V ℓ → Type ℓ
  NoInto w = (f : ⟪ ω ⟫ → ⟪ Lset w ⟫)
           → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥

一般の形は、g の ω への所属に沿って有限の場合を運ぶことで得られます。ω の要素は、単に、ある数項であり、この輸送が排除の主張全体をその数項の段階へ移します。目標が矛盾の命題であるため、消去は正当です。

  no-inj-fin : (g : V ℓ) → ⟨ g ∈ˢ ω ⟩ → NoInto g
  no-inj-fin g g∈ω = PT.rec (isPropΠ2 (λ _ _ → Empty.isProp⊥))
    (λ { (k , e) → subst NoInto e (FinNo.noinj (lower k)) }) g∈ω

無限順序数 ω は構成可能です。その順序数性が、順序数の段階の構成を供給します。

hω : ⟨ isL ω ⟩
hω = isL-ord ω ω-ord

Lset ω の段階の順序は、L の内部の、符号化された対からなる構成可能な集合 Rω として実装されます。

Rω : SL.S
Rω = relL ω hω ω-ord

関係の仕様は、Rω の符号化された対が、段階の順序で関係づけられた L の要素の順序対にちょうど一致することを言います。

specω : IsRel ω Rω
specω = relL-spec ω hω ω-ord

端点条件は、関係する各対の両端点について段階への所属を復元します。符号化された対を展開すると Lset ω の二つの要素が得られ、成分の等式がそれらの底の集合を端点 y と x にそれぞれ同一視します。

Rsub : (y x : SL.S) → Holds Rω y x
     → ⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩
Rsub y x h = PT.rec isP
  (λ { (_ , h₁) → PT.rec isP
    (λ { (a , h₂) → PT.rec isP

二つの所属は、順序対の符号化の単射性が供給する、二つの成分の等式に沿って運ばれます。

      (λ { (b , (q , _)) →
             subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .fst)) (a .snd)
           , subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .snd)) (b .snd) })
      h₂ })
    h₁ })

二つの所属の連言は命題であり、符号化された対の関係は、構成可能な順序対のもとの関係の仕様から産み出されます。

  rel
  where
  isP : isProp (⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩)
  isP = isProp× (snd (fst y ∈ˢ Lset ω)) (snd (fst x ∈ˢ Lset ω))
  rel : ⟨ Related ω (pr (fst y) (fst x)) ⟩

関係は、符号化された対を、二つの底の集合の素の順序対と同一視する輸送に沿って運ばれます。

  rel = subst (λ w → ⟨ Related ω w ⟩) (prʟ-fst y x)
    (specω (prʟ y x) .fst
      (subst (λ w → ⟨ w ∈ˢ fst Rω ⟩) (sym (prʟ-fst y x)) h))

順序型の仕組みは、内部の関係とその端点の条件とともに、段階 Lset ω のもとで具体化されます。これにより、小さな定義域・内部の関係・そして前章の崩壊の構成が固定されます。

module OT = Code Lω Rω Rsub using ( module Conjuncts; Dom; _≺_; isProp≺; ≺-in; ≺-out )

ホストの整列順序は、Lset ω の提示に運ばれた段階の順序であり、抽象的な整列順序の仕組みを小さな索引型の上で使えます。

Wω : SWO ⟪ Lset ω ⟫
Wω = carry (Lset ω) (orderAt ω ω-ord)

この整列順序が Lset ω の提示上に与える狭義の比較を a <ω b と書きます。次の二つの補題は、この関係と内部で符号化された先行関係 a OT.≺ b が同じ比較を表すことを示します。

open SWO Wω using () renaming ( _<∙_ to _<ω_ )

内部関係と周囲の段階順序は、共通の提示の上で一致します。最初の向きでは、符号化された関係の表現定理を使い、内部の先行関係の証明 a OT.≺ b を周囲の順序比較 a <ω b として読み取ります。

≺→< : (a b : OT.Dom) → a OT.≺ b → a <ω b
≺→< a b k = ixRel-rep ω ω-ord Rω specω a b (OT.≺-out a b k)

逆に、符号化された関係の充足定理は、周囲の順序比較 a <ω b を内部の先行関係の証明 a OT.≺ b へ変換します。この二方向の変換により、周囲の関係がもつ順序論的性質を内部関係へ移せます。

<→≺ : (a b : OT.Dom) → a <ω b → a OT.≺ b
<→≺ a b k = OT.≺-in a b (ixRel-fill ω ω-ord Rω specω a b k)

内部の関係の整礎性は、ホストの順序の整礎性から従います。到達可能性は点ごとに運ばれます。内部の関係のそれぞれの先行者は、まずホストの先行者に変換されるのです。

wfω : WellFounded OT._≺_
wfω m = go (SWO.wf∙ Wω m)
  where
  go : {n : OT.Dom} → Acc _<ω_ n → Acc OT._≺_ n
  go {n} (acc r) = acc (λ n' k → go (r n' (≺→< n' n k)))

内部の関係の推移性も、ホストの順序を通して運ばれます。連なる二つの内部の一歩が変換され、合成され、そして元に戻されます。

transω : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
transω {a} {b} {c} k k' =
  <→≺ a c (SWO.trans∙ Wω a b c (≺→< a b k) (≺→< b c k'))

任意の a と b に対して、周囲の整列順序の三岐性は a <ω b、等しい、または b <ω a のいずれかを与えます。結論を入れ子の直和で表すことで、各比較を内部関係の対応する場合へ変換できます。

triω : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
triω a b = go (SWO.tri∙ Wω a b)
  where
  go : TriW (a <ω b) (a ≡ b) (b <ω a)
     → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))

ホストのそれぞれの場合が、対応する内部の場合、すなわち小さい・等しい・大きいへ変換されます。

  go (lt h) = inl (<→≺ a b h)
  go (eq e) = inr (inl e)
  go (gt h) = inr (inr (<→≺ b a h))

整礎性と推移性から、崩壊値とその順序数像 otL が得られます。三岐性により異なる点の崩壊値が異なることが分かるので、崩壊グラフ colTable は単射性の条件を満たし、後で使う符号を与えます。

module C = OT.Conjuncts wfω transω using ( module Inj; col; col-ord; col-out; colTable; otL; otL-out )
module I = C.Inj triω using ( code; col-inj )

誕生段階の族は、内部の ω のもとで具体化されます。Lset ω の提示されたすべての要素は ω の中に誕生段階をもち、族の関係がそれを順序づけます。

private
  module F = Family ω (λ δ _ → orderAt δ) ω-ord using ( _≺_; bornAt )

族の関係の展開された読みが証明されます。ω のもとでは、抽象的に述べられた順序は、誕生段階とその次の一歩からなる具体的な順序と等しくなります。

  unfoldω : (a b : MemOf (Lset ω))
          → relOf (orderAt ω ω-ord) a b ≡ F._≺_ a b
  unfoldω a b = cong (λ z → relOf (z ω-ord) a b) (orderAt-step ω)

要素の誕生段階は、周囲の集合として読まれます。

  bAt : MemOf (Lset ω) → V ℓ
  bAt a = F.bornAt a .fst

すべての誕生段階は内部の ω に属します。族の全体が ω より下にあるからです。

  bAt∈ω : (a : MemOf (Lset ω)) → ⟨ bAt a ∈ˢ ω ⟩
  bAt∈ω a = F.bornAt a .snd

すべての誕生段階は順序数です。順序数 ω の要素であり、順序数の要素は順序数だからです。

  bAt-ord : (a : MemOf (Lset ω)) → IsOrd (bAt a)
  bAt-ord a = mem-ord {A = ω} ω-ord (bAt a) (bAt∈ω a)

Lset ω の提示されたすべての要素は、その自身の誕生段階を一つ上げた段階に属します。要素の構成可能性が、その後続の段階の中へ運ばれるのです。

  self-at : (a : MemOf (Lset ω)) → ⟨ a .fst ∈ˢ Lset (sucV (bAt a)) ⟩
  self-at a = birth-mem (a .fst) (Lset→isL ω ω-ord (a .fst) (a .snd))

ステップの上界は次を言います。族の順序で a が b に先行するなら、a の底の集合は、b の誕生段階に一つを加えたものが添字づける段階に属します。誕生段階が真に早い場合には、後続の比較が順序数の線形性によって判定されます。

  step-bound : (a b : MemOf (Lset ω)) → F._≺_ a b
             → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
  step-bound a b (inl h) =
    raise (suc∈or≡ (bAt a) (bAt b) (bAt-ord a) (bAt-ord b) h)
    where

誕生段階が真に早い分岐では、順序数の離散性によって sucV (bAt a) と bAt b を直接比較します。この後続がなお bAt b より下にある場合も、それと等しい場合も、段階の単調性によって既知の a∈Lset (sucV (bAt a)) を Lset (sucV (bAt b)) へ移します。

    raise : ⟨ sucV (bAt a) ∈ˢ bAt b ⟩ ⊎ (sucV (bAt a) ≡ bAt b)
          → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
    raise (inl k) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}
      (∈sucV-inl {A = bAt b} {x = sucV (bAt a)} k) (self-at a)
    raise (inr e) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}

等式の場合 sucV (bAt a) ≡ bAt b には、まずこの順序数を bAt b の後続に入れ、それから段階の単調性を適用します。もう一方の主な分岐では誕生段階が等しく、ステップ順序の証人そのものが a の共通の誕生段階の後続段階への所属を含みます。その等しさに沿って移送すれば、求める上界が得られます。

      (subst (λ w → ⟨ sucV (bAt a) ∈ˢ sucV w ⟩) e (self∈sucV (sucV (bAt a))))
      (self-at a)
  step-bound a b (inr (e , u)) =
    subst (λ w → ⟨ a .fst ∈ˢ Lset (sucV w) ⟩) (sym e) (u .fst)

内部の崩壊の定義域のすべての点は、Lset ω の提示された要素として読まれます。

  atIx : OT.Dom → MemOf (Lset ω)
  atIx m = ⟪ Lset ω ⟫↪ m , memOf (Lset ω) m

崩壊領域の点 p に対し、護衛となる添字 gOf p は、p が表す要素の誕生段階の後続です。有限段階 Lset (gOf p) が p のすべての先行者を含むことになります。

  gOf : OT.Dom → V ℓ
  gOf p = sucV (bAt (atIx p))

どの衛も内部の ω の中にあります。ω の要素の後続だからです。

  gOf∈ω : (p : OT.Dom) → ⟨ gOf p ∈ˢ ω ⟩
  gOf∈ω p = ω-limit (bAt (atIx p)) (bAt∈ω (atIx p))

先行者の上界は、点 p のすべての先行者 r が、p の衛とされる有限の段階の周囲の要素を提示することを言います。証明は、ステップの上界を、族の順序の展開された読みを通して運びます。

  seg-bound : (p r : OT.Dom) → r OT.≺ p
            → ⟨ ⟪ Lset ω ⟫↪ r ∈ˢ Lset (gOf p) ⟩
  seg-bound p r k =
    step-bound (atIx r) (atIx p) (transport (unfoldω (atIx r) (atIx p)) (≺→< r p k))

先行者の区間は、p の先行者 r と、その崩壊の値が与えられた集合と等しいことの同一視を記録します。

private
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))

先行者の区間は命題です。同じ崩壊の値をもつ二つの記録は、崩壊が小さな定義域の上で単射であり、関係が命題値であり、底の集合が h-集合を作ることによって、同一視されます。

  isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b)
  isPropSeg p b (r , _ , e) (r' , _ , e') =
    Σ≡Prop (λ z → isProp× (OT.isProp≺ z p) (setIsSet _ _))
      (I.col-inj r r' (e ∙ sym e'))

崩壊の値の中の所属はどれも、先行者の区間を与えます。崩壊の切り詰められた読みが、命題値の区間の中へ消去されるのです。

  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h)

残るのは、各順序数 C.col p が ω より下にあることの証明です。順序数の三分律で妨げとなるのは、ω に等しい場合と、崩壊が ω を要素として含む場合です。どちらからも同じ包含 ω ⊆ C.col p が従うので、まずこの包含が有限段階 Lset (gOf p) へのありえない単射を導くことを示します。

col-fin : (p : OT.Dom) → ⟨ C.col p ∈ˢ ω ⟩
col-fin p = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
  where
  refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
  refute sub = no-inj-fin (gOf p) (gOf∈ω p) f f-inj