L の内部で順序型を構成する

L で符号化された関係の要素を小さな型で表示すれば、整礎関係を崩壊できます。さらに推移性があれば、個々の崩壊値は順序数となり、したがって L の要素になります。本章はそれらの値を正確な値域 otL に集め、グラフ colTable を別に集めますが、otL の順序数性を定理としてまとめてはいません。三分法を追加して初めて、このグラフは元の領域からその値域への符号化された単射になります。

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

古典的仮定を明示するのは、後の存在証明で、候補となる点が現在扱う点に先行するかどうかを判定する必要があるからです。整礎再帰そのものはこの判定を必要としません。排中律が使われるのは、関係が成り立つ場合と成り立たない場合に分けて一つの置換関数を定める箇所です。

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

宇宙レベル ℓ と、構成可能な台に必要なレベルでの排中律の実例を固定します。このモジュール以後の構成はすべて、この一つの古典的パラメータを受け継ぎます。排中律が公理として隠されているわけではありません。

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

崩壊は集合論の一階言語の論理式によって特徴づけられます。順序対の所属と等号が原子的な判定を与え、連言、選言、含意、否定、および非有界量化子が表の条件を表します。「すべての先行者について」のような制限は、関係の原子論理式を含意の前件に置いて表し、有界量化子の構成子は使いません。

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

構成の全体を通して、二つの表示を対応させる必要があります。整礎再帰を使うために D の要素は小さな表示を通して扱い、グラフの項目は累積階層の中で順序対として符号化された集合のまま扱います。表示と順序対符号化の単射性により、後の証明でこれらの表示から元の要素と二つの座標へ戻れます。

open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )

証明では、再帰的に定めた値を、L の内部で充足できる論理式へ結び付ける必要があります。整礎再帰が崩壊を作り、再帰グラフがその値と順序対を集合へ集め、符号化の論理式がそれらの対を適用として解釈します。最後に段階についての定理が、各順序数である崩壊値を L の中に置きます。

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; appC; appC-adequate; prʟ; prʟ-fst; svAt; domAt )

集められたグラフには、二段階の目標があります。まず崩壊を D 上の全域的な一価関係として表さなければなりません。その後、三分法のもとで初めて、内部単射に必要な入力の一意性も満たせます。順序対の論理式がグラフを表し、単射の四条件はそれぞれ証明された後に初めて単射符号へまとめられます。

open import L.Coding.Expressions {ℓ} using ( module PairExpression )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap ) renaming ( module Inj to DefinableInj )
open import L.Mostowski {ℓ} using ( module Mostowski )

後の一意性証明では、構成可能な集合をその要素によって繰り返し比較します。外延性は所属の点ごとの同値を基礎集合の等しさに変え、命題値の証拠によって、対として作られた構成可能な対象の等しさは証明の取り方に依存しません。そのため、切り詰められた場合分けから恒久的な選択を取り出さずに、等しさを結論できます。

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ; isPropΣ; isSetΣSndProp )
open import Cubical.Functions.Logic using ( ⇔toPath )

累積階層は、周囲の集合と、その各集合の要素の小さな表示を同時に与えます。したがって 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 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

構成可能構造の台を S と書きます。構造の所属 _∈ˢ_ は L の要素間の所属を表し、後で周囲の階層にある集合の表示を読むために使う小さな所属 _∈ₛ_ とは異なります。

open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )

論理式は L が担う構造で解釈します。記法 S ^ n は n 個の構成可能集合からなる環境を表し、γ ⊨ φ は、制限された構成可能構造の内部で環境 γ が論理式 φ を満たすことを表します。

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

基礎となる階層の台 V ℓ は h-集合であり、構成可能性の証拠は命題値です。したがって、依存対からなる台 S も h-集合であり、構成可能な集合の間の等式は命題になります。このため、後の切り詰められた場合分けを台の要素の等式へ除去できます。

isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))

符号化されたグラフは、底の集合の上で読まれます。底の要素の順序対が F の底の集合に属するとき、F は x と y について成立すると書きます。以下のすべての節が、この形を読みます。

Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩

構成可能集合 D と、順序対を符号化する構成可能集合 R を固定します。仮定 Rsub が述べるのは、R に実際に現れる各順序対の二つの端点が D に属することだけです。崩壊を作る段階で整礎性と推移性を加え、さらに後で単射性を証明するときに三分法を加えます。この章では関係の外延性を仮定しません。

