小さな集合を定義可能な最小の証人について閉じても、無限基数による上界は保たれるはずです。この章では、始集合が無限基数へ単射するなら、その Skolem 包も同じ基数へ単射することを L の内部で示します。

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

排中律は、和集合の要素が左側に属するかどうかなどの局所的な判定を与えます。古典的推論は一つの明示的な仮定として入り、得られる上界はその仮定を正確に記録します。

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

宇宙レベル ℓ と、レベル ℓ-suc ℓ の命題に対する排中律を固定します。内部集合、符号化されたグラフ、切り詰められた証人は、すべてこの固定した仮定のもとで構成されます。

module L.GCH.HullCounting {ℓ : 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 ( 𝒮ᵥ )

議論では順序数段階とその構成可能な要素との間を行き来します。推移性により要素も L にとどまり、順序数の所属と段階の累積性により、各対象を定義可能な選択に十分大きい段階へ入れられます。

open import V.Coding {ℓ} using ( pr; pr-inj; #-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( Lset-cumul; ord∈Lset-suc )

数え上げに用いる写像は、それ自身が L の集合でなければなりません。分出で部分グラフを作り、対と和集合で符号を構成し、妥当性によって適用、一価性、定義域の内部論理式を集合論的な意味と結びつけます。

open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; unionʟ )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; svAt-out; domAt-in )

内部の単射は、定義域が正確で、一価かつ単射的であり、値域に上界をもつ構成可能なグラフによって証されます。InjCode は具体的なグラフを保ち、InjL はその存在命題だけを保ちます。

open import L.Coding.Expressions {ℓ} using ( numL; tagAtL; tagAtL-adequate )
open import L.Coding.CodeConstructibility {ℓ}
  using ( sglʟ; sglʟ-in; sglʟ-out; cupʟ; cupʟ-inl; cupʟ-inr; cupʟ-out )
open import L.Coding.Injection {ℓ} lem using ( injAt-out; module Extract )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )

数え上げの証明では内部の単射を合成します。定義可能な写像は一意な値をもつ論理式を構成可能なグラフにし、最小証人の選択は Skolem 閉包にそのような写像を与え、内部の積はタグ付きの対を収めます。

open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.LeastWitnessMap {ℓ} lem using ( module Least )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; prodL-in; module Relation )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )

最小の証人は一つの共通する構成可能段階の中で選びます。有界順序数がパラメータをそこへ集め、強化された十分な段階であることが充足関係を安定させ、充足グラフが選択を L の集合として記録します。

open import L.Stage {ℓ} lem using ( LeastOrd; isPropLeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Ordinal using ( boundingOrd )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )

Skolem 包は、始集合から最小証人による閉包を反復して得られます。その構成可能な提示が選択に必要な段階の上界を与え、凝縮が包を対応する構成可能構造と同一視します。

open import L.GCH.SkolemHull {ℓ} lem using ( module Frame; module HullStage )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module Condense′; module Telescope )
open import L.GCH.StageCountingTools {ℓ} lem
  using ( isPropInjCode; injcode-resp; injFo; module InjFo; pinAt; pin-in; pin-out; seq-map; Lω
        ; limit-stage-counted )

各閉包段階は論理式の符号と有限なパラメータ列で添字づけられます。論理式の形は可算であり、無限基数上の有限列は平方則で抑えられ、整礎帰納法が数え上げに現れる内部基数についてその平方則を与えます。

open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seq-count )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prod-inj; ω⊆; Goal; module Step )
open import L.Cardinal {ℓ} lem using ( IsCardinalL )
open import V.Hierarchy {ℓ} using ( regularityV )
import Cubical.Induction.WellFounded as WF

グラフの二つの引数がそれぞれ等しさで同一視されるとき、二項の移送によってグラフへの所属証明を両方の同一視に沿って一度に移せます。したがって等しさによる置換は符号化された関係と両立します。

open import Cubical.Foundations.Prelude using ( subst2 )

タグ 0 と 1 は異なるので、タグ付き単射の二つの分岐は交わりません。命題値のファイバーをもつ依存対の等しさは第一成分の等しさに帰着するため、構成可能性の証明は数え上げに影響しません。

open import Cubical.Data.Nat.Properties using ( znots; snotz )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isSetΣSndProp )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

von Neumann 数項をタグに用い、ω がそれらを集め、後続が有限な進み方を表します。空集合は単元集合からの単射の値となり、命題的切り詰めは代表を選ばずに存在を記録します。

open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

符号化された単射の存在は命題的に切り詰められます。数え上げに必要なのは証人となるグラフの存在だけだからです。したがって除去は命題に対してのみ行い、結果がグラフの選び方に依存しないようにします。

open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

周囲の集合について、x ∈ˢ y は x が y に属するという命題です。符号化された関数の定義域と値域の条件は、最終的に底集合上のこの関係へ帰着します。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

構成可能モデルの台を S と書きます。その要素は周囲の集合と、それが L に属することの証明との対です。この証明は命題なので、底集合が構成可能な要素を等しさまで一意に定めます。

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

構成可能な定数をもつ論理式は L の内部で評価でき、周囲の階層へも射影できます。推移性により二つの読み方は一致するので、内部で証明したグラフの主張を底集合間の通常の所属として使えます。

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

Holds F x y は、x と y の底集合の順序対が底のグラフ F に属することを意味します。これは、議論に現れる各符号化された適用論理式が表す周囲の関係です。

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

要素 nn k : S は、周囲の von Neumann 数項 # k とその構成可能性の証明との対です。とくに nn 0 と nn 1 は、L の外へ出ることなく内部のタグとして働きます。

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

S の二つの要素の底集合が等しければ、要素そのものも等しくなります。第二成分は構成可能性の証明だけなので、証明無関係性によって第一成分の等しさを依存対の等しさへ持ち上げられます。

S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
S≡ = Σ≡Prop (λ v → snd (isL v))

台 S は h-集合です。第一成分が属する累積階層は h-集合であり、構成可能性の証明からなる各ファイバーは命題なので、S のすべての等式型は命題になります。

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

最初の二つの変数の枠の De Bruijn 索引に名前が付けられます。この章の符号化された論理式は、一度に多くとも八つの枠しか扱わないからです。

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

i2、i3、i4 は、それぞれ変数位置 2、3、4 を表します。各添字は直前の添字の後続であり、多相的な末尾の長さ k によって、さらに変数が利用できる場合にもその位置が有効に保たれます。

  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))

i4 の定義式を与えた後、同じ後続のパターンで位置 5 と 6 を定めます。これらの名前により、入れ子になった束縛子が生む位置のずれを符号化された論理式の型で確認できます。

  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

順序数はその自身の段階に含まれます。順序数の各要素はそれ自身順序数であり、累積的な構成が、順序数のすべての要素をその順序数が索引づける段階の中に置きます。

