计数无穷可构造层的工具

最后的值域条款只要求 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 仅仅断言存在模型元素 u 与 v，使得 s(i)=u、y(i)=v，且图 E 把 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 共同确立 fo 对 Wit 的充分性。

  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 γ