module Collapse (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

D への所属は、台の上の一項の述語として述べられます。

  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst D ⟩

この述語は命題です。提示された集合の底の集合への所属だからです。この命題性は後で重要になります。ある構成が所属の証明に依存しても、それで選択のデータを運ぶことはないのです。

  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst D)

D の要素は、小さな型、すなわち提示の添字型によって提示されます。

  Dom : Type ℓ
  Dom = ⟪ fst D ⟫

提示は、その索引を周囲の階層の中へ埋め込みます。

  ↪ : Dom → V ℓ
  ↪ = ⟪ fst D ⟫↪

索引は構成可能な集合へ戻されます。埋め込まれた要素には、D への所属に沿って、構成可能性の推移性によって運ばれた構成可能性の証明が対にされます。

  up : Dom → S
  up m = ↪ m , isL-trans {x = fst D} {y = ↪ m} (member (fst D) m) (snd D)

作り直された構成可能な集合は D の要素です。これは、提示自身の所属の記録によるものです。

  up-mem : (m : Dom) → Mem (up m)
  up-mem m = member (fst D) m

この表示には重複する添字がありません。埋め込まれた二つの要素が等しければ、その添字も等しくなります。後で既知の要素 up b から添字を復元するとき、復元された添字を b 自身と同一視できるため、集めたグラフが期待する対 (↪ b, col b) を含むことが分かります。崩壊関数の単射性は別の結果であり、三分法を必要とします。

  Dom≡ : {a b : Dom} → ↪ a ≡ ↪ b → a ≡ b
  Dom≡ {a} {b} e = ↪-inj {a = fst D} {m = a} {n = b} e

逆に、D の要素とその所属の証明からは、提示のその要素における繊維を取ることで、提示の索引が復元されます。

  toDom : (x : S) → Mem x → Dom
  toDom x mx = fst (fiber (fst D) mx)

復元された索引は、与えられた要素をちょうど提示します。繊維が、埋め込まれた索引とその要素の同一視を運ぶからです。

  toDom-val : (x : S) (mx : Mem x) → ↪ (toDom x mx) ≡ fst x
  toDom-val x mx = snd (fiber (fst D) mx)

符号 R は小さな表示の上に関係を誘導します。a ≺ b とは、表示された要素 ↪ a と ↪ b の順序対が R に属することです。整礎再帰はこの関係に沿って進みます。続く二つの補題が、この関係を構成可能集合上の Holds R (up a) (up b) と両方向に結び付けます。

  opaque
    _≺_ : Dom → Dom → Type ℓ
    a ≺ b = ⟨ pr (↪ a) (↪ b) ∈ₛ fst R ⟩

添字 a と b を固定すると、関係の型 a ≺ b は階層内の集合への所属を述べる命題です。したがって、この関係が記録するのは辺の有無だけであり、特定の証明が担う追加のデータではありません。この命題性だけでは辺の有無を判定できず、その判定が実際に必要となる後の箇所で初めて排中律を使います。

    isProp≺ : (a b : Dom) → isProp (a ≺ b)
    isProp≺ a b = snd (pr (↪ a) (↪ b) ∈ₛ fst R)

符号化された関係の中の所属は、小さな関係を与えます。L の中に記録された順序対が、二つの所属の関係をつなぐ橋によって認められるのです。

    ≺-in : (a b : Dom) → Holds R (up a) (up b) → a ≺ b
    ≺-in a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .fst

逆に、小さな関係は R の本当の対を記録するので、関係の二つの読みは両方向で一致します。

    ≺-out : (a b : Dom) → a ≺ b → Holds R (up a) (up b)
    ≺-out a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .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) → (⟨ fst w ∈ fst v ⟩ → Src F R x w)
                          × (Src F R x w → ⟨ fst w ∈ fst v ⟩)

