後者段階の要素の正準な名前

module Naming (A : S) (w : SWO ⟪ A ⟫) where

module DA = DefOf A
open DA using ( _⊨ᵐ_ )

Name : Type ℓ
Name = Σ[ k ∶ ℕ ] (Formula (⊥* {ℓ}) (suc k) × Vec ⟪ A ⟫ k)

射たちは三つの鍵の出所に名前を与える。arity はその数を返し、formula はちょうど一つ多い変数スロットをもつパラメータなし論理式を、params は列を返す。それらの型は名前そのものに依存する。だから formula a はアリティ suc (arity a) に、params a は arity a に住む。この依存性こそ、のちの比較における輸送の問題すべての出所である。

arity : Name → ℕ
arity a = a .fst

formula : (a : Name) → Formula (⊥* {ℓ}) (suc (arity a))
formula a = a .snd .fst

params : (a : Name) → Vec ⟪ A ⟫ (arity a)

第一の鍵もまた射である。codeOf は論理式に limitCode を適用し、そのコードを極限段階での所属証明書とともに届ける。limitOrder が比較できるように。

params a = a .snd .snd

codeOf : Name → Limit
codeOf a = limitCode (formula a)

名前の指示対象とは、パラメータが環境として与えられたとき、その論理式が選び出す A の部分集合である。その並びはパラメータ抽象化定理が要求する順序である。環境は一つの要素とそれに続くパラメータ列からなり、すべて定義可能冪集合自身の定数解釈によって制限された台へ読み込まれ、充足は内側のものを取る。したがって指示対象は、Def A を定義したのと同じ概念によって A から切り出された部分集合である。小ささはそのまま引き継がれる。任意の論理式と任意の環境における内側の充足は小さいので、この部分集合は小さな索引型の上の sett となり、レベルの引き下げの費用は一切かからない。

述語によって A から切り出される部分集合は直接提示できる。subsetOf は A の小さな要素型の上の命題族を受け取り、索引型を「要素 m と、その m で述語が成り立つ証明」の依存対とし、その対を集合 ⟪ A ⟫↪ m へ送る sett を組み立てる。したがって索引とは証人とその証明書の対であり、結果の集合への所属はそのような対が「だけ」存在することを要求する。これは defSet と同じ形なので、どちらの形で書いた述語も同じ種類の対象を提示する。

private module SemM = FOL.Semantics DA.𝒮M
private

  subsetOf : (⟪ A ⟫ → hProp ℓ) → S
  subsetOf P = sett (Σ[ m ∶ ⟪ A ⟫ ] ⟨ P m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))

指示対象そのものの前に、提示上の二つの細部を確かめる。補題 ⟪⟫↪-inj は、写像 ⟪ A ⟫↪ が埋め込みであること、つまりその値の間の経路が根底の添字の間の経路から来ることを記録する。これにより m' ≡ m が復元され、所属の仕様の順方向を閉じるのに使われる。環境はその後組み立てられる。自由変数を担う要素 m に対し、環境は DA.ι m に DA.ι で復号したパラメータ列を続けたものである。先頭の項が部分集合を切り出す一つの余分なスロットを埋め、残りの項がパラメータのスロットを埋める。環境の長さは定義上 suc (arity a) であり、名前の論理式のアリティとちょうど一致する。

  ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
  ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

environment : (a : Name) → ⟪ A ⟫ → Vec DA.SM (suc (arity a))
environment a m = DA.ι m ∷ map DA.ι (params a)

satAt : (a : Name) → ⟪ A ⟫ → hProp ℓ

名前の指示対象を定める述語は satAt a m である。これは、埋め込まれた論理式が組み立てた環境で内側の充足を受けるという命題と同値な小さな命題である。これを subsetOf に通すと、denote a は階層の集合となり、内側の意味論が A から選んだ部分集合になる。ここで新たなサイズの決定は一切行われない。小ささは ⊨ᵐ-small を通じて一度だけ入り、sett の索引型に費やされるのである。

satAt a m = DA.⊨ᵐ-small (embed (formula a)) (environment a m) .fst

denote : Name → S
denote a = subsetOf (satAt a)

この仕様は「指示する」という語を文字どおりに述べる。A の要素がその指示対象に属するのは、内側の世界が名前の定める環境でその論理式を充足するとき、そしてそのときに限る。小さな命題への圧縮は符号化にすぎず、同値がそれを元に戻す。

この定理は命題としての経路であり、defSet-mem が述べられたのと同じ形をしている。二つの含意から ⇔toPath によって証明される。補助定義 decode は satAt a m を ⊨ᵐ-small が返す完全な対へ展開し直し、両方向がその第二成分の同値、つまり小さな命題と内側の充足の命題を結ぶ同値を使えるようにする。

denote-mem : (a : Name) (m : ⟪ A ⟫)
           → (⟪ A ⟫↪ m ∈ˢ denote a) ≡ (environment a m ⊨ᵐ embed (formula a))
denote-mem a m = ⇔toPath fwd bwd
  where
  decode = DA.⊨ᵐ-small (embed (formula a)) (environment a m)