ord⊆Lset : (α : V ℓ) → IsOrd α → (z : V ℓ) → ⟨ z ∈ α ⟩ → ⟨ z ∈ Lset α ⟩
ord⊆Lset α oα z z∈α =
  Lset-cumul z α oz oα z∈α (ord∈Lset-suc z oz)
  where
  oz : IsOrd z

z ∈ α であり α が順序数なので、z 自身も順序数です。これにより z はその後続段階に属し、さらに z ∈ α に沿って累積性を用いると z ∈ Lset α が得られます。

  oz = mem-ord {A = α} oα z z∈α

構成可能集合 D₁ と D₂ を固定します。それらの内部の二項和集合は二つの単射をまとめる共通の定義域であり、その所属原理から二つの包含と切り詰められた場合分けが得られます。

module Union2 (D₁ D₂ : S) where

この和は、二つの集合の内部の和です。

  D : S
  D = cupʟ D₁ D₂

左側の要素は、和の左の規則によって含められます。

  in₁ : (z : S) → ⟨ fst z ∈ fst D₁ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₁ z = cupʟ-inl D₁ D₂ (fst z)

右側の要素は対称的に含められます。

  in₂ : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₂ z = cupʟ-inr D₁ D₂ (fst z)

z ∈ D₁ ∪ D₂ なら、z が左側または右側に属することだけが得られます。この選言は命題的に切り詰められています。所属は、ある提示添字が z を名指すことを保ちますが、具体的な添字は保たないからです。

  out : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ ⟨ fst z ∈ fst D₁ ⟩ ⊎ ⟨ fst z ∈ fst D₂ ⟩ ∥₁
  out z = cupʟ-out D₁ D₂ (fst z)

κ をタグ 0 と 1 を含む構成可能集合とし、E₁ と E₂ がそれぞれ D₁ と D₂ から κ への単射を符号化するとします。値にタグを付けると、D₁ ∪ D₂ から κ × κ への一つの単射にまとめられます。この構成では κ が順序数である必要はありません。