表が実際に含む各順序対について、その入力で完全性が成り立ち、出力が先行者の値だけからなるとき、その表を正しいといいます。この条件は領域を指定しないので、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 を適用すると命題的に切り詰められた候補値が得られます。PT.map は切り詰めを保ったまま、appAt の妥当性を表すパスによって、そのグラフ原子を Holds F y u へ変えます。

  complete-out : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ completeAt f R x ⟩
               → Complete (lookup f γ) R (lookup x γ)
  complete-out f R x γ h y p = PT.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 を与え、PT.map がそれに伴う Holds F y u を、存在結論が要求する適用原子の充足へ戻します。

  complete-in : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
              → Complete (lookup f γ) R (lookup x γ)
              → ⟨ γ ⊨ completeAt f R x ⟩
  complete-in f R x γ h y p = PT.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) (γ : S ^ n)
          → ⟨ γ ⊨ srcAt f R x w ⟩
          → Src (lookup f γ) R (lookup x γ) (lookup w γ)
  src-out f R x w γ = PT.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) (γ : S ^ n)
         → Src (lookup f γ) R (lookup x γ) (lookup w γ)
         → ⟨ γ ⊨ srcAt f R x w ⟩
  src-in f R x w γ = PT.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) (γ : 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) (γ : 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) (γ : 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) (γ : 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 
    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 = PT.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) を認識します。これにより、局所的な崩壊の論理式を、以下で構成する再帰の値関係として使えます。

open import L.Recursion.Graph {ℓ} lem public using ( module PairFo )

一意性、存在、崩壊表

内部の構成は、符号化された定義域 D と関係 R から始まります。最初の付帯条件は、R に属する各順序対の両成分が D に属することだけです。整礎性と推移性はこのモジュールの境界では仮定されず、崩壊の議論を始めるときに別々に与えられます。

module Internal (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) 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 → snd (isL v)) (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 → Empty.⊥
    ≺-irrefl = W.induction {P = λ a → a ≺ a → Empty.⊥} (λ 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 → fst v ≡ col a
    correct-val F hc = W.induction {P = λ a → (v : S) → Holds F (up a) v → fst v ≡ col a} go
      where
      go : (a : Dom) → ((b : Dom) → b ≺ a → (v : S) → Holds F (up b) v → fst v ≡ col b)

証明は、各点の同値に帰着します。w が記録された値に属することと、w が崩壊に属することは同値です。正しさの仮定から、up a での完備さと、値の条項という二つの補助の事実が取り出されます。

         → (v : S) → Holds F (up a) v → fst v ≡ col a
      go a IH v hv = extensionalV {a = fst v} {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 ∈ fst v ⟩ → ⟨ w ∈ col a ⟩
        fwd w w∈ = PT.rec (snd (w ∈ col a)) read (val wS .fst w∈)
          where
          wS : S
          wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)

出所の項目は、必要な二つの事実に変換されます。載せられた先行者と入力の間の関係と、載せられた先行者での表の項目です。先行者は、その内部の添字に復号されます。

          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) ∈ fst R ⟩) (sym (toDom-val y my)) ry)
            e : w ≡ col b

この等式は、復号された先行者に帰納の仮定を適用したものです。表の、載せられた先行者での値は、その内部の添字の崩壊に等しく、輸送によって w に等しくなります。

            e = IH b b≺a wS (subst (λ t → ⟨ pr t w ∈ fst F ⟩) (sym (toDom-val y my)) fy)

逆向きの包含では w ∈ col a とします。崩壊の除去則から、ある先行者 r ≺ a について col r ≡ w であることが、命題的切り詰めのもとで得られます。目標 w ∈ fst v は命題なので、その切り詰めの内側で議論できます。また w は構成可能な集合 col a の要素なので、構成可能性の証拠と組にして wS とできます。

        bwd : (w : V ℓ) → ⟨ w ∈ col a ⟩ → ⟨ w ∈ fst v ⟩
        bwd w w∈ = PT.rec (snd (w ∈ fst v)) 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 ∈ fst v ⟩
          read (r , (ra , e)) = PT.rec (snd (w ∈ fst v)) inner (cmp (up r) (≺-out r a ra))
            where
            inner : Σ[ u ∈ S ] Holds F (up r) u → ⟨ w ∈ fst v ⟩
            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 ∈ fst F ⟩) (IH r ra u fu ∙ e) fu) ∣₁