sett への所属は添字の存在を切り捨てた形で与えるので、順方向は切断を命題へ消去し、索引 (m' , h) と ⟪ A ⟫↪ m' から ⟪ A ⟫↪ m への経路 q を得る。埋め込みの単射性が q を m' ≡ m に変え、それに沿って h を輸送すれば satAt a m の証明が得られ、decode の同値がその証明を充足の命題へ変換する。各段階は命題しか要らない場所で証明を費やすだけで、証人が選ばれることはない。

  fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩ → ⟨ environment a m ⊨ᵐ embed (formula a) ⟩
  fwd = rec₁ ((environment a m ⊨ᵐ embed (formula a)) .snd)
    (λ { ((m' , h) , q) →
      invEq (decode .snd) (subst (λ v → ⟨ satAt a v ⟩) (⟪⟫↪-inj q) h) })
  bwd : ⟨ environment a m ⊨ᵐ embed (formula a) ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩

逆方向は同じ同値を逆向きに走らせる。充足の証明が satAt a m の証明に変わり、それを自明な経路とともに索引 (m , 証明) として ∣_∣₁ で切断する。両方向を合わせると、所属と内側の充足は余りなく同一視され、これが「指示する」という語に求められた意味である。

  bwd h = ∣ (m , equivFun (decode .snd) h) , refl ∣₁

後者段階の各要素は名前をもつ

定義可能冪集合の仕様は、後続段階の各要素に定数付き論理式を与える。その定数を抽象すると、名前を構成するパラメータなし論理式とパラメータ列が得られる。

𝒟ₒ A の要素は、その演算子自身の仕様によれば、A の定数を用いた一自由変数の論理式で定義される部分集合にすぎない。パラメータ抽象化は、その論理式をより高いアリティのパラメータなし論理式へ変換し、そこに現れる定数の列を与える。後者を前者から読み出すこと、それが名付けのすべてであり、しかもそれは関数である。

関数 nameOf は三つの鍵を一度に組み立てる。countFo φ は定数の出現を一つずつ数えてアリティを与え、したがって抽象 absFo φ は 1 + countFo φ 個の自由スロット、つまりアリティの後続数のところに住む。constantsFo φ は同じ順序で定数を並べ、⟪ A ⟫ の中のちょうどその長さの列である。nameOf が受け取るのは定数付きの論理式であって、名前のパラメータなし成分ではないことに注意してほしい。抽象化は定義の内部で、構成子ごとに一つの節として行われる。

nameOf : Formula ⟪ A ⟫  → Name
nameOf φ = countFo φ , (absFo φ , constantsFo φ)

その妥当性はパラメータ抽象化定理 ⊨-abs₁ から従い、その前に空の定数領域に対する二つの解釈を同一視する。パラメータなし論理式には二つの読み方が現れるので、まず両者を同一視しなければならない。名前の指示対象は embed を通して定数域 ⟪ A ⟫ の中で式を読み、一方抽象化の定理は空の定数域で読む。二つの解釈は空型から出る関数なので一致し、この一致を述べることが同一視に必要な検証のすべてである。

抽象化の定理 ⊨-abs₁ は空の定数域の上での充足を語り、一方名前の意味論は ⟪ A ⟫ の上の充足を読む。二つの命題を項ごとに比べるため、emptySat は任意の定数解釈 f : ⊥* → DA.SM における充足の命題の形を固定し、f の変更を関数の関数への適用の問題にする。論理式そのものは定数を一切言及しないので、この一様性が使えるのである。

private
  emptySat : (f : ⊥* {ℓ} → DA.SM) {n : ℕ}
           → Vec DA.SM n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
  emptySat f γ χ = γ ⊨ᶠ χ
    where open SemM.At (⊥* {ℓ}) f using () renaming ( _⊨_ to _⊨ᶠ_ )

パラメータなし論理式の二つの定数解釈は、どちらも型 ⊥* → DA.SM をもつ。作業用の意味論が使う方、すべての定数を DA.ι (⊥*-rec b) へ送るものと、消去子 ⊥*-rec 自身である。⊥* には要素がないので、funExt と消去子だけで二つの関数の相等 sameReading が証明され、何も検査する必要がない。そして absSat は、指示対象が embed を通して使う環境の読み方と、抽象化の定理が使う空定数域の読み方が、同じ要素 m と同じ抽象化された論理式において一致することを述べる。

  sameReading : (λ (b : ⊥* {ℓ}) → DA.ι (⊥*-rec b)) ≡ ⊥*-rec
  sameReading = funExt (λ b → ⊥*-rec b)

  absSat : (φ : Formula ⟪ A ⟫ ) (m : ⟪ A ⟫)
         → (environment (nameOf φ) m ⊨ᵐ embed (formula (nameOf φ)))
         ≡ ((DA.ι m ∷ []) ⊨ᵐ φ)

証明は三段の経路である。改名の補題 embed-⊨ は、パラメータなし論理式をより豊かな定数域へ埋め込んでもその意味は変わらないと言い、これが左辺を ⊥*-rec の標識の読み方へ移す。次に sameReading が指示対象自身の読み方をそこへ代入する。最後に ⊨-abs₁ を逆向きに読むと、抽象化された論理式の単一パラメータにおける充足と元の論理式の充足とを同一視する抽象化の定理そのものである。各段階は前の章の定理をつなぐだけで、再証明はしない。

  absSat φ m =
      embed-⊨ DA.𝒮M DA.ι (absFo φ)
        (environment (nameOf φ) m)
    ∙ cong (λ f → emptySat f (environment (nameOf φ) m) (absFo φ)) sameReading
    ∙ sym (⊨-abs₁ DA.𝒮M DA.ι φ (DA.ι m))

二つの読み方を命題の面で同一視したうえで、satAt-abs はこの同一視を充足の命題から、集合が構成される小さな命題へ引き上げる。比較するのは、名前の指示対象の根底にある小さな命題 satAt (nameOf φ) m と、defSet φ の根底にある小さな命題 DA.smallSat φ m である。補助名 big と small がそれぞれの ⊨ᵐ-small の対を展開し、どちらの方向も二つの同値を使えるようにする。

  satAt-abs : (φ : Formula ⟪ A ⟫ ) (m : ⟪ A ⟫)
            → satAt (nameOf φ) m ≡ DA.smallSat φ m
  satAt-abs φ m = ⇔toPath fwd bwd
    where
    big = DA.⊨ᵐ-small (embed (formula (nameOf φ))) (environment (nameOf φ) m)

順方向は三つの変換を証明に施して合成する。まず大きい方の同値を逆向きに走らせて埋め込まれた充足の命題に達し、経路 absSat φ m に沿って証明を空定数域の命題へ輸送し、それから小さい方の同値を順方向に走らせて DA.smallSat φ m に達する。経路 absSat φ m が二つの充足型を同一視するので、通常の輸送によって証明を必要な向きへ移せる。命題性は充足型を hProp としてまとめるために使われ、輸送そのものが必要とするのはこの経路である。

    small = DA.⊨ᵐ-small φ (DA.ι m ∷ [])
    fwd : ⟨ satAt (nameOf φ) m ⟩ → ⟨ DA.smallSat φ m ⟩
    fwd h = equivFun (small .snd) (subst ⟨_⟩ (absSat φ m) (invEq (big .snd) h))
    bwd : ⟨ DA.smallSat φ m ⟩ → ⟨ satAt (nameOf φ) m ⟩
    bwd h = equivFun (big .snd)

逆方向は同じ合成で経路を逆向きにしたものである。sym (absSat φ m) が証明を逆方向へ動かし、二つの同値も逆の順序で適用される。ここで新たに証明されるものはない。要点は、すべての m に対して satAt (nameOf φ) m と DA.smallSat φ m が同じ小さな命題であることであり、これが次の段階で二つの集合を等しくするのである。

      (subst ⟨_⟩ (sym (absSat φ m)) (invEq (small .snd) h))

どちらの部分集合も、その要素の上の小さな述語によって A から切り出されている。したがって二つの述語が等しければ、二つの集合は合同によって等しく、外延性を持ち出す必要はない。完全性はその等式に沿って輸送すれば得られ、命題的に切り詰めた形で述べられる。定義可能冪集合が論理式を与える仕方がもともとそうだからである。

等式 denote-defSet は、述語の一致 satAt-abs を集合の等式に変えたものである。funExt が点ごとの等しさを述語族の等しさにまとめ、cong subsetOf がそれを提示された集合へ運ぶ。完全性は証明書 h : ⟨ x ∈ˢ 𝒟ₒ A ⟩ を 𝒟ₒ-inv で反転することから始まる。これは defSet φ ≡ x を満たす論理式 φ を「だけ」与えるものであり、したがって結論も名前と等式の存在を切り詰めた形であり、選ばれた名前ではない。

denote-defSet : (φ : Formula ⟪ A ⟫ ) → denote (nameOf φ) ≡ DA.defSet φ
denote-defSet φ = cong subsetOf (funExt (satAt-abs φ))

names-complete : (x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
               → ∥ Σ[ a ∶ Name ] (denote a ≡ x) ∥₁
names-complete x h = map₁ named (𝒟ₒ-inv A x h)

切断の内側では、反転されたデータから求める対への段階は普通のものである。論理式 φ は nameOf φ によって名付けられ、必要な等式は denote-defSet φ ∙ q、つまり名前の指示対象から defSet φ への経路に、与えられた x への経路を続けたものである。目標の ∥ Σ[ a ∶ Name ] (denote a ≡ x) ∥₁ は命題なので、map₁ は切断の下で働き、ただ与えられた論理式をただ与えられた名前へ写す。それがどの論理式かを検査することは一切ない。

  where
  named : Σ[ φ ∶ Formula ⟪ A ⟫  ] (DA.defSet φ ≡ x)
        → Σ[ a ∶ Name ] (denote a ≡ x)
  named (φ , q) = nameOf φ , (denote-defSet φ ∙ q)

パラメータ列上の順序

パラメータ列は A の要素に与えられた整列順序によって辞書式に比較する。この関係は異なる二つの長さを受け取り、一方が先に尽きる場合には先行元を持たず、両方が空でなければ先頭を比較し、先頭が等しいときだけ尾へ進む。この形により、三つの列の実際の長さのまま推移性を使える。三分性は後で、アリティの経路に沿って一方を他方の長さへ輸送してから適用する。

ここでは二つの整列順序が働いており、どちらも短い名前で一度に固定される。極限段階の順序 limitOrder は論理式コードを比較し、_≺_ と改名される。モジュールパラメータ w、つまり A の要素の上の整列順序はパラメータを比較し、_≺ₚ_ と改名される。各 open は三分性・非反射性・推移性・整礎性の法則も改名するので、これからの証明はどちらの順序の法則も長い修飾名なしに呼び出せる。

open SWO limitOrder using () renaming
  ( _<∙_ to _≺_ ; tri∙ to ≺-tri ; irr∙ to ≺-irr
  ; trans∙ to ≺-trans ; wf∙ to ≺-wf )
open SWO w using () renaming
  ( _<∙_ to _≺ₚ_ ; tri∙ to ≺ₚ-tri ; irr∙ to ≺ₚ-irr

比較そのものは両ベクトルのパターン照合で定義され、長さ j と k で添字づけられる。どちらかの列が空なら、それ以上の降下は不可能で、結果の型は空型になる。使い尽くされた列の下にはどの位置にも何もないのである。これらの場合は費用がゼロで、反証できるという事実こそ、推移性と非反射性の証明で使われるものである。

  ; trans∙ to ≺ₚ-trans ; wf∙ to ≺ₚ-wf )

infix  _≺ᵥ_
_≺ᵥ_ : ∀ {j k} → Vec ⟪ A ⟫ j → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ)
[]      ≺ᵥ []      = ⊥*
[]      ≺ᵥ (y ∷ q) = ⊥*

二つの空でない列は先頭で比較される。先頭 x がパラメータ順序で y より下に落ちるか、先頭同士が経路として等しく、降下が尾へ続くかのどちらかである。狭義の場合が和の左の支、等しい先頭の場合が右の支なので、後の証明はどの位置が先に判定したかで場合分けできる。先頭の相等は経路 x ≡ y であり、推移性の混在する場合はこれを比較の中へ代入することになる。

(x ∷ p) ≺ᵥ []      = ⊥*
(x ∷ p) ≺ᵥ (y ∷ q) = (x ≺ₚ y) ⊎ ((x ≡ y) × (p ≺ᵥ q))

四つの法則のうち三つはそのままの帰納法で得られる。非反射性と三分性は長さが等しいことを要求する。列がある列と等しくなりうるのはそこでだけだからである。推移性はそれを要求せず、三つの異なる長さの列を受け取り、すべての列が空でない場合を除くすべての場合が空型によって反証される。

非反射性はベクトルに関する帰納法で証明される。ベクトルが自分自身より下になることは決してない。p ≺ᵥ p は二つの出現が同じ長さをもつことを要求するので、この命題は単一の長さでのみ意味をもち、帰納法は一段短い長さでの命題を尾に対して消費する。続いて推移性の命題が続く。こちらは三つの長さに対して一度に述べられる。

≺ᵥ-irr : ∀ {k} (p : Vec ⟪ A ⟫ k) → p ≺ᵥ p → ⊥₀
≺ᵥ-irr []      h             = ⊥*-rec h
≺ᵥ-irr (x ∷ p) (inl h)       = ≺ₚ-irr x h
≺ᵥ-irr (x ∷ p) (inr (_ , h)) = ≺ᵥ-irr p h

≺ᵥ-trans : ∀ {i j k} (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ j) (r : Vec ⟪ A ⟫ k)

推移性は三つのベクトルに対する同時の場合分けで証明される。最初の降下が使い尽くされた列から始まるなら、その比較の型はすでに空型であり、中間の列が使い尽くされた場合も同様である。三番目の列が使い尽くされた場合は、二番目の比較が反証可能である。そのようなすべての場合において証明は空型の消去子であり、それ自体の数学的内容はない。

         → p ≺ᵥ q → q ≺ᵥ r → p ≺ᵥ r
≺ᵥ-trans []      []      r       h k = ⊥*-rec h
≺ᵥ-trans []      (y ∷ q) r       h k = ⊥*-rec h
≺ᵥ-trans (x ∷ p) []      r       h k = ⊥*-rec h
≺ᵥ-trans (x ∷ p) (y ∷ q) []      h k = ⊥*-rec k

三つの列がすべて空でないとき、比較は先頭から読み取れ、最初の二つの混在する場合が興味の対象である。x が y より下で y が z と等しいなら、その経路を最初の比較に代入して x が z より下であることが得られる。対称的に、x ≡ y の後に y が z より下が続くなら、二番目の比較を経路に沿って逆向きに輸送する。どちらも同じ動きの実例である。要素の経路は輸送によって比較に作用するのである。

≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inl k) = inl (≺ₚ-trans x y z h k)
≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inr (e , k)) =
  inl (subst (λ v → x ≺ₚ v) e h)
≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inl k) =
  inl (subst (λ v → v ≺ₚ z) (sym e) k)