module TagUnion (κ : S) (0∈κ : ⟨ #  ∈ fst κ ⟩) (1∈κ : ⟨ #  ∈ fst κ ⟩)
                (D₁ D₂ E₁ E₂ : S) (c₁ : InjCode E₁ D₁ κ) (c₂ : InjCode E₂ D₂ κ) where

D = D₁ ∪ D₂ と書きます。どちらか一方の集合の要素は D に属し、D の各要素からは、二つの集合のいずれかに由来するという切り詰められた証明が得られます。

  open Union2 D₁ D₂ public using ( D; in₁; in₂; out )

それぞれの符号化された単射は、その底にある関数と、グラフが符号化の言う通りにちょうど成立する証明を抽出します。

  module X₁ = Extract E₁ D₁ (fst c₁) (fst (snd c₁)) using ( toFun; toFun-graph )
  module X₂ = Extract E₂ D₂ (fst c₂) (fst (snd c₂)) using ( toFun; toFun-graph )

Mem z は z が和集合の定義域 D に属するという命題です。入力にこの証明を添えることで、場合分けされた関数を評価するために必要な定義域の証拠がちょうど得られます。

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

左の定義域への所属は排中律で判定でき、この判定こそ、タグ付きの単射を作るための場合分けです。

  Case : S → Type (ℓ-suc ℓ)
  Case z = ⟨ fst z ∈ fst D₁ ⟩ ⊎ (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)

排中律は、和のすべての要素が左の定義域から来たかどうかを判定します。

  decide : (z : S) → Case z
  decide z = lem (fst z ∈ fst D₁)

左の定義域に属さない要素は、右の定義域に属します。和の中の所属は二つの側に分かれ、左側は仮定された失敗と矛盾します。

  off : (z : S) → Mem z → (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
  off z m no = PT.rec (snd (fst z ∈ fst D₂))
    (λ { (inl h) → Empty.rec (no h) ; (inr h) → h }) (out z m)

それぞれの側の値はタグ付きの像です。数項のタグ 0 か 1 を、抽出された関数の値と対にします。こうして二つの単射は、重ならないタグ付きの値域に着地します。

  val : (z : S) → Mem z → Case z → S
  val z m (inl h)  = prʟ (nn ) (X₁.toFun (z , h))
  val z m (inr no) = prʟ (nn ) (X₂.toFun (z , off z m no))

z ∈ D に対し、関数 fn は z ∈ D₁ かどうかを判定します。左の場合は (0,E₁(z)) を返し、補集合にあたる右の場合は (1,E₂(z)) を返します。

  fn : (z : S) → Mem z → S
  fn z m = val z m (decide z)

周囲での意味 Wit y z には二つの分岐があります。左の分岐では z ∈ D₁ であり、(z,v) ∈ E₁ を満たす v が単に存在して、y の底集合が (0,v) に等しくなります。

  Wit : (y z : S) → Type (ℓ-suc ℓ)
  Wit y z =
      (⟨ fst z ∈ fst D₁ ⟩
        × ∥ Σ[ v ∈ S ] (Holds E₁ z v × (fst y ≡ pr (# ) (fst v))) ∥₁)
    ⊎ ((⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)

右の分岐では z ∉ D₁ であり、(z,v) ∈ E₂ を満たす v が単に存在して、底集合について y = (1,v) となります。異なるタグにより、別々の分岐から得た出力が等しくなることはありません。

        × ∥ Σ[ v ∈ S ] (Holds E₂ z v × (fst y ≡ pr (# ) (fst v))) ∥₁)

グラフは二つの枠をもつ論理式として書かれます。D₁ への所属と最初の符号の上の存在量化の連言、あるいはその所属の否定と第二の符号の上の存在量化の連言です。存在量化子の内側では、単射された値とタグの等式が符号化のアトムです。

  opaque
    fo : Formula S 
    fo = ((var i1 ∈̇ con D₁) ∧̇ ∃̇ (appC E₁ i2 i0 ∧̇ tagAtL i1  i0))
       ∨̇ ((¬̇ (var i1 ∈̇ con D₁)) ∧̇ ∃̇ (appC E₂ i2 i0 ∧̇ tagAtL i1  i0))

二つの符号化のアトムを読むには、その妥当性の補題を使います。適用のアトムの充足は所属 Holds E z v になり、タグのアトムの充足は、y とタグ付きの対との等式になります。

    private
      rd : (E : S) (k : ℕ) (y z v : S)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ → ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
         → Holds E z v × (fst y ≡ pr (# k) (fst v))
      rd E k y z v ha ht =

二つの妥当性の同値に沿って移送すると、充足の証人は Wit が要求する成分、すなわちグラフ所属 Holds E z v と、y をタグ k の付いた対と同一視する等しさになります。

          subst ⟨_⟩ (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ [])) ha
        , subst ⟨_⟩ (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ [])) ht

逆に、Holds E z v と底集合についての等しさ y = (k,v) から、妥当性に沿って逆向きに移送すると適用の原子式の充足が得られます。

      wr : (E : S) (k : ℕ) (y z v : S)
         → Holds E z v → fst y ≡ pr (# k) (fst v)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ × ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
      wr E k y z v ha ht =
          subst ⟨_⟩ (sym (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ []))) ha

同じ逆向きの移送により、タグ付き対の等しさはタグ原子式の充足になります。二つの証明を合わせると、存在量化子のもとにある連言が再構成されます。

        , subst ⟨_⟩ (sym (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ []))) ht

fo の充足証明は二つの選言肢に分けて読みます。左からは z ∈ D₁ と 0 のタグが付いた切り詰められた E₁ の証人が得られ、右からは z ∉ D₁ と 1 のタグが付いた対応する E₂ の証人が得られます。各切り詰めの内側で rd を適用すると、Wit y z の切り詰められた要素が得られます。

    fo-out : (y z : S) → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩ → ∥ Wit y z ∥₁
    fo-out y z = PT.map
      (λ { (inl (h , hv)) → inl (h , PT.map (λ { (v , (ha , ht)) → v , rd E₁  y z v ha ht }) hv)
         ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
             , PT.map (λ { (v , (ha , ht)) → v , rd E₂  y z v ha ht }) hv) })

グラフの内向きの読み出しは、ホスト側の証人を場合ごとに充足へ変えます。左の場合は、所属と切り詰められた項目を、適用とタグの符号化の妥当性の等式に沿って運び、右の場合は、所属しないことの反駁を対象言語の否定へ持ち上げてから同じことをします。

    fo-in : (y z : S) → Wit y z → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩
    fo-in y z (inl (h , hv)) =
      ∣ inl (h , PT.map (λ { (v , (ha , ht)) → v , wr E₁  y z v ha ht }) hv) ∣₁
    fo-in y z (inr (h , hv)) =
      ∣ inr ((λ z∈ → lift (h z∈))

右の場合の残りが第二の選言肢を完成させます。E₂ の項目は、タグを 0 から 1 に替えるだけで左と同じように運ばれます。二つの選言肢は切り詰められた存在へ注入され、導入は終わりです。

          , PT.map (λ { (v , (ha , ht)) → v , wr E₂  y z v ha ht }) hv) ∣₁

符号化されたそれぞれの関係は一価です。第一成分を共有する項目は第二成分も共有します。これが注入の符号の最初の連言項で、適用の符号化の妥当性を通して読み出されます。

  private
    sv₁ : (x y y' : S) → Holds E₁ x y → Holds E₁ x y' → fst y ≡ fst y'
    sv₁ = svAt-out zero (E₁ ∷ D₁ ∷ []) (fst c₁)
    sv₂ : (x y y' : S) → Holds E₂ x y → Holds E₂ x y' → fst y ≡ fst y'
    sv₂ = svAt-out zero (E₂ ∷ D₂ ∷ []) (fst c₂)

符号化された関係はさらに単射でもあります。第二成分を共有する項目は、第一成分の基礎の集合が等しくなります。範囲の条項はここからはじまり、関係のどの値も基数の中にあると述べます。

    ij₁ : (y x x' : S) → Holds E₁ x y → Holds E₁ x' y → fst x ≡ fst x'
    ij₁ = injAt-out zero (E₁ ∷ D₁ ∷ []) (fst (snd (snd c₁)))
    ij₂ : (y x x' : S) → Holds E₂ x y → Holds E₂ x' y → fst x ≡ fst x'
    ij₂ = injAt-out zero (E₂ ∷ D₂ ∷ []) (fst (snd (snd c₂)))
    ran₁ : (x y : S) → Holds E₁ x y → ⟨ fst y ∈ fst κ ⟩

二つ目の値域条件により、二つの単射符号から読み出すデータがそろいます。各関係について一価性、単射性、そしてすべての値が κ に属することが得られ、タグ付き写像はこれらの性質から構成されます。

    ran₁ = snd (snd (snd c₁))
    ran₂ : (x y : S) → Holds E₂ x y → ⟨ fst y ∈ fst κ ⟩
    ran₂ = snd (snd (snd c₂))

証人は要素についての二つの場合から構成します。z ∈ D₁ なら E₁ から取り出した関数の値を使い、そうでなければ、そこから得られる z ∈ D₂ に対して E₂ から取り出した関数の値を使います。どちらの場合も、取り出しによりグラフの項目と、タグ付きの対を選んだ値と同一視する等式の両方が得られます。

  wit : (z : S) (m : Mem z) (c : Case z) → Wit (val z m c) z
  wit z m (inl h)  = inl (h , ∣ X₁.toFun (z , h)
    , (X₁.toFun-graph (z , h) , prʟ-fst (nn ) (X₁.toFun (z , h))) ∣₁)
  wit z m (inr no) = inr (no , ∣ X₂.toFun (z , off z m no)
    , (X₂.toFun-graph (z , off z m no) , prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∣₁)

左の場合の一意性は、三つの等式を合成します。項目の第二成分が、切り詰められた証人が名指す値に等しいこと。E₁ の一価性が二つの関数の値を同一視すること。そして対の第一射影の等式が、値がちょうどタグつきの項目であることを述べます。

  only : (z : S) (m : Mem z) (c : Case z) (y : S) → Wit y z → fst y ≡ fst (val z m c)
  only z m (inl h) y (inl (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# )) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
          ∙ sym (prʟ-fst (nn ) (X₁.toFun (z , h))) }) hv

交差する場合はそのまま反駁されます。D₁ の中の要素が、D₁ の外で記録された証人をもつことはできず、逆もまた然りです。右と右の場合は、E₂ とタグ 1、そして外れた要素での関数の値を使って、左とまったく同じように処理されます。

  only z m (inl h) y (inr (no , _)) = Empty.rec (no h)
  only z m (inr no) y (inl (h , _)) = Empty.rec (no h)
  only z m (inr no) y (inr (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# )) (sv₂ z v (X₂.toFun (z , off z m no)) hg (X₂.toFun-graph (z , off z m no)))

最後の等式が、タグの同定と対の第一射影の等式を合成し、一意性が完成します。こうして、どちらの場合でも証人はその値を決定します。

          ∙ sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) }) hv

値は内部の直積に落ちます。数項 0 か 1 と関数の値の対は、その第一射影の等式を通して提示され、二つの数項が κ の中にあり、範囲の条項によって関数の値も κ の中にあるので、prodL-in がそれを受け入れます。

  into : (z : S) (m : Mem z) (c : Case z) → ⟨ fst (val z m c) ∈ˢ fst (prodL κ) ⟩
  into z m (inl h) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn ) (X₁.toFun (z , h))))
    (prodL-in κ (nn ) (X₁.toFun (z , h)) 0∈κ (ran₁ z (X₁.toFun (z , h)) (X₁.toFun-graph (z , h))))
  into z m (inr no) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))))
    (prodL-in κ (nn ) (X₂.toFun (z , off z m no)) 1∈κ

右の場合は E₂ と数項 1 から範囲の事実を供給し、タグつきの値がどちらも直積の中にあることが揃います。

      (ran₂ z (X₂.toFun (z , off z m no)) (X₂.toFun-graph (z , off z m no))))

これらの材料から、通常の和集合 D から内部直積 prodL κ への写像を定めます。値は左側を優先する場合分けで選ばれ、into がそのタグ付きの値が直積に属することを証明します。

  Dmap : DefinableMap
  Dmap = record
    { dom = D ; cod = prodL κ ; fn = fn
    ; into = λ z m → into z m (decide z)
    ; graph = fo

定義の条項が証人をグラフの導入に渡し、一意性が、どのグラフの項目も、決められた場合の値へ、台の等しさに沿って変換します。これで定義可能な写像は完成です。

    ; defines = λ z m → fo-in (fn z m) z (wit z m (decide z))
    ; only = λ z m y h → S≡ (PT.rec (setIsSet _ _) (only z m (decide z) y) (fo-out y z h)) }

タグつきの写像の単射性は、二つの入力について決められた場合を比較することで証明します。場合分けには四つの組み合わせがあり、タグつきの対の構造がそれをきれいに分けます。

  inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z') → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
  inj z m z' m' = go (decide z) (decide z')
    where
    go : (c : Case z) (c' : Case z') → fst (val z m c) ≡ fst (val z' m' c') → fst z ≡ fst z'
    go (inl h) (inl h') q = ij₁ (X₁.toFun (z , h)) z z' (X₁.toFun-graph (z , h))

同じタグの場合は、対の等式を pr-inj で逆にたどります。タグが一致するので、値の等式が二つの関数の値を同一視し、これが単射性の条項が消費する議論そのものです。

      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₁ ⟩) (sym (snd p)) (X₁.toFun-graph (z' , h')))
      where
      p : (#  ≡ # ) × (fst (X₁.toFun (z , h)) ≡ fst (X₁.toFun (z' , h')))
      p = pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₁.toFun (z' , h')))
    go (inl h) (inr no') q = Empty.rec (znots (#-inj   (fst

タグが異なる二つの場合はいずれも不可能です。二つの値が等しければ数項 0 と数項 1 が等しくなってしまい、二つの向きはそれぞれ znots と snotz に反します。両方の入力が右側の場合は、E₂ の単射性がそれらを同一視します。

      (pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' no')))))))
    go (inr no) (inl h') q = Empty.rec (snotz (#-inj   (fst
      (pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∙ q ∙ prʟ-fst (nn ) (X₁.toFun (z' , h')))))))
    go (inr no) (inr no') q = ij₂ (X₂.toFun (z , off z m no)) z z' (X₂.toFun-graph (z , off z m no))
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₂ ⟩) (sym (snd p)) (X₂.toFun-graph (z' , off z' m' no')))