ここで q が実際に D の要素であり、v が q で局所的な崩壊の論理式を満たすとします。論理式から得られるのは、(q,v) を含む正しい表が単に存在することだけですが、求める集合の等式は命題なので切り詰めを除去できます。項目を q から復号された表示へ輸送すると、correct-val によって fst v は col (toDom q mq) と同定されます。

    colFo-val : (q : S) (mq : Mem q) (v : S) → ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩
              → fst v ≡ col (toDom q mq)
    colFo-val q mq v h = PT.rec (setIsSet (fst v) (col (toDom q mq)))
      (λ { (F , (hc , hv)) → correct-val F hc (toDom q mq) v
             (subst (λ t → ⟨ pr t (fst v) ∈ fst F ⟩) (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 ] ((fst z ≡ pr (fst q) (fst v)) × ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩) ∥₁)
        ⊎ ((Holds R q (up a) → Empty.⊥) × (fst z ≡ fst ea))

対象言語の中で先行者の場合と既定の場合を分けるには、変化する入力 q と固定された点 a からなる順序対を関係検査に使う必要があります。対の式は、局所的な論理式の二つの自由な枠において、この項を一様に与えます。

      module PE = PairExpression

式 image は順序対 (q,up a) を表します。第一成分は入力の枠から取り、第二成分は a を表す台の要素をリテラルとして置きます。したがって image が R に属することは、ちょうど q が a の R-先行者であることを述べ、局所表の項目を記述するものではありません。

      image : PE.Expr 
      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 
        ψ = (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 = PT.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)) = PT.rec (snd ((z ∷ q ∷ []) ⊨ ψ))
          (λ { (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) ∈ fst R ⟩) (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 (lem (pr (fst q) (↪ a) ∈ fst R)))
          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 : Holds R q (up a) ⊎ (Holds R q (up a) → Empty.⊥)
                 → ∥ Σ[ z ∈ S ] (⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
                                × ((z' : S) → ⟨ (z' ∷ q ∷ []) ⊨ ψ ⟩ → z' ≡ z)) ∥₁

q R a と仮定します。帰納仮定は col b が q で colFo を満たすことを与え、prʟ-fst は fst zb と順序対の符号 pr (fst q) (col b) の間に必要な等式を与えるので、正準な出力 zb は左の分岐を満たします。一意性を示すため、任意の充足する出力を同じ二つの場合に分けて読みます。左の分岐の証人は colFo-val によって決まり、右の分岐の証人は仮定 q R a と矛盾します。

          decide (inl 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' → PT.rec (isSetS z' zb)
                  (λ { (inl (_ , hv)) → PT.rec (isSetS z' zb)
                         (λ { (v , (e , hcol)) → Σ≡Prop (λ w → snd (isL w))

左の分岐にある別の証人について、colFo-val はその第二成分を col b と同定します。これを順序対の等式と合成すると、出力全体が zb に等しいことが従います。右の分岐にある別の証人は q R a の反証を含むので存在できません。これで先行者の場合の一意性が完了します。最後の行からは、既定の出力 ea を選ぶ、先行者でない場合が別に始まり、その一意性証明は次のコードブロックへ続きます。

                                (e ∙ cong (pr (fst q)) (colFo-val q mq v hcol) ∙ sym (prʟ-fst q (colʟ b))) })
                         hv
                     ; (inr (nh , _)) → Empty.rec (nh h) })
                  (ψ-out z' q hz') ) ∣₁
          decide (inr nh) = ∣ ea

所属を否定する場合が一意性の議論を閉じます。既定の項目 ea は ψ を満たします。別の証人を外向きに読むと、nh と矛盾する肯定的な所属が得られるか、既定の分岐から fst z' ≡ fst ea が得られます。後者では、構成可能性の証明が命題であることにより、基礎集合のこの等式が S で必要な等式 z' ≡ ea へ持ち上がります。

            , ( ψ-in ea q (inr (nh , refl))
              , λ z' hz' → PT.rec (isSetS z' ea)
                  (λ { (inl (h , _)) → Empty.rec (nh h)
                     ; (inr (_ , e)) → Σ≡Prop (λ w → snd (isL w)) 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 ∈ fst Fa ⟩) (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 × (fst y ≡ pr (↪ b) (col b))) ∥₁
      Fa-out y hy = PT.rec squash₁
        (λ { (q , (mq , hψ)) → PT.rec squash₁
          (λ { (inl (h , hv)) → PT.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 からは、fst x ≡ ↪ b かつ fst v ≡ col b を満たすある b ≤ a が単に得られます。

      Fa-pair : (x v : S) → Holds Fa x v
              → ∥ Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v)) ∥₁
      Fa-pair x v h = PT.map step
        (Fa-out (prʟ x v) (subst (λ w → ⟨ w ∈ fst Fa ⟩) (sym (prʟ-fst x v)) h))
        where

輸送は等式を内部の対に向け直し、補助が順序対の単射性を通してそれを、添字の名指しの等式と崩壊の値の名指しの等式に分けます。

        step : Σ[ b ∈ Dom ] (Below b × (fst (prʟ x v) ≡ pr (↪ b) (col b)))
             → Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
        step (b , (k , e)) = b , (k , sym (fst q) , sym (snd q))
          where
          q : (fst x ≡ ↪ b) × (fst v ≡ col b)

合成した順序対の等式に pr-inj を適用すると、fst x ≡ ↪ b と fst v ≡ 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 = PT.rec
        (isProp× (isPropΠ (λ _ → isPropΠ (λ _ → squash₁)))
                 (isPropΠ (λ w → isProp× (isPropΠ (λ _ → squash₁))
                                          (isPropΠ (λ _ → snd (fst w ∈ fst v))))))

選んだ項がある 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 ≡ fst x) × (col b ≡ fst v))
              → Complete Fa R x × ValueIs Fa R x v
        build (b , (k , ex , ev)) = cmp , (λ w → fwd w , bwd w)

ここで中心となる変換は、符号化された先行者 y R x を Dom 上の狭義比較へ移すことです。項目の表示が同一視するのは fst x と表示された要素 ↪ 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 ≡ fst y))
          pred y hy = c , (≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩)
                              (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 ≡ fst y に沿って輸送すると、入力 y で必要な項になります。b ≤ a を介する推移性により、c は a より真に下にあります。

          cmp : Complete Fa R x
          cmp y hy = ∣ colʟ c , subst (λ t → ⟨ pr t (col c) ∈ fst Fa ⟩) 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 を fst w ∈ col b と書き換えます。崩壊の外向き補題から単に得られる r ≺ b と col r ≡ fst w により、up r から x への R-辺と、up r を w に対応させる表の項が構成できます。

          fwd : (w : S) → ⟨ fst w ∈ fst v ⟩ → Src Fa R x w
          fwd w w∈ = PT.map read (col-out b (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) (sym ev) w∈))
            where
            read : Σ[ r ∈ Dom ] ((r ≺ b) × (col r ≡ fst w)) → Σ[ y ∈ S ] (Holds R y x × Holds Fa y w)
            read (r , (rb , er)) = up r

二つの所属は添字の等式と狭義の比較に沿って輸送され、関係と表の所属の両方が名指された先行者のところに置かれます。

              , ( subst (λ t → ⟨ pr (↪ r) t ∈ fst R ⟩) ex (≺-out r b rb)
                , subst (λ t → ⟨ pr (↪ r) t ∈ fst Fa ⟩) er (Fa-in r (inl (below-trans rb k))) )

逆方向では、Src Fa R x w の証人から、y R x を満たし、表で y から w への項をもつような y が単に得られます。目標 fst w ∈ fst v は命題なので、出所の証人と表の読み出しに含まれる命題的切り詰めを順にそこへ除去できます。

          bwd : (w : S) → Src Fa R x w → ⟨ fst w ∈ fst v ⟩
          bwd w = PT.rec (snd (fst w ∈ fst v)) (λ { (y , (hy , fy)) →
            PT.rec (snd (fst w ∈ fst v)) (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 ≡ fst y) × (col c ≡ fst w))
                 → ⟨ fst w ∈ fst v ⟩
            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 ∈ fst R ⟩) (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 → snd ((w ∷ q ∷ []) ⊨ CF.colFo))
                (sym (Σ≡Prop (λ w → snd (isL w)) (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 ∈ fst otL が得られます。

    otL-in : (b : Dom) → ⟨ col b ∈ fst otL ⟩
    otL-in b = OT.table-in (up b) (colʟ b) (up-mem b) (approx b)

逆に、各 y ∈ fst otL について、col b ≡ y を満たす添字 b : Dom が単に存在します。結論には意図的に命題的切り詰めが残されているため、各要素の原像を選ぶことなく正確な値域を記述しています。

    otL-out : (y : V ℓ) → ⟨ y ∈ fst otL ⟩ → ∥ Σ[ b ∈ Dom ] (col b ≡ y) ∥₁
    otL-out y hy = PT.map (λ { (q , (mq , h)) → toDom q mq , sym (colFo-val q mq yS h) })
      (OT.table-out yS hy)
      where
      yS : S

置換の読み出しを適用するには、周囲の集合 y を構成可能な領域の要素として扱う必要があります。y ∈ fst otL と otL の構成可能性から、構成可能性の下方閉性がこの組を与えます。

      yS = y , isL-trans {x = fst otL} {y = y} hy (snd otL)

再帰グラフの構成を 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) ∈ fst colTable ⟩
    colTable-in b = subst (λ t → ⟨ pr (↪ b) t ∈ fst colTable ⟩)
      (cong col (Dom≡ (toDom-val (up b) (up-mem b)))) (CT.F-in (up b) (up-mem b))

逆に colTable-out は、グラフの任意の要素 y について、ある b : Dom に対する fst y ≡ pr(↪ b,col b) が単に成り立つと述べます。その添字は命題的切り詰めの中にあるため、この外向きの読みはグラフを特徴づけますが、各要素を表示する添字を選びません。

    colTable-out : (y : S) → ⟨ y ∈ˢ colTable ⟩
                 → ∥ Σ[ b ∈ Dom ] (fst y ≡ pr (↪ b) (col b)) ∥₁
    colTable-out y hy = PT.map (λ { (q , mq , e) → toDom q mq
      , e ∙ cong (λ t → pr t (col (toDom q mq))) (sym (toDom-val q mq)) }) (CT.F-out (fst y) hy)

ファイバーの述語は、x と対にされる要素 v が x の提示する添字の崩壊の値であることを述べ、提示の所属をデータとして伴います。

    Fib : S → S → Type (ℓ-suc ℓ)
    Fib x v = Σ[ mx ∈ Mem x ] (fst v ≡ col (toDom x mx))

x と v を固定すると、Fib x v は命題です。所属 mx : Mem x は命題値であり、各 mx に対する等式 fst v ≡ col (toDom x mx) も、V が集合であるため命題です。したがって、この依存和は追加の選択データをもちません。

    isPropFib : (x v : S) → isProp (Fib x v)
    isPropFib x v = isPropΣ (isPropMem x) (λ mx → setIsSet (fst v) (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
                  → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) 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 が置かれます。したがって、一価性と正確な定義域の論理式は、これらの固定位置によってグラフとその意図された定義域を参照できます。

    γ : S ^ 
    γ = colTable ∷ D ∷ []

第一の条件は一価性です。colTable が同じ入力に対して値 y と y' をもつ二つの順序対を含むなら、fst y ≡ fst y' が成り立ちます。これは再帰値の一意性から従うものであり、各入力が値をもつこと自体は主張しません。

    sv : ⟨ γ ⊨ svAt zero ⟩
    sv = CT.sv

定義域条件は同値です。ある入力が colTable で何らかの値をもつことと、その入力が D に属することとは同値です。したがって、この条件は D の外の項を排除すると同時に、D の各要素上での全域性も述べます。後者の方向での値の存在は命題的に切り詰められたままです。

    dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
    dm = CT.dm

値域条件はグラフの対の読み出しから従います。x から y への項は、x が定義域に属する証拠を与え、fst y を対応する崩壊値と同一視します。その崩壊値は otL-in によって otL に属します。ここで示したのはグラフの値が otL に入ることだけであり、colTable の単射性には次に導入する三分法の仮定がなお必要です。

    ran : (x y : S) → Holds colTable x y → ⟨ fst y ∈ fst otL ⟩
    ran x y h = subst (λ t → ⟨ t ∈ fst otL ⟩) (sym (snd (colTable-pair x y h)))
      (otL-in (toDom x (fst (colTable-pair x y h))))

崩壊表はすでに 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)       = Empty.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)) = Empty.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 ≡ fst x を満たす添字 b : Dom を選ばなければなりません。これは崩壊の原像であり、関係のある固定した点の先行者であるとは限りません。第二の引数 bound は、表示された元の入力 ↪ b が Y に属することを証明します。逆向きのインターフェースを使うたびにこれらのデータを別途与える必要があり、otL-out だけから自動的に得られるものではありません。

      module Inverse (X Y : S)
        (pre : (x : S) → ⟨ fst x ∈ fst X ⟩ → Σ[ b ∈ Dom ] (col b ≡ fst x))
        (bound : (x : S) (mx : ⟨ fst x ∈ fst X ⟩) → ⟨ ↪ (pre x mx .fst) ∈ fst Y ⟩) where