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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

private

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    final : y .fst ≡ y₀ .fst

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

D : DefinableMap
D = record
  { dom = seqL A ; cod = seqL B ; fn = fn ; into = into ; graph = fo
  ; defines = λ s m → T.funct s m .fst .snd
  ; only    = λ s m y h → sym (T.val-uniq s m y h) }

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

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

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

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

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

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

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

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

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

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

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

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

private
  F A : S
  F = lookup f γ
  A = lookup B γ