右と右の場合の対の等式は、タグの一致と関数の値の一致に分かれ、単射性が消費するのは後者です。

      where
      p : (#  ≡ # ) × (fst (X₂.toFun (z , off z m no)) ≡ fst (X₂.toFun (z' , off z' m' no')))
      p = pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∙ q
                  ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' no')))

得られたグラフは、通常の和集合 D₁ ∪ D₂ から prodL κ への符号化された単射です。写像は値のタグで二つの枝を区別し、両方に属する要素は第一の枝で扱います。

  injL : InjL D (prodL κ)
  injL = Inj.injL Dmap inj

二つの前提は、それぞれの単射グラフを命題的切り詰めのもとでしか与えません。二つの切り詰めを命題 InjL (D₁ ∪ D₂) (prodL κ) へ消去すると、どの証人グラフの組にもタグ付き構成を適用でき、必要な符号化単射の単なる存在が得られます。

tag-union : (κ : S) → ⟨ #  ∈ fst κ ⟩ → ⟨ #  ∈ fst κ ⟩
          → (D₁ D₂ : S) → InjL D₁ κ → InjL D₂ κ
          → InjL (unionʟ (pairʟ D₁ D₂)) (prodL κ)
tag-union κ h0 h1 D₁ D₂ = PT.rec2 squash₁
  (λ { (E₁ , c₁) (E₂ , c₂) → TagUnion.injL κ h0 h1 D₁ D₂ E₁ E₂ c₁ c₂ })

最小の前者の構成は、一般的な形で述べられます。順序数 γ、関係 G、定義域 D、そして段階 γ で抑えられた前者の集合 P を受け取り、D のすべての要素が P の中に G の前者を「単に」もつとします。課題は、その一つを正準に選ぶことです。

module LeastPre (γ : V ℓ) (oγ : IsOrd γ) (G D P : S)
  (inP : (p z : S) → Holds G p z → ⟨ fst p ∈ fst P ⟩)
  (P⊆L : (p : S) → ⟨ fst p ∈ fst P ⟩ → ⟨ fst p ∈ Lset γ ⟩)
  (have : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁) where

定義域への所属は型として記録され、議論が要素とともにそれを運べるようにします。

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

グラフの論理式は、定数 G の適用の条項です。対の上で成立することは、ちょうどその対が関係に属することを意味します。

  private
    graphFo : Formula S 
    graphFo = appC G i0 i1

存在仮定を共通の段階へ移しますが、前者を大域的に選ぶことはしません。切り詰めのもとで存在する各前者は P に属し、したがって Lset γ に属します。さらに妥当性の等式が、その関係への所属をグラフ論理式の充足へ変えます。

    have-γ : (z : S) → Mem z
           → ∥ Σ[ p ∈ S ] (⟨ fst p ∈ Lset γ ⟩ × ⟨ (p ∷ z ∷ []) ⊨ graphFo ⟩) ∥₁
    have-γ z m = PT.map
      (λ { (p , h) → p , P⊆L p (inP p z h)
                       , subst ⟨_⟩ (sym (appC-adequate G i0 i1 (p ∷ z ∷ []))) h })

もとの切り詰められた存在が、輸送が消費する証人を供給します。

      (have z m)

段階順序による構成は、定義域の各要素に対して Lset γ にある最小の G 前者を選びます。また、定義可能なグラフと、各入力をその選ばれた値に対応させる所属の読み出しも与えます。

    module Ls = Least γ oγ D graphFo have-γ using ( fn; fn-holds; Dmap; T; T-in; T-out )

選ばれた最小の前者が、この構成の値を与える関数です。

  fn : (z : S) → Mem z → S
  fn = Ls.fn

値はその入力で関係を満たします。内部の充足は、値と入力を対にした環境での適用の条項へと運び戻されます。

  fn-holds : (z : S) (m : Mem z) → Holds G (fn z m) z
  fn-holds z m = subst ⟨_⟩ (appC-adequate G i0 i1 (fn z m ∷ z ∷ [])) (Ls.fn-holds z m)