推移性の最後の場合は両方の先頭をそのままにする。二つの経路は x ≡ z に連結され、再帰は尾へ降りる。長さはそれぞれの列がもつものそのままである。推移性が済むと、三分性は一つの長さをもつ二つの列に対して述べられる。二つの列が一致しうるのはそこでだけだからである。空の列どうしは refl によって等しくなる。

≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inr (e' , k)) =
  inr (e ∙ e' , ≺ᵥ-trans p q r h k)

≺ᵥ-tri : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Tri (p ≺ᵥ q) (p ≡ q) (q ≺ᵥ p)
≺ᵥ-tri []      []      = eq refl
≺ᵥ-tri (x ∷ p) (y ∷ q) = decide (≺ₚ-tri x y)

空でない列では、先頭がパラメータ順序の三分性によって比較され、補助 decide が判定を先頭から列全体へ運ぶ。どちら向きの狭義の判定も左の支になる。先頭で決着がつき、尾は一切登場しないからである。等しい場合だけが尾を調べる必要があり、それは次で扱われる。

  where
  decide : Tri (x ≺ₚ y) (x ≡ y) (y ≺ₚ x)
         → Tri ((x ∷ p) ≺ᵥ (y ∷ q)) ((x ∷ p) ≡ (y ∷ q)) ((y ∷ q) ≺ᵥ (x ∷ p))
  decide (lt h) = lt (inl h)
  decide (gt h) = gt (inl h)

先頭が経路 e によって等しいとき、ベクトルの比較は尾の比較に帰着し、Tri-map が三つの結果に付け替える。尾が狭義に下なら右の支 e , h となり、尾が等しいことは cong₂ _∷_ のもとで列全体の相等となり、鏡像の判定には sym e が付く。再帰は尾について構造的で、帰納はここで閉じる。

  decide (eq e) =
    Tri-map (λ h → inr (e , h)) (cong₂ _∷_ e) (λ h → inr (sym e , h))
      (≺ᵥ-tri p q)

整礎性は計画を要するものである。ベクトルから降りていくと、先頭が与えられた順序で落ちて尾が同じ長さの任意のものに置き換わるか、先頭はそのままで尾が落ちるかのどちらかである。したがって降下は二重の帰納である。先頭には与えられた順序の整礎性を、尾には尾の到達可能性を使い、任意の尾は一段短い長さでの命題が供給する。この第三の材料があるからこそ、全体も長さについて再帰する。また、先頭の帰納を再帰引数ではなく帰納原理として取るのはこのためである。三つの要求を一つの再帰で同時に満たそうとすると、降下が単一の減少尺度を提示できなくなるからである。

補助 consAcc は到達可能性を長さ k から suc k へ持ち上げる。長さ k のすべての列が到達可能であるという仮定のもとで、y ∷ q の到達可能性を組み立てる。入力 prev は一段前の長さでの命題そのものであり、狭義の場合に尾を同じ長さの任意の r に置き換えられるのはこのためである。証明は先頭について与えられた順序の整礎帰納を実行し、先頭の降下が駆動装置となり、尾の到達可能性はその内部で使われる。

private
  consAcc : (k : ℕ) → ((r : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) r)
          → (y : ⟪ A ⟫) (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q
          → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q)
  consAcc k prev = WFI.induction ≺ₚ-wf onHead

帰納仮説 ih の述べ方は慎重である。y より狭義に下のすべての z に対し、尾自身の到達可能性を与えれば、z ∷ q の到達可能性が長さ k のすべての尾 q について成り立つというものである。q についての全称量化があるから、狭義の場合は調べているベクトルへの再帰なしに機能する。そしてこれが可能なのは、≺ₚ-wf を再帰的に呼び出すのではなく帰納原理として適用したからである。

    where
    onHead : (y : ⟪ A ⟫)
           → ((z : ⟪ A ⟫) → z ≺ₚ y → (q : Vec ⟪ A ⟫ k)
                → Acc (_≺ᵥ_ {k} {k}) q → Acc (_≺ᵥ_ {suc k} {suc k}) (z ∷ q))
           → (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q

到達可能性は構成されたデータである。acc は要素と、狭義に下のすべての要素をその要素自身の到達可能性へ送る関数とを対にする。したがって y ∷ q に対する目標は acc によって与えられ、それに適用されるのは、y ∷ q からの狭義の降下が取りうる二つの形を処理するステップ関数である。証明の残りはこのステップ関数の本体である。

           → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q)
    onHead y ih q (acc rq) = acc step
      where
      step : (r : Vec ⟪ A ⟫ (suc k)) → r ≺ᵥ (y ∷ q)
           → Acc (_≺ᵥ_ {suc k} {suc k}) r

狭義の場合は先頭 z が y より下で、尾 r は任意である。ここでは帰納仮説がすべての仕事をする。z ≺ₚ y と、長さ k における r の到達可能性 prev r とから、z ∷ r の Acc が供給される。等しい場合は先頭を保つ。経路が z と y を同一視するので、y ∷ r の到達可能性を sym e に沿って逆向きに輸送すれば z ∷ r の到達可能性が得られる。先頭の経路に沿ったこの輸送が、長さを越えた比較の代価であり、ここで一度だけ支払われる。

      step (z ∷ r) (inl h)       = ih z h r (prev r)
      step (z ∷ r) (inr (e , h)) =
        subst (λ v → Acc (_≺ᵥ_ {suc k} {suc k}) (v ∷ r)) (sym e)
          (onHead y ih r (rq r h))

≺ᵥ-wf : (k : ℕ) (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p

主定理は長さに関する帰納法である。空の列の到達可能性は直ちに得られる。唯一の候補となる先行要素は空の列自身であり、その比較は空型だからである。x ∷ p に対しては consAcc を適用し、≺ᵥ-wf k が一段前の長さでの任意の尾についての命題を、≺ᵥ-wf k p がこの列自身の尾の到達可能性を供給する。両方とも k に関する一つの構造的再帰から来る。

≺ᵥ-wf     []      = acc (λ { [] h → ⊥*-rec h })
≺ᵥ-wf (suc k) (x ∷ p) = consAcc k (≺ᵥ-wf k) x p (≺ᵥ-wf k p)

この比較に伴って一つの派生的な事実が使われ、経路の帰納法で証明される。列を長さの等式に沿って移しても、それが何の下にあるか、何がその下にあるかは変わらない。これが必要なのは三分性と降下の二箇所で、どちらも長さが等しいが同一ではない二つの列に出会う。

左側の補題は、比較 subst (Vec ⟪ A ⟫) e p ≺ᵥ q が p ≺ᵥ q への経路であること、つまり比較される列を長さの等式 e に沿って輸送しても比較の命題は変わらないことを述べる。証明はベクトルの場合分けをまったく展開しない。一般の補題 constSubstCommSlice は、e に沿う輸送が添字を使わない型族と可換であることを言い、固定された q との比較はまさにそのような型族である。sym は等式を後の証明が必要とする向きに整える。

private
  ≺ᵥ-subst-left : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ k)
                → (subst (Vec ⟪ A ⟫) e p ≺ᵥ q) ≡ (p ≺ᵥ q)
  ≺ᵥ-subst-left e p q = sym (constSubstCommSlice
    (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → v ≺ᵥ q) e p)

右側の補題は鏡像である。もう一方の列をそれ自身の長さの等式に沿って移しても、その下にあるものは変わらない。両方向が必要なのは、名前の比較が lt の場合は最初の名前のパラメータを二番目の長さへ輸送し、gt の場合は逆向きだからであり、後の整礎性の証明ではどちら側も動く。両方の向きを一度に述べておけば、これ以降の証明は列の上の subst について推論する必要がなくなる。

  ≺ᵥ-subst-right : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i)
                 → (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q)
  ≺ᵥ-subst-right e p q = sym (constSubstCommSlice
    (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)

三つの鍵を順に比較する

名前は論理式コード、アリティ、パラメータ列の順に辞書式で比較する。比較を三つの場合として明示することで、三分性と推移性を鍵ごとに示せる。

この比較は定義からそのまま読み取れる型の族である。外側の支は、極限順序の下での論理式コードの狭義の比較である。一方の名前のコードが他方より下なら、コードが判定し、他は一切問われない。右の支は経路 codeOf b ≡ codeOf a、つまり次の鍵へ進むことを許すコードの相等を携え、それを第二の鍵の比較、自然数のアリティの狭義の不等号と組みにする。

infix  _≺ₙ_
_≺ₙ_ : Name → Name → Type (ℓ-suc ℓ)
a ≺ₙ b = (codeOf a ≺ codeOf b)
       ⊎ ( (codeOf b ≡ codeOf a)
         × ( (arity a < arity b)

最も内側の支が降下を完成させる。コードが等しくアリティも等しい場合、後者はやはり経路 arity b ≡ arity a として携えられ、その上でパラメータ列が _≺ᵥ_ によって比較される。したがって入れ子の各層は「前の鍵の相等」と「次の鍵の狭義の比較」の対であり、四つの法則の場合分けはまさにこの形に沿って鍵ごとに進む。

           ⊎ ((arity b ≡ arity a) × (params a ≺ᵥ params b)) ) )

非反射性と推移性は、三つの鍵それぞれの法則を場合分けで並べたものである。推移性の混在する場合は、一方の鍵の等式を他方の鍵の比較に代入するだけで、必要な検証はそれですむ。パラメータの場合は三つの長さでの列の比較を援用する。あの比較を長さを越えて証明したのはこのためである。

名前が自分自身より狭義に下になることは決してなく、三つの節がそれぞれ理由を言う。a ≺ₙ a を証明する和の支はどれも、三つの鍵のどれかが自分自身への狭義の降下を与えることになるからである。コードの場合は極限順序の非反射性と矛盾し、アリティの場合は自分自身より小さい自然数となり ¬m<m で反証され、パラメータの場合は params a 自身の長さでの列の非反射性と矛盾する。

≺ₙ-irr : (a : Name) → a ≺ₙ a → ⊥₀
≺ₙ-irr a (inl h)                 = ≺-irr (codeOf a) h
≺ₙ-irr a (inr (_ , inl h))       = ¬m<m h
≺ₙ-irr a (inr (_ , inr (_ , h))) = ≺ᵥ-irr (params a) h

≺ₙ-trans : (a b c : Name) → a ≺ₙ b → b ≺ₙ c → a ≺ₙ c

推移性は三つの名前に対して述べられ、二つの比較がそれぞれどこで決着したかによる場合分けで証明される。両方がコードで決着したときは、極限順序の推移性を直接適用する。最初の混在した場合は、a がコードで b より狭義に下であり、二番目の比較が知っているのは codeOf c ≡ codeOf b だけである。その等式を逆向きに代入すれば codeOf a が codeOf c より下であることが得られ、対称の場合は同じ代入を順方向に読んだものである。混在した各場合は輸送が一回あるだけで、それ以上ではない。

≺ₙ-trans a b c (inl h) (inl k) =
  inl (≺-trans (codeOf a) (codeOf b) (codeOf c) h k)
≺ₙ-trans a b c (inl h) (inr (q , _)) =
  inl (subst (λ v → codeOf a ≺ v) (sym q) h)
≺ₙ-trans a b c (inr (q , _)) (inl k) =

アリティの鍵で決着した場合は、自然数で同じ型を繰り返す。二つの狭義のアリティの不等号は <-trans で合成され、狭義の不等号とアリティの等式が並ぶときは、適切な端点を代入する輸送で狭義の不等号に変わる。携えられる経路の向きに注意してほしい。比較が記録するのは codeOf b ≡ codeOf a と arity b ≡ arity a、つまりより大きな名前の側で述べた相等なので、連結と代入はその向きに逆らって走る。

  inl (subst (λ v → v ≺ codeOf c) q k)
≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inl k)) =
  inr (q' ∙ q , inl (<-trans h k))
≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inr (e , _))) =
  inr (q' ∙ q , inl (subst (λ j → arity a < j) (sym e) h))

最後の場合は、三つの鍵がパラメータに至るまで一致しているところであり、ここでまさに必要なのが第三の鍵の三つの長さでの推移性である。≺ᵥ-trans はそれぞれの列のもつ長さで params a ≺ᵥ params b と params b ≺ᵥ params c を受け取り、params a ≺ᵥ params c を返す。二つのアリティの経路は arity a ≡ arity c に連結され、右の支の三つの成分がそろう。

≺ₙ-trans a b c (inr (q , inr (e , _))) (inr (q' , inl k)) =
  inr (q' ∙ q , inl (subst (λ j → j < arity c) e k))
≺ₙ-trans a b c (inr (q , inr (e , h))) (inr (q' , inr (e' , k))) =
  inr (q' ∙ q , inr (e' ∙ e , ≺ᵥ-trans (params a) (params b) (params c) h k))

三歧性は三番目の法則であり、他の法則を組み合わせるのではなく比較そのものを読み取るものである。証明は鍵の順に降りていく。コードがすでに判定を与えれば直ちに結論が出て、コードが等しければアリティが判定し、アリティも等しければパラメータ列が判定する。最後の段階だけが注意を要する。等しいアリティは同一化ではなく経路で結ばれているため、params a と params b は異なる長さに住んでいる。まず前者を後者の長さへ輸送しなければベクトル比較は実行できず、比較が返す狭義の判定も元の型へ輸送し戻して初めて、元の二つの名前の間の比較になる。等しい場合はさらに多くが要る。二つの名前を等しい依存三つ組として提示しなければならないので、論理式そのものも一致する必要があり、それを与えるのがまさにコードの単射性である。code-shift はアリティの経路に沿う輸送がコードを変えないことを述べ、コード上の判定はコードがすでに一致していると言っているからである。

主張の型は Tri、つまり三択の判定であり、a ≺ₙ b の証明、経路 a ≡ b、あるいは b ≺ₙ a の証明のいずれかを運ぶ。証明は問題全体をコード上の順序に委ねる。≺-tri はすでに二つのコードに対しこうした判定を返すので、局所的な補助関数 byCodes がコード上の判定を名前上の判定へ変換する。補助関数はまず型で導入されるため、変換の形が各節の前に見えている。

≺ₙ-tri : (a b : Name) → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
≺ₙ-tri a b = byCodes (≺-tri (codeOf a) (codeOf b))
  where
  byCodes : Tri (codeOf a ≺ codeOf b) (codeOf a ≡ codeOf b) (codeOf b ≺ codeOf a)
          → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)

狭義の場合は直接である。どちら向きであれ、コードの狭義比較は名前の順序の和の左成分そのものである。等しい場合は第二の鍵が開かれ、byArities に委ねられる。これはアリティに対して、byCodes がコードに対してしたのと同じことをする。

  byCodes (lt h) = lt (inl h)
  byCodes (gt h) = gt (inl h)
  byCodes (eq ec) = byArities (arity a ≟ arity b)
    where
    byArities : NatOrder.Trichotomy (arity a) (arity b)

ここでの判定は和の右成分を取り、コードの等式そのものを運ぶ。向きに注意してほしい。比較は大きな名前の側で述べた codeOf b ≡ codeOf a を記録するので、こちらの狭義の場合には sym ec が、双対の場合には書かれたままの ec が要る。アリティも等しいときは ≺ᵥ-tri がベクトルを比較するが、params a は長さ arity a、params b は arity b に住むので、最初のベクトルはアリティの経路 e に沿って輸送されてから比較される。

              → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
    byArities (NatOrder.lt h) = lt (inr (sym ec , inl h))
    byArities (NatOrder.gt h) = gt (inr (ec , inl h))
    byArities (NatOrder.eq e) =
      byParams (≺ᵥ-tri (subst (Vec ⟪ A ⟫) e (params a)) (params b))

輸送されたベクトルには shifted という名前が与えられ、以下の記述が各自の実際の長さで読みやすく保たれる。等しい場合に必要なのはベクトルだけではない。a ≡ b を直接得るには論理式も一致しなければならず、sameFormula は輸送された論理式のところでこれを述べる。その型は、アリティ arity b の名前の論理式の型である。この等式がなければ、二つの名前は判定済みの二つの鍵でもパラメータでも一致しながら、構文の上ではなお異なり得る。

      where
      shifted : Vec ⟪ A ⟫ (arity b)
      shifted = subst (Vec ⟪ A ⟫) e (params a)

      sameFormula : subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a)
                  ≡ formula b

