编码单射

private
  Holds₀ : S → S → Type (ℓ-suc ℓ)
  Holds₀ x y = ⟨ pr (x .fst) (y .fst) ∈ (lookup f γ) .fst ⟩

  at₁ : (y x x' : S)

路径 at₁ 记录第一条应用条款在扩张赋值 x' ∷ x ∷ y ∷ γ 处的充分性：那里的满足被等同于对 (x, y) 属于图的投影事实。这一等同是命题之间的相等，由 appAt-adequate 在所给变元索引处给出，因此可以向两个方向运输。

      → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)))
      ≡ (pr (x .fst) (y .fst) ∈ (lookup f γ) .fst)
  at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero))
                 (x' ∷ x ∷ y ∷ γ)

  at₂ : (y x x' : S)

路径 at₂ 是另一条条款的同样陈述：变元 0 与 2 处的应用的满足等同于 (x', y) 属于图的投影事实。两条路径只在对码中输入哪个第一分量上不同，而这正是单射性所利用的不对称。

      → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero)))
      ≡ (pr (x' .fst) (y .fst) ∈ (lookup f γ) .fst)
  at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero))
                 (x' ∷ x ∷ y ∷ γ)

injAt-out : ⟨ γ ⊨ injAt f ⟩

向外的方向 injAt-out 从公式在 γ 处成立的证明与两个成员关系事实 Holds₀ x y、Holds₀ x' y 出发。把三个量词实例化，得到含取式体在扩张赋值处的满足证明；再把成员关系事实沿 at₁、at₂ 的反向运输，变成两条前件条款的满足证明。最后的 x .fst ≡ x' .fst 在模型的相等中读出。

          → (y x x' : S) → Holds₀ x y → Holds₀ x' y → x .fst ≡ x' .fst
injAt-out h y x x' p q = h y x x'
  (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q)

injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → x .fst ≡ x' .fst)
         → ⟨ γ ⊨ injAt f ⟩

向内的方向 injAt-in 沿同样的路径正向运输：把投影的单射性质作为关于 Holds₀ 的假设，沿 at₁、at₂ 本身运输两个成员关系事实，得到两条前件的满足，假设随后给出公式结论所需的等式。两个方向合起来说明：该公式对单射性是充分的，既不强也不弱。

injAt-in h y x x' p q = h y x x'
  (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q)

γ : Vec S 
γ = F ∷ D ∷ []

Holds x y 是底层对属于底层图的投影成员关系。原像 Fib x 把一个输出 y 与这样的证明配成一对；它的元素就是图在 x 处的候选值，每个候选都带着「它确实是取值」的证书。

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

Fib : S → Type (ℓ-suc ℓ)
Fib x = Σ[ y ∶ S ] Holds x y

isPropFib : (x : S) → isProp (Fib x)

要证明 Fib x 是命题，比较 (y,p) 与 (y′,q)。单值性先给出路径 y .fst ≡ y′ .fst。内层 Σ≡Prop 利用 S 元素的第二分量即 isL 证书为命题，把该路径提升为 y ≡ y′；外层 Σ≡Prop 再利用图成员关系证明为命题，把这一相等提升为 Fib x 的两个元素相等。这是两个不同的证明无关性步骤，并不是说周遭集合的相等仅由可构造性推出。

isPropFib x (y , p) (y' , q) =
  Σ≡Prop (λ w → (pr (x .fst) (w .fst) ∈ F .fst) .snd)
    (Σ≡Prop (λ z → (isL z) .snd) (svAt-out zero γ sv x y y' p q))

toVal : (x : S) → ∥ Fib x ∥₁ → Fib x
toVal x = rec₁ (isPropFib x) (λ z → z)

由于 Fib x 是命题，toVal 能把取值的截断存在 ∥ Fib x ∥₁ 消去为实际的原像。选择似乎藏在这里，其实没有：命题截断可以消去到任何命题值的目标，既不需要排中律也不需要选典范代表。定义域 Dom 把输入与其属于 D 的投影证明打包，fib 把由 domAt-in 得到的每个输入的截断像送入 toVal。

Dom : Type (ℓ-suc ℓ)
Dom = Σ[ x ∶ S ] ⟨ x .fst ∈ D .fst ⟩

fib : (u : Dom) → Fib (u .fst)
fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m)

toFun : Dom → S

函数 toFun 把定义域元素送到其唯一原像中的输出 y : S。它只舍去随附的图成员关系证明；输出仍是模型元素，因此保留其可构造性证书。定理 toFun-graph 恰把这份被舍去的成员关系证据作为原像的第二分量取回。

toFun u = (fib u) .fst

toFun-graph : (u : Dom) → Holds (u .fst) (toFun u)
toFun-graph u = (fib u) .snd

module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where

toFun-inj : (u v : Dom) → (toFun u) .fst ≡ (toFun v) .fst

          → (u .fst) .fst ≡ (v .fst) .fst
toFun-inj u v e = injAt-out zero γ ij (toFun v) (u .fst) (v .fst)
  (subst (λ w → ⟨ pr ((u .fst) .fst) w ∈ F .fst ⟩) e (toFun-graph u))
  (toFun-graph v)

内层模块以 F、D 与前两个满足证明重新打开 Extract，于是上一节的所有构造都以带前缀的名字可用。接着 toS 把 D 的典范呈现的一个索引 m 变成模型元素。第一分量就是被呈现的集合本身；第二分量是其可构造性证书，由 isL-trans 从显式成员关系 member (D .fst) m 与 D 自身可构造的证书得出。传递性正是所需的原理：可构造集合的元素是可构造的。

module E = Extract F D sv dm

toS : ⟪ D .fst ⟫ → S
toS m = ⟪ D .fst ⟫↪ m
      , isL-trans {x = D .fst} {y = ⟪ D .fst ⟫↪ m} (member (D .fst) m) (D .snd)

每个小索引还须被看作 Extract 意义下定义域的元素，at 提供这一对：模型元素 toS m 连同显式成员关系证明 member (D .fst) m。把 at m 经 E.toFun 喂给图得到一个取值，取值假设证书化该值属于 C。由于典范呈现中的成员关系 ⟪ C .fst ⟫↪ k ≡ (E.toFun (at m)) .fst 是具有命题值原像的嵌入的原像，fiber 返回的是实际的索引 k 连同一条路径，而非仅仅是截断的存在。

at : ⟪ D .fst ⟫ → E.Dom
at m = toS m , member (D .fst) m

fib : (m : ⟪ D .fst ⟫)
    → Σ[ k ∶ ⟪ C .fst ⟫ ] (⟪ C .fst ⟫↪ k ≡ (E.toFun (at m)) .fst)
fib m = fiber (C .fst)

舍去路径便得到 small：从 D 的索引类型到 C 的索引类型的函数。每个定义域索引被送到「在图下的像」所对应的索引。至此两种表示会合：small 是固定宇宙层级上类型之间的映射，正是计数论证所需的形状，而它经由保留的路径与图联系在一起。

  (ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m)))

small : ⟪ D .fst ⟫ → ⟪ C .fst ⟫
small m = (fib m) .fst

small-inj : (m n : ⟪ D .fst ⟫) → small m ≡ small n → m ≡ n
small-inj m n e = ↪-inj {a = D .fst} {m = m} {n = n}

small 的单射性由索引的相等沿呈现往返证得。由 small m ≡ small n，反向取 (fib m) .snd 得到 m 处的呈现值，嵌入下的同余把相等传过去，(fib n) .snd 落到 n 处的呈现值；三条路径按这个确切方向拼接，使两个输出的底层集合相等。Extract 的单射性随之给出两个输入的底层集合相等，而 ↪-inj，即定义域呈现嵌入在索引上的单射性，最终给出 m ≡ n。这里有两个不同的单射性事实在起作用，一个关于图，一个关于典范嵌入，二者不可互相替代。

  (E.toFun-inj ij (at m) (at n)
    (sym ((fib m) .snd) ∙ cong ⟪ C .fst ⟫↪ e ∙ (fib n) .snd))