定義可能な写像は、余域を P として記録されます。値の所属は、既存の仮定の内向きの方向が保証します。

  Dmap : DefinableMap
  Dmap = record Ls.Dmap { cod = P ; into = λ z m → inP (fn z m) z (fn-holds z m) }

最小の前者の関数のグラフは L の要素であり、段階の機構がその所属の記述とともに返します。

  T : S
  T = Ls.T

内向きの読み出しは、入力と選ばれた値の対がグラフの項目であることを示します。

  T-in : (z : S) (m : Mem z) → ⟨ pr (fst z) (fst (fn z m)) ∈ fst T ⟩
  T-in = Ls.T-in

外向きの読み出しは、すべての項目から、入力と、第二成分を選ばれた値と同一視する等式を復元します。のちの議論が候補を比較するときに使うのはこれです。

  T-out : (z e : S) → ⟨ pr (fst z) (fst e) ∈ fst T ⟩
        → Σ[ m ∈ Mem z ] (fst e ≡ fst (fn z m))
  T-out = Ls.T-out

関係が関数的であるという追加の仮定のもとで、最小の前者の関数は単射になります。モジュールが携えるのは、この一つの仮定だけです。

  module Functional
    (funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z') where

二つの入力が同じ値を共有すれば、その値は両方の入力で関係を満たします。二つ目の充足が値の等式に沿って輸送され、関数性が二つの入力を同一視します。

    inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z')
        → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
    inj z m z' m' q = funct (fn z m) z z' (fn-holds z m)
      (subst (λ w → ⟨ pr w (fst z') ∈ fst G ⟩) (sym q) (fn-holds z' m'))

この単射性は、定義域から前者の集合への、符号化された単射としてまとめられます。

    injL : InjL D P
    injL = Inj.injL Dmap inj

点の構成は、高々一要素の定義域を扱います。0 ∈ κ だけを仮定し、a から作った単集合の各要素を零番の数項へ送り、κ への符号化された単射を得ます。

module Point (κ : S) (0∈κ : ⟨ #  ∈ fst κ ⟩) (a : S) where

Y を a から作られる構成可能な単集合とします。議論で使うのは、その所属の導入則と除去則だけです。

  Y : S
  Y = sglʟ a

要素 a はそれ自身の単集合に属します。一元集合の構成の導入の読み出しによるものです。

  Y-in : ⟨ fst a ∈ fst Y ⟩
  Y-in = sglʟ-in a (fst a) refl

消去の読み出しは、単集合がそれ以外を含まないと言います。どの要素も、基礎の集合は a です。

  Y-out : (z : S) → ⟨ fst z ∈ fst Y ⟩ → fst z ≡ fst a
  Y-out z = sglʟ-out a (fst z)

グラフは、二つの自由スロットをもつ原子論理式で記述されます。この論理式は値のスロットを内部の空集合と等置し、その底の集合は数項 0 です。

  fo : Formula S 
  fo = var i0 ≐ con ∅ʟ

定義可能な写像は、ただ一つの入力を零番の数項へ送ります。余域への所属は、既存の事実 0∈κ です。

  Dmap : DefinableMap
  Dmap = record
    { dom = Y ; cod = κ ; fn = λ _ _ → nn 
    ; into = λ _ _ → 0∈κ
    ; graph = fo

グラフは定義どおりに成立します。原子文が数項をそれ自身と等置するからです。一意性は、単集合の二つの要素が同じ基礎の集合を提示することから成立します。

    ; defines = λ z m → refl
    ; only = λ z m y h → S≡ h }

単射性は、二つの外向きの読み出しを合成します。どちらの入力も a と同じ基礎の集合を提示するので、台の要素として両者は等しいのです。

  inj : (z : S) (m : ⟨ fst z ∈ fst Y ⟩) (z' : S) (m' : ⟨ fst z' ∈ fst Y ⟩)
      → fst (nn ) ≡ fst (nn ) → fst z ≡ fst z'
  inj z m z' m' _ = Y-out z m ∙ sym (Y-out z' m')

単集合から基数への単射は、ほかの計数の部品と同じ形でまとめられます。

  injL : InjL Y κ
  injL = Inj.injL Dmap inj

有限な閉包の各段階を数える

計数定理では、後者に閉じた順序数 lam、Lset lam に含まれる始点集合 X、そして X が構成可能であることを固定します。初等性と超妥当性の仮定は、X から生成される Skolem 包に必要な閉包と最小証人の性質を与えます。

module Count (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆L : (x : V ℓ) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)

計数の目標は、ω の外にある内部の基数 κ と、始点からそれへの符号化された単射です。課題は、同じ基数で包全体を数えることです。

  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ) (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  (base : InjL (X , X-isL) κ) where

この包は有限反復 hullStep n の和集合として表されます。一回の閉包は Φ によって定まり、その非自明な枝は、論理式の鍵と現在の反復上の有限なパラメータ環境による最小証人を記録します。

  module Cn = Condense′ lam ordλ succλ X X⊆L ∅∈λ elem sup X-isL
    using ( hullStep; hullL; hullStep⊆Hull )
  module B = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ
    using ( A; Body
          ; LeastWitness; leastWitnessFo; leastWitness-in; leastWitness-out

最小証人に付随するデータから、自然数の長さ、現在の集合への有限な割り当て、その符号化された環境、そして論理式の鍵が Lset ω に属することが得られます。一意性は、鍵と環境を固定した後に成立します。

          ; LeastWitnessData; leastWitness-data; leastWitness-unique; witFo-leastWitness
          ; Φ; Φ-out; λ-isL; ω-num; pack )
  module SM = SatGraph B.A using ( pairs; pairs-out; valOf )

有限反復には所属の導入則と除去則があり、各反復は包全体に含まれます。さらに包全体は Lset lam に含まれます。これらの包含により、計数構成で使う各集合は固定した周囲の段階内に保たれます。

  module It = Telescope.HullIter.It lam ordλ succλ X X⊆L ∅∈λ X-isL B.pack
    using ( Num; iter; iter-in; iter-out; iterUnion-out; ω-num )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  open Cn using ( hullStep; hullL )

κ は順序数であり ω に属さないので、すべての有限数項を含みます。この結論に内部基数性は使われず、内部基数性は別に平方法則で必要になります。

  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)

無限基数の平方に関する議論から、符号化された単射 pairκ : InjL (prodL κ) κ が得られます。ここでは κ の順序数性、内部基数性、ω に属さないことの三つをすべて使います。結論は単射であり、全単射ではありません。

  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω

段階 Lω = Lset ω は、単射の合成によって κ へ入ります。極限段階の計数がまず Lω ↪ ωʟ を与え、κ の順序数性と非有限性から得られる ω ⊆ κ が ωʟ ↪ κ を与えます。

  Lω↪κ : InjL Lω κ
  Lω↪κ = injl-trans Lω ωʟ κ limit-stage-counted
    (inclusion-coded ωʟ κ (λ z hz → ω⊆ (fst κ) oκ κ∉ω z hz))

一回の閉包を数えるため、Lset lam に含まれる構成可能な集合 Z と、InjCode E Z κ を満たす実際のグラフ E を固定します。目標は、この選ばれた段階の単射から、符号化単射の単なる存在 InjL (Φ Z) κ を構成することです。

  module OneStep (Z : S) (Z⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
                 (E : S) (cE : InjCode E Z κ) where

ΦZ = Φ Z は一回の閉包です。その所属の記述には三つの枝があります。Z の既存の要素、空集合という予備の場合、または論理式の鍵と Z 上の有限なパラメータ環境によって定まる最小証人です。

    ΦZ : S
    ΦZ = B.Φ Z

新しい部分をまず分出します。D₂ は ΦZ のうち Z に属さない要素を集めます。L の内部の分出により、新しい部分も構成可能です。

    opaque
      D₂ : S
      D₂ = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .fst

その所属の仕様は、分出が計算した内容を正確に述べます。D₂ への所属とは、ΦZ への所属と Z への所属の否定を合わせたものです。

      D₂-spec : (z : S) → (fst z ∈ fst D₂)
              ≡ ((fst z ∈ fst ΦZ) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z)))
      D₂-spec z = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .snd z

導入規則は所属の反証を対象レベルへ持ち上げます。したがって ΦZ の要素と、それが Z に属さないことの証明が揃えば D₂ に入れます。

    opaque
      D₂-in : (z : S) → ⟨ fst z ∈ fst ΦZ ⟩ → (⟨ fst z ∈ fst Z ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
      D₂-in z h no = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (no z∈))

消去の規則は、仕様を通して D₂ の所属を展開し、対象レベルの反証を通常の含意へと降ろします。

      D₂-out : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst ΦZ ⟩ × (⟨ fst z ∈ fst Z ⟩ → Empty.⊥)
      D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
        where
        r : ⟨ fst z ∈ fst ΦZ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z) ⟩

展開された主張は一つの対です。ΦZ への所属と、否定された原子の充足です。

        r = subst ⟨_⟩ (D₂-spec z) h

新しい部分の内側から、空集合と等しい要素が D∅ として分出されます。

    opaque
      D∅ : S
      D∅ = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .fst

その仕様は同じ二重の型です。D₂ への所属と、空集合との等式です。

      D∅-spec : (z : S) → (fst z ∈ fst D∅)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
      D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z

D₂ の要素で空集合と等しいものは、二つのデータとともに D∅ に入ります。

    opaque
      D∅-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → fst z ≡ ∅ → ⟨ fst z ∈ fst D∅ ⟩
      D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)

その消去は、仕様をそのまま読んだものです。D₂ への所属と、空集合との等式です。

      D∅-out : (z : S) → ⟨ fst z ∈ fst D∅ ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅)
      D∅-out z h = subst ⟨_⟩ (D∅-spec z) h

残りの部分 Dw は、D₂ のうち空集合と異なる要素を集めます。

    opaque
      Dw : S
      Dw = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .fst

その仕様は前のものと鏡像で、等式の代わりに否定された等式が置かれます。

      Dw-spec : (z : S) → (fst z ∈ fst Dw)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ)))
      Dw-spec z = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .snd z