なぜ論理式が一致するのか。code-shift により、formula a を e に沿って輸送してもそのコードは変わらず、ec の第一成分は formula a のコードが formula b のコードと等しいことを述べる。これらを連結すれば等しいコードが得られ、code-inj が等しいコードを等しいパラメータなし論理式へと戻す。これは本章の前半で証した単射性そのものであり、ここでその主張が予期していた仕事を果たす。shifted と sameFormula がそろえば、byParams がベクトル上の判定を名前上の判定へ変換する。

      sameFormula =
        code-inj (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a))
          (formula b)
          (code-shift e (formula a) ∙ cong (λ p → p .fst) ec)

      byParams : Tri (shifted ≺ᵥ params b) (shifted ≡ params b)

狭義の判定は輸送後の長さで得られたので、その述べ方を元へ戻す必要がある。≺ᵥ-subst-left は、subst (Vec ⟪ A ⟫) e p を q と比べることは命題として p を q と比べることと同じだと言うので、h をこの等式に沿って輸送すれば shifted についての比較が params a についての比較に変わる。どちらの判定も、和が要求する向きに揃えたコードとアリティの等式を運ぶ。双対の場合は対称で、比較の反対側の ≺ᵥ-subst-right を使う。

                     (params b ≺ᵥ shifted)
               → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
      byParams (lt h) = lt (inr (sym ec , inr (sym e ,
        transport (≺ᵥ-subst-left e (params a) (params b)) h)))
      byParams (gt h) = gt (inr (ec , inr (e ,

等しいという判定は Name の二つの元の間の経路であり、Name はそれ自身三つ組である。ΣPathP はアリティの経路 e を残りの成分どうしの経路と組み合わせる。toPathP sameFormula が論理式の等式を型族 Formula (⊥*) (suc k) に沿って持ち上げ、toPathP ep がベクトルの等式に同じことをする。ここが sameFormula の出番である。判定済みの二つの鍵が等しくパラメータも等しい後、欠けているのは論理式の等式だけであり、それが補われれば二つの名前はデータとして同一になる。

        transport (≺ᵥ-subst-right e (params b) (params a)) h)))
      byParams (eq ep) =
        eq (ΣPathP (e , ΣPathP (toPathP sameFormula , toPathP ep)))