導入には、D₂ への所属と、空集合との相等の反証が要ります。

    opaque
      Dw-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → (fst z ≡ ∅ → Empty.⊥) → ⟨ fst z ∈ fst Dw ⟩
      Dw-in z h ne = subst ⟨_⟩ (sym (Dw-spec z)) (h , λ q → lift (ne q))

消去は D₂ への所属と、対象レベルから降ろされた反証を返します。

      Dw-out : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅ → Empty.⊥)
      Dw-out z h = r .fst , λ q → lower (r .snd q)
        where
        r : ⟨ fst z ∈ fst D₂ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ) ⟩

二つの和集合が後で必要となる上界を与えます。U₁ は Z と真に新しい部分 D₂ を含み、U₃ は空集合の部分 D∅ と空でない証人の部分 Dw を含みます。続く補題は、これらの和集合への必要な包含を証明します。

        r = subst ⟨_⟩ (Dw-spec z) h
    module U₁ = Union2 Z D₂ using ( D; in₁; in₂ )
    module U₃ = Union2 D∅ Dw using ( D; in₁; in₂ )

閉包の段階は第一の和集合で覆われます。ΦZ の各要素 z は Z に属するか属さないかが排中律で決まり、いずれの場合も ΦZ が構成可能なので z も構成可能です。

    ΦZ⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst ΦZ ⟩ → ⟨ z ∈ˢ fst U₁.D ⟩
    ΦZ⊆ z h = go (lem (z ∈ fst Z))
      where
      zS : S
      zS = z , isL-trans {x = fst ΦZ} {y = z} h (snd ΦZ)

二つの場合は、和集合への二つの包含によって U₁ に入ります。すでに Z に属する要素には第一の包含を使い、そうでなければ D₂-in で新しい部分への所属を示してから第二の包含を使います。

      go : ⟨ z ∈ fst Z ⟩ ⊎ (⟨ z ∈ fst Z ⟩ → Empty.⊥) → ⟨ z ∈ fst U₁.D ⟩
      go (inl hz) = U₁.in₁ zS hz
      go (inr no) = U₁.in₂ zS (D₂-in zS h no)

新しい部分は第二の和集合で覆われます。これも空集合との等式についての排中律によるものです。

    D₂⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst D₂ ⟩ → ⟨ z ∈ˢ fst U₃.D ⟩
    D₂⊆ z h = go (lem ((z ≡ ∅) , setIsSet z ∅))
      where
      zS : S
      zS = z , isL-trans {x = fst D₂} {y = z} h (snd D₂)

空集合と等しい要素は D∅ から入り、異なる要素は Dw から入ります。

      go : (z ≡ ∅) ⊎ (z ≡ ∅ → Empty.⊥) → ⟨ z ∈ fst U₃.D ⟩
      go (inl e)  = U₃.in₁ zS (D∅-in zS h e)
      go (inr ne) = U₃.in₂ zS (Dw-in zS h ne)

D∅ の各要素は ∅ に等しいですが、D∅ 自体は空であるかもしれません。数項 0 が κ に属するので、包含の符号化から L の内部で D∅ ↪ κ が得られます。

    D∅↪κ : InjL D∅ κ
    D∅↪κ = inclusion-coded D∅ κ
      (λ z hz → subst (λ w → ⟨ w ∈ fst κ ⟩)
        (sym (D∅-out (z , isL-trans {x = fst D∅} {y = z} hz (snd D∅)) hz .snd)) (num∈κ ))

第二の和集合が証人の符号化の準備をします。U₂ は、段階 ω で生まれる要素と、Z の要素の有限列をつなぎます。

    module U₂ = Union2 Lω (seqL Z) using ( D; in₁; in₂ )

PB を U₂ = Lω ∪ seqL Z の平方とします。s ∈ Lω かつ e ∈ seqL Z である実際の証人符号 (s,e) はすべて PB に属します。ただし PB は一様な上界であり、有効な証人符号でない対も含みます。

    PB : S
    PB = prodL U₂.D

最小証人の論理式を固定した基 Z に釘付けします。得られる五変数の論理式 pin₅ は、枠 (e,s,z,p,q) において、z が環境 e と鍵 s によって定まる最小証人であるとき、かつそのときに限り満たされます。最後の二つのスロットは周囲の枠が運びます。

    opaque
      pin₅ : Formula S 
      pin₅ = pinAt Z B.leastWitnessFo

内向きには、パラメータの環境 e と鍵 s による z の最小証人が、五スロットの文脈での釘付けされた論理式の充足を与えます。

      pin₅-in : (e s z p q : S) → B.LeastWitness Z e s z
              → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
      pin₅-in e s z p q h =
        pin-in Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ [])
          (B.leastWitness-in Z e s z p q h)

外向きには、釘付けされた論理式の充足が最小証人へと展開されます。釘付けをほどくのは釘付けの補題です。

      pin₅-out : (e s z p q : S) → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
               → B.LeastWitness Z e s z
      pin₅-out e s z p q h =
        B.leastWitness-out Z e s z p q
          (pin-out Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ []) h)

数える関係は命題的に切り詰められています。GW p z は、鍵 s と環境 e が存在し、p = (s,e) であり、z がそれらによって定まる最小証人であることを単に述べます。

    GW : (p z : S) → Type (ℓ-suc ℓ)
    GW p z = ∥ Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z) ∥₁

同じ関係は論理式としても書かれます。二つの存在量化子が鍵と環境を束縛し、対の原子が p を確定し、釘付けされた論理式が証人の条件を運びます。

    opaque
      se₃ : Formula S 
      se₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ pin₅))

内向きには、対の等式と最小証人が与えられれば、二つの証人を入れ、対の原子をその妥当性に沿って対象言語へ輸送します。

      se₃-in : (z p q s e : S) → fst p ≡ pr (fst s) (fst e)
             → B.LeastWitness Z e s z → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩
      se₃-in z p q s e qp h =
        ∣ s , ∣ e , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ []))) qp
                    , pin₅-in e s z p q h ) ∣₁ ∣₁

外向きには、二つの存在量化子を一度に一つずつ消費します。最初の段階で外側の量化子をはぎ、項目 s と切り詰められた残りを取っておきます。

      se₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩ → GW p z
      se₃-out z p q = PT.rec squash₁ at₁
        where
        at₂ : (s : S) → Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                   × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) → GW p z

二つ目の存在量化子を開くと、対を表す原子式の妥当性から p = (s,e) が得られ、釘付けされた論理式の外向きの読みから最小証人の条件が得られます。これらの証人を、GW を定義する命題的切り詰めの中へ戻します。

        at₂ s (e , (qp , h)) = ∣ s , e
          , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ [])) qp
            , pin₅-out e s z p q h ) ∣₁
        at₁ : Σ[ s ∈ S ] ∥ Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                      × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) ∥₁ → GW p z

GW p z は命題なので、残る外側の切り詰めをそこへ消去できます。se₃-in と se₃-out を合わせると、ホスト側の関係 GW と、それを表す対象言語の論理式の充足との間の二つの含意が得られます。

        at₁ (s , h) = PT.rec squash₁ (at₂ s) h

有界分出により、L の内部に関係 G を構成します。その項目は、p ∈ PB、z ∈ Dw、GW p z を満たす順序対 (p,z) です。したがって G は、最小証人の関係を選んだ符号の池と空でない新しい部分の間に制限します。

    private
      module WitnessGraph = Relation PB Dw ((var i1 ∈̇ con PB) ∧̇ se₃)
        (λ p z → (fst p ∈ fst PB) ⊓ (GW p z , squash₁))
        (λ p z q h → h .fst , se₃-out z p q (h .snd))
        (λ p z q h → h .fst , PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ se₃))

記述の条件の外向きの読みは、論理式そのものの外向きの読みであり、返ってくるのはまさに GW のデータです。

          (λ { (s , e , qp , hw) → se₃-in z p q s e qp hw }) (h .snd))

G は、順序対 (p,z) の集合として表された構成可能な関係です。PB の候補符号が Dw の要素について最小証人のデータを運ぶとき、G はその符号と要素を関係づけます。

    G : S
    G = WitnessGraph.rel

内向きには、PB の符号 p が、ある鍵と環境を通して z とともに最小証人を名指すなら、G に属します。

    G-in : (p z : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst z ∈ fst Dw ⟩
         → (s e : S) → fst p ≡ pr (fst s) (fst e)
         → B.LeastWitness Z e s z → Holds G p z
    G-in p z hp hz s e qp h =
      WitnessGraph.into p z hp hz (hp , ∣ s , e , qp , h ∣₁)

逆に、Holds G p z から p ∈ PB と、命題的に切り詰められた証人データ GW p z の両方が得られます。切り詰めの外で鍵と環境を選ぶわけではありません。

    G-out : (p z : S) → Holds G p z → ⟨ fst p ∈ fst PB ⟩ × GW p z
    G-out = WitnessGraph.pair-out

この関係が Dw 上で全域的なのは切り詰められた意味においてです。各 z ∈ Dw には Holds G p z を満たす p が単に存在します。z ∈ ΦZ を外向きに読むと、z が閉包に入った三つの可能な理由が現れます。

    have : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
    have z hz = PT.rec squash₁ body (B.Φ-out Z z (D₂-out z (Dw-out z hz .fst) .fst))
      where
      body : B.Body Z z → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
      body (inl h) = Empty.rec (D₂-out z (Dw-out z hz .fst) .snd h)

そのうちの二つはすでに分出によって排除されています。z は Z の古い要素でも空集合でもあり得ません。残るのは証人の場合であり、証人の論理式の外向きの補題を通して読まれます。

      body (inr (inl e)) = Empty.rec (Dw-out z hz .snd e)
      body (inr (inr hw)) = PT.rec squash₁ read (B.witFo-leastWitness z Z hw)
        where
        read : Σ[ e ∈ S ] Σ[ s ∈ S ] B.LeastWitness Z e s z
             → ∥ Σ[ p ∈ S ] Holds G p z ∥₁

証人の枝は、環境 e、鍵 s、最小証人を与えます。そのデータ補題から、自然数の長さ n、メタレベルの割り当て g : Fin n → ⟪Z⟫、e を g の符号化された環境と同一視する等式、そして s ∈ Lset ω が得られます。

        read (e , s , hw') = PT.map at (B.leastWitness-data Z e s z hw')
          where
          at : B.LeastWitnessData Z e s → Σ[ p ∈ S ] Holds G p z
          at (n , g , qe , hs) = prʟ s e
            , G-in (prʟ s e) z

符号 p は鍵と環境の内部の対です。その PB への所属は項目ごとに築かれます。鍵は Lset ω に属するため Lω から入り、環境は Z への長さ n の割り当ての環境であるため Z の有限列から入ります。そして関係がこの対を受け入れます。

                (subst (λ w → ⟨ w ∈ fst PB ⟩) (sym (prʟ-fst s e))
                  (prodL-in U₂.D s e (U₂.in₁ s hs)
                    (U₂.in₂ e (seqL-in Z n e
                      (subst (λ w → ⟨ w ∈ˢ fst (envSet Z n) ⟩) (sym qe) (envSet-in Z g))))))
                hz s e (prʟ-fst s e) hw'

証人キーに対する一意性

必要な関数性は、計数に必要な逆向きの形をしています。一つの固定した符号 p が z と z' の両方に関係するなら、z と z' の底の集合は等しくなります。同じ要素に異なる符号があることは依然として許されます。

    funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z'
    funct p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (G-out p z h .snd) (G-out p z' h' .snd)
      where
      read : Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z)