三つの鍵に沿って降下する

整礎性は入れ子になった降下に従い、鍵ごとに一層をなす。最内層ではコードとアリティを固定してパラメータ列を降り、減少する引数はベクトルの到達可能性である。中層ではコードを固定してアリティを降り、最外層ではコードを降りる。各層は外側の層の帰納仮定を引数として受け取る別個の関数なので、それぞれがちょうど一つの到達可能性の証明について再帰し、再帰は至る所構造的である。すべての主張は名前そのものの上で、各鍵の位置を言う等式とともになされる。これは三歧性で見たのと同じ規律であり、名前の射影の上で述べた内容は名前の上で述べた内容と一致させなければならない。

最内層は、降下の全体像を一つの引数列に記録する関数である。与えられるのは、固定されたコード c、コードが c より下のすべての名前を覆う外側の帰納仮定 ihC、境界 k、コードが c でアリティが k より下の名前を覆う中層の帰納仮定 ihK、それ自身のベクトル到達可能性をもつパラメータ列 p、そして研究対象の名前 a と、三つの等式である。qc はコードを c に、ek はアリティを k に固定し、qp は輸送されたパラメータ列を p と同一視する。結論は単に a が到達可能だということである。

private
  accAtParam : (c : Limit)
             → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
             → (k : ℕ)
             → ((b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b)

ベクトル到達可能性のパラメータの型は単一の長さ k で述べられ、p と一致している。これが、パラメータをその場で比較するのではなく等式 qp によって p の長さへ輸送する理由である。a の到達可能性は構成子 acc とステップ関数によって与えられる。すべての名前が到達可能だと示すには、各 a に対し、a より下の任意の b を受け取って b の到達可能性を返す関数を示せば十分である。

             → (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p
             → (a : Name) → codeOf a ≡ c → (ek : arity a ≡ k)
             → subst (Vec ⟪ A ⟫) ek (params a) ≡ p
             → Acc _≺ₙ_ a
  accAtParam c ihC k ihK p (acc rp) a qc ek qp = acc step

ステップ関数は、どの鍵が b ≺ₙ a を判定したかで場合分けする。コードが落ちた場合、qc は codeOf b ≺ codeOf a を codeOf b ≺ c へ移し、外側の帰納仮定で終わる。アリティが判定した場合、この先行元の判定は q : codeOf a ≡ codeOf b を運ぶので、sym q ∙ qc : codeOf b ≡ c が得られる。さらに ek : arity a ≡ k に沿って arity b < arity a を arity b < k へ輸送すれば、中層の帰納仮定を適用できる。

    where
    step : (b : Name) → b ≺ₙ a → Acc _≺ₙ_ b
    step b (inl h)           = ihC b (subst (λ v → codeOf b ≺ v) qc h)
    step b (inr (q , inl h)) = ihK b (sym q ∙ qc) (subst (λ j → arity b < j) ek h)
    step b (inr (q , inr (e , h))) =

残るのはパラメータの鍵であり、最内層で再帰する唯一の場合である。先行元の判定 b ≺ₙ a では、この枝は e : arity a ≡ arity b を与え、ek : arity a ≡ k は現在の名前を固定アリティに結ぶ。したがって eb = sym e ∙ ek は arity b ≡ k をもち、これに沿って params b を輸送すると固定長の先行ベクトル pb が得られる。コードの等式は独立に sym q ∙ qc で揃える。

      accAtParam c ihC k ihK pb (rp pb hb) b (sym q ∙ qc) eb refl
      where
      eb : arity b ≡ k
      eb = sym e ∙ ek
      pb : Vec ⟪ A ⟫ k

狭義の比較 h は params b と params a の間で各自の長さでなされたもので、用いられる到達可能性は p のものである。この隔たりは二つの操作で埋まる。≺ᵥ-subst-left と ≺ᵥ-subst-right は、長さの等式に沿う輸送がベクトルの下辺を変えないと言うので、まず h を境界の長さでの比較へ書き換える。次に qp が右端点を params a から p へ輸送し、hb : pb ≺ᵥ p が得られる。再帰呼び出しは hb を p の到達可能性である rp に渡し、b の到達可能性を返す。

      pb = subst (Vec ⟪ A ⟫) eb (params b)
      hb : pb ≺ᵥ p
      hb = subst (λ v → pb ≺ᵥ v) qp
        (transport (sym (≺ᵥ-subst-right ek pb (params a)))
          (transport (sym (≺ᵥ-subst-left eb (params b) (params a))) h))

中層は一つのコードを固定し、アリティに沿って降りる。引数列は短くなる。コードの帰納仮定 ihC、自然数順序での到達可能性をもつ境界 k、そしてコードを c に、アリティを k に固定された名前である。ベクトルの到達可能性の代わりになったのは自然数の到達可能性 rk で、アリティの鍵は ℕ の中で降りるからである。

  accAtArity : (c : Limit)
             → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
             → (k : ℕ) → Acc _<_ k
             → (a : Name) → codeOf a ≡ c → arity a ≡ k → Acc _≺ₙ_ a
  accAtArity c ihC k (acc rk) a qc ek =

本体はすべてを最内層に委ねる。パラメータ列は k へ輸送され、そのベクトル到達可能性は ≺ᵥ-wf がすべての長さのすべてのベクトルに対して成り立つので、ここでは再帰を要求せずそのまま供給される。真の帰納はアリティについてだけである。局所的な ihK が自然数の到達可能性 rk をほどき、コードが c でアリティが真に小さい名前はその小さい境界での再帰呼び出しで処理される。この層が、任意の名前の真に小さいアリティを小さい境界へ変換する場所である。

    accAtParam c ihC k ihK (subst (Vec ⟪ A ⟫) ek (params a))
      (≺ᵥ-wf k (subst (Vec ⟪ A ⟫) ek (params a))) a qc ek refl
    where
    ihK : (b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b
    ihK b q h = accAtArity c ihC (arity b) (rk (arity b) h) b q refl

最外層はコードに沿って降り、アリティについての等式をまったく必要としない。コード c の到達可能性と、コードが c である名前が与えられると、境界 arity a で中層を呼び出し、無条件に成り立つ自然数の到達可能性を供給する。局所的な ihC がコードの到達可能性をほどき、コードが真に小さい名前はその名前自身のコードでの再帰呼び出しを得る。これは中層の正確な写しであり、一段だけ外側である。

  accAtCode : (c : Limit) → Acc _≺_ c → (a : Name) → codeOf a ≡ c → Acc _≺ₙ_ a
  accAtCode c (acc rc) a qc =
    accAtArity c ihC (arity a) (<-wellfounded (arity a)) a qc refl
    where
    ihC : (b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b

最後の定理は三層の一行の合成である。名前 a が与えられると、コード順序自身の整礎性が codeOf a の到達可能性を与え、最外層がそれを a の到達可能性へ変換する。コードの等式は反射性により成立する。こうしてすべての名前は三つの鍵による比較のもとで到達可能となり、これが狭義整列順序の整礎性の法則である。

    ihC b h = accAtCode (codeOf b) (rc (codeOf b) h) b refl

≺ₙ-wf : WellFounded _≺ₙ_
≺ₙ-wf a = accAtCode (codeOf a) (≺-wf (codeOf a)) a refl

整列順序と最小の名前

四つの法則は、名前全体が狭義整列順序を運ぶことを示す。それをその構造のレコードへまとめることで、一般の最小要素探索に渡せるようになる。この順序に探索を適用すると、単に非空な名前の族が確定した最小元へ変わる。名前を構成した目的はまさにここにある。一つの段階の上の集合の族は名前の族になり、名前の族には最小元があるからである。

レコード nameOrder は、すでに証明済みの四つの法則をフィールドごとに集める。比較そのもの、三歧性、非反射性、推移性、そして整礎性である。ここで新たに証明されるものは何もない。束の意味は、下流の構成がこの順序の組立方を知らずに狭義整列順序を消費できるようにすることにある。

nameOrder : SWO (Name)
nameOrder = record
  { _<∙_   = _≺ₙ_
  ; tri∙   = ≺ₙ-tri
  ; irr∙   = ≺ₙ-irr

最小要素探索は、名前付けの構成に必要な指示述語だけに適用される。名前が x を指示するとは、その意味値が x に等しいことであり、これは指示対象を変数の枠に、x を定数に置く等号の論理式で表示される。環境は候補となる名前に応じて変わるが、論理式は固定されている。したがって古典的降下が判定するのは、明示された論理式の充足であって、任意のホスト述語ではない。

  ; trans∙ = ≺ₙ-trans
  ; wf∙    = ≺ₙ-wf }

Denotes : S → Name → hProp (ℓ-suc ℓ)
Denotes x a = (denote a ≡ x) , setIsSet (denote a) x

definedDenotes : (x : S) → FOL.Semantics.FormulaPredicate 𝒮ᵥ Name S id (Denotes x)
definedDenotes x = FOL.Semantics.presented  (var zero ≐ con x)
  (λ a → denote a ∷ []) (λ a → refl)

leastName : (x : S) → ∥ Σ[ a ∶ Name ] ⟨ Denotes x a ⟩ ∥₁
          → Σ[ a ∶ Name ] IsLeast nameOrder (Denotes x) a
leastName x = leastOfFormula nameOrder (definedDenotes x) lem