二つの関係は外向きに読まれ、それぞれ鍵、環境、対の等式、そして最小証人を返します。

           → Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
               ((fst p ≡ pr (fst s₂) (fst e₂)) × B.LeastWitness Z e₂ s₂ z')
           → fst z ≡ fst z'
      read (s , e , q , hw) (s₂ , e₂ , q₂ , hw₂) =
        B.leastWitness-unique Z e s z z' hw hw₂'

二つの読み出しは、同じ固定した p をそれぞれ (s,e) と (s₂,e₂) として表します。順序対の符号化の単射性が、二つの鍵と二つの環境を底の集合の水準で同一視し、証明無関連性がそれらを対応する S の要素の等式へ持ち上げます。

        where
        ee : (fst s₂ ≡ fst s) × (fst e₂ ≡ fst e)
        ee = pr-inj (sym q₂ ∙ q)
        hw₂' : B.LeastWitness Z e s z'
        hw₂' = subst2 (λ e' s' → B.LeastWitness Z e' s' z')

それらの同一視に沿って二つ目の最小証人の証明を輸送すると、二つの証明は同じ鍵と環境に関するものになります。そこで最小証人の一意性から fst z ≡ fst z' が得られます。

          (S≡ {x = e₂} {y = e} (snd ee)) (S≡ {x = s₂} {y = s} (fst ee)) hw₂

符号の池には誕生の段階があります。γG は PB が階層に現れる段階です。

    γG : V ℓ
    γG = stage (fst PB) (snd PB)

その段階は順序数で添字づけられており、計数の補題が要求するのはこれです。

    oγG : IsOrd γG
    oγG = stage-ord (fst PB) (snd PB)

池はその誕生の段階に含まれます。段階の推移性によるものです。γG で生まれた集合の要素は Lset γG に属します。

    PB⊆Lγ : (p : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst p ∈ Lset γG ⟩
    PB⊆Lγ p hp = layer-trans (Lset-layer γG) {x = fst PB} {y = fst p} hp (stage-mem (fst PB) (snd PB))

これらの仮定によって LeastPre を具体化します。各 z ∈ Dw には PB にある関係づけられた符号が単に存在し、固定した一つの符号はそのような z を高々一つ定めます。最小選択が各要素について一つの符号を選び、InjL Dw PB を与えます。証人符号が初めから一意だったとは主張せず、ここで数えたのは空でない新しい部分だけで、閉包一段階全体の結論ではありません。

    module LP = LeastPre γG oγG G Dw PB (λ p z h → G-out p z h .fst) PB⊆Lγ have
      using ( module Functional )

最小原像の構成は、真に新しい証人を PB へ単射します。各 z ∈ Dw には関連する符号が単に存在し、段階順序がその最小のものを選びます。選択前の符号は一意である必要はありません。単射性は、一つの固定した符号が高々一つの証人しか表さないことから従います。

    Dw↪PB : InjL Dw PB
    Dw↪PB = LP.Functional.injL funct

単射 Z ↪ κ を有限列の各成分に作用させると、seqL Z ↪ seqL κ が得られます。これを有限列の数え上げと合成して seqL Z ↪ κ を得ます。後者に必要なのは κ が無限順序数であることだけで、内部の基数である必要はありません。

    seq↪κ : InjL (seqL Z) κ
    seq↪κ = injl-trans (seqL Z) (seqL κ) κ (seq-map Z κ E cE) (seq-count κ oκ κ∉ω)

まず U₂.D = Lω ∪ seqL Z を数えます。二つの集合にタグを付けて κ × κ へ単射し、pairκ でその積を κ へ折りたたみます。PB = U₂.D × U₂.D なので、prod-inj がこの単射を PB ↪ κ × κ へ持ち上げ、pairκ をもう一度使うと PB ↪ κ が得られます。二回の折りたたみは平方則を用いるため、内部の基数性に依存します。

    PB↪κ : InjL PB κ
    PB↪κ = injl-trans PB (prodL κ) κ
      (prod-inj U₂.D κ
        (injl-trans U₂.D (prodL κ) κ (tag-union κ (num∈κ ) (num∈κ ) Lω (seqL Z) Lω↪κ seq↪κ) pairκ))
      pairκ

二つの単射を合成すれば、真に新しい証人の数え上げが得られます。そのような証人はそれぞれある p ∈ PB で符号化され、PB は κ へ単射するので、Dw も κ へ単射します。

    Dw↪κ : InjL Dw κ
    Dw↪κ = injl-trans Dw PB κ Dw↪PB PB↪κ

新しい部分 D₂ は D∅ ∪ Dw に含まれます。D∅ は空集合に等しい新しい要素だけを含み、それ自身が空の場合もあります。Dw は空でない証人の要素を含みます。二つの数え上げにタグを付けて κ × κ へ入れ、pairκ で折りたたすと D₂ ↪ κ が得られます。

    D₂↪κ : InjL D₂ κ
    D₂↪κ = injl-trans D₂ U₃.D κ (inclusion-coded D₂ U₃.D D₂⊆)
      (injl-trans U₃.D (prodL κ) κ (tag-union κ (num∈κ ) (num∈κ ) D∅ Dw D∅↪κ Dw↪κ) pairκ)

ΦZ の各要素は Z ∪ D₂ に属します。与えられたグラフ E が Z を数え、先の構成が D₂ を数えます。この二つの単射にタグを付けて κ × κ へ写し、pairκ と合成すると ΦZ ↪ κ が得られます。

    result : InjL ΦZ κ
    result = injl-trans ΦZ U₁.D κ (inclusion-coded ΦZ U₁.D ΦZ⊆)
      (injl-trans U₁.D (prodL κ) κ (tag-union κ (num∈κ ) (num∈κ ) Z D₂ ∣ E , cE ∣₁ D₂↪κ) pairκ)