可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

module L.InjectionComposition {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章在 L 内部发展两种编码单射的构造，并证明一个排除。其一，两个编码单射的复合：当某个中间值 y 使 (x, y) 落在第一个图、(y, z) 落在第二个图时，复合图把 x 关联到 z。其二，集合的包含由较小集合上的恒等映射编码，其图是由相等定义的有序对集合：即满足 y = x 的那些对 (x, y)。最后，从 ω 到有限序数平方的单射不存在。

open import Cubical.HITs.PropositionalTruncation using ( rec2 )

图的性质与应用由模型语言的公式表达。每个变元空位对照一列元素读取，满足关系即结构的语义。这里有两个结构。外围层级提供集合本身；可构造结构提供图所居、被读取的载体。

外围集合的有序对由一个配对运算编码，其两个分量皆可恢复：相等的码有相等的分量。小集合带有呈现，即嵌入层级的索引类型，因此关于被呈现元素的事实可转移为关于索引的事实。可构造性是沿成员关系向下封闭的谓词：可构造集合的元素是可构造的。

四项材料支撑全章。序数 ω，连同「其元素恰为数码」的事实。数码与有限集之间的有限词典，及其抽象追逐论证。小域原理：把由可构造集合组成的任何小族界于单一层。以及 L 内部的分离，对任意复杂度的公式可用，下文的每个关系都由此从公共界中刻出。

open SQ using ( module FiniteBase )

在 L 内部，语言的应用原子在常元处读取：图施于参数后仍是公式，且该读取是忠实的。单射的三条公式条件在这些原子下各有引入与消去两种形式。编码单射还可读回为其定义域与陪域的呈现之间的真正函数。

单射的码是图连同全部四项条件：单值性、定义域上的全域性、单射性作为在定义域上读取的公式，外加以元语言陈述的值域条款。内部单射关系 InjL 仅仅地断言：这样的图连同其四项条件存在。可定义单射构造把连同定义公式一起给出的映射变成这样的码。

内部存在经命题截断来断言：陈述成立而无需选定见证，截断后的陈述只能消去到命题。空类型与自然数从两端抑住下文的有限论证。

集合之间的路径给出呈现类型之间的等价，函数与单射可沿这份等价搬运。证明单射性时，retEq e x 提供往返路径 invEq e (equivFun e x) ≡ x，从而把恢复出的原像与原来的输入等同。外围层级是本章一切成员关系陈述所读取的载体。

open import Cubical.Foundations.Equiv using ( retEq )
open import Cubical.Foundations.Univalence using ( pathToEquiv )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

层级同样地构造后继与极限：后继运算向集合添入一个元素，无穷集合 ω 收集诸数码，每个有限序数一个。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
module IS = InfinitySet {ℓ}
open IS using ( sucV; #_; ω )

呈现把索引类型与到层级的嵌入配成一对，其纤维在元素与索引之间搬运事实。取值于命题的存在量词陈述复合所用的定义域条件。

open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪ )

可构造载体以本章一切集合所居之名打开。绝对性一章带来两种读法：在可构造结构处的满足 (为本地使用而改名)，及其抬升形式，即原子在常元列表处求值。下文图的一切应用都经过这一抬升读法。

open hPropView 𝒮ʟ using ( S )

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

有限一侧打开其数码词典与抽象追逐，二者都以本章只需例示的形式陈述。

open FiniteBase using ( ω-mem→numeral; toFin; toFin-inj; fromFin; fromFin-inj )
open FiniteBase using ( module AbstractChase )

共同的可构造界

用分离刻出关系，需要候选元素落在同一个可构造集合中。共享装置接收任意小索引族 g : I → S，返回包含每个 g i 的可构造集合；稍后的 PairBound 才把它例示于由选定定义域与陪域产生的有序对。

module StageBound (I : Type ℓ) (g : I → S) where

opaque
  bnd : S
  bnd = smallDom I g .fst

读取器直接陈述界的用途：族的每个元素按外围元素读取时都属于该界。此后每个被纳入 Relation 的对都经此读取器进入该界。

  below : (i : I) → ⟨ (g i) .fst ∈ bnd .fst ⟩
  below = smallDom I g .snd

排除有限目标

后文所需的有限排除取如下形式：从 ω 到有限序数平方的单射不存在。这条路线几乎完全避开 ω 的内部成员关系。所用到的只是：ω 的每个元素仅仅地是某个数码；每个数码呈现一个有限集，且词典在两个方向上都单射；以及一条抽象追逐。给定从每个有限呈现到某个固定类型的单射、再给定从该固定类型到某个有限呈现之平方的单射，便导出从较大有限集到较小有限集的单射。

关于 ω 自身的一条事实，取其成员关系谓词所能支撑的强度：ω 的元素仅仅地是某个数码，而数码 n 的后继仍是数码，因而仍是元素。γ 与其数码的同一视沿后继搬运。

ω-limit : (γ : V ℓ) → ⟨ γ ∈ ω ⟩ → ⟨ sucV γ ∈ ω ⟩
ω-limit γ γ∈ω = rec₁ ((sucV γ ∈ ω) .snd) go (ω-mem→numeral γ γ∈ω)
  where
  go : Σ[ n ∶ ℕ ] (γ ≡ # n) → ⟨ sucV γ ∈ ω ⟩
  go (n , p) = subst (λ w → ⟨ sucV w ∈ ω ⟩) (sym p) (#∈ω (suc n))

诸数码嵌入 ω 的呈现，路线是直接的。数码 m 的呈现的一个索引指名该数码的一个元素；该数码属于 ω，而由 ω 的传递性，被指名的元素也属于 ω；取 ω 的呈现在该元素处的纤维，即得呈现它的那个 ω 呈现索引。

numeral-into-ω : (m : ℕ) → ⟪ # m ⟫ → ⟪ ω ⟫
numeral-into-ω m i = fiber ω (ω-ord .fst (member (# m) i) (#∈ω m)) .fst

嵌入是单射的。若同一数码的两个索引在 ω 的呈现中取值相等，两条纤维的同一视就把像的相等换成该数码内部被呈现元素的相等；而数码自身的呈现是单射的，故两个索引重合。

numeral-into-ω-inj : (m : ℕ) (i₁ i₂ : ⟪ # m ⟫)
                   → numeral-into-ω m i₁ ≡ numeral-into-ω m i₂ → i₁ ≡ i₂
numeral-into-ω-inj m i₁ i₂ e = ↪-inj {a = # m}
  (sym (fiber ω (ω-ord .fst (member (# m) i₁) (#∈ω m)) .snd)
    ∙ cong (⟪ ω ⟫↪) e

ω 一侧用到的单射事实只有数码呈现的单射性。

    ∙ fiber ω (ω-ord .fst (member (# m) i₂) (#∈ω m)) .snd)

追逐是元理论层面关于呈现索引类型的陈述，并非内部单射关系。其假设有二：其一，对每个数码 n，呈现类型 ⟪ # n ⟫ 与有限集 Fin n 之间在两个方向各有一个单射，各自单射；其二，每个 ⟪ # m ⟫ 都有到固定类型 ⟪ ω ⟫ 的单射。其结论：从 ⟪ ω ⟫ 到 ⟪ # n ⟫ × ⟪ # n ⟫ 的单射不可能存在。

no-inj-finite-ω : (n : ℕ) → (f : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫)
                → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → ⊥₀
no-inj-finite-ω n f finj =

抽象论证恰好消耗那两本词典与到固定类型的单射族。其核心是鸽笼计数：从 Fin (suc (n · n)) 到 Fin (n · n) 的单射不存在，而追逐把所设单射化归为恰是这一形状。

  AbstractChase.NoInj.no-inj
    (λ n → ⟪ # n ⟫)
    toFin toFin-inj
    fromFin fromFin-inj
    (⟪ ω ⟫)

本章只需交出数码的词典与到 ω 呈现的嵌入。

    (numeral-into-ω)
    (numeral-into-ω-inj)
    n f finj

该条款把排除提升到任意有限序数，且始终停留在呈现索引类型层面，保持追逐的形状：此处固定类型是 ⟪ ω ⟫，有限呈现是诸 ⟪ # n ⟫。

finite-excl-ω : (β : V ℓ) → IsOrd β → ⟨ β ∈ ω ⟩
              → (f : ⟪ ω ⟫ → ⟪ β ⟫ × ⟪ β ⟫)
              → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → ⊥₀
finite-excl-ω β oβ β∈ω f finj =
  rec₁ isProp⊥ go (ω-mem→numeral β β∈ω)

设 β 是 ω 的序数元素，并设从 ω 的呈现到 β 之呈现的平方的函数为单射；要证的是矛盾。

  where

β 属于 ω 仅仅地给出一个与 β 同一视的数码，故只需对数码情形导出反驳；截断消去到空类型，而空类型是命题。

  go : Σ[ n ∶ ℕ ] (β ≡ # n) → ⊥₀
  go (n , p) = no-inj-finite-ω n f' finj'
    where

该同一视是集合之间的路径，对路径取平方便得两个平方呈现之间的等价。所设函数与该等价复合，其单射性沿等价的单位律转移：若被搬运的函数等同了两个输入，原来的函数也会等同它们。

    e : ⟪ β ⟫ × ⟪ β ⟫ ≃ ⟪ # n ⟫ × ⟪ # n ⟫
    e = pathToEquiv (cong (λ w → ⟪ w ⟫ × ⟪ w ⟫) p)
    f' : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫
    f' x = equivFun e (f x)
    finj' : (x y : ⟪ ω ⟫) → f' x ≡ f' y → x ≡ y

于是追逐施于该数码，其矛盾正是所述鸽笼形状：从 Fin (suc (n · n)) 到 Fin (n · n) 的单射。

    finj' x y e' = finj x y
      (sym (retEq e (f x)) ∙ cong (invEq e) e' ∙ retEq e (f y))

有界有序对图所呈现的关系

L 中两个集合之间的关系将成为编码有序对组成的集合。界在任何公式出现之前就枚举了这些对：索引类型是定义域的一个呈现索引与陪域的一个呈现索引之积。

module PairBound (D C : S) where

Ix : Type ℓ
Ix = ⟪ D .fst ⟫ × ⟪ C .fst ⟫

每个呈现索引被实现为载体的元素：即那个被呈现的集合；它是可构造集合 D 或 C 的元素，可构造性沿成员关系向下搬运。

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

  toC : ⟪ C .fst ⟫ → S

每一侧各为每个索引产生一个 L 元素。

  toC k = ⟪ C .fst ⟫↪ k
        , isL-trans {x = C .fst} {y = ⟪ C .fst ⟫↪ k} (member (C .fst) k) (C .snd)

该族把每对索引送到两个实现元素的编码有序对，共享界装置对这个族一次施用：一个可构造集合包含由 D 与 C 可能产生的一切编码对。

  pw : Ix → S
  pw (m , k) = prʟ (toD m) (toC k)

  module SB = StageBound Ix pw

界从该装置读出，此后只通过成员关系使用；下文无需其构造。

bnd : S
bnd = SB.bnd

读取器把界扩展到呈现之外：对 D 的任意元素 x 与 C 的任意元素 z，即便不由索引给出，其编码对仍在界内。此后每个构造触及界用的都是这个形式。

below : (x z : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩
      → ⟨ pr (x .fst) (z .fst) ∈ bnd .fst ⟩
below x z mx mz = subst (λ w → ⟨ w ∈ bnd .fst ⟩) pa (SB.below i)
  where

由于 D 与 C 是被呈现的，两个元素各有纤维：一个索引，其被呈现集合与该元素被等同。两条纤维各自独立取得。

  fD : Σ[ m ∶ ⟪ D .fst ⟫ ] (⟪ D .fst ⟫↪ m ≡ x .fst)
  fD = fiber (D .fst) mx
  fC : Σ[ k ∶ ⟪ C .fst ⟫ ] (⟪ C .fst ⟫↪ k ≡ z .fst)
  fC = fiber (C .fst) mz

两个索引构成界的族的一个索引，族在该索引处的取值是被呈现元素们的编码对，沿两条纤维路径它等于 x 与 z 的编码对。沿该相等搬运成员关系，读取器即告完成。

  i : Ix
  i = fD .fst , fC .fst
  pa : (pw i) .fst ≡ pr (x .fst) (z .fst)
  pa = prʟ-fst (toD (fD .fst)) (toC (fC .fst))
     ∙ cong₂ pr (fD .snd) (fC .snd)

从界中刻出关系需要三份数据：一个三空位公式，以及定义在有序对上的宿主谓词 P，连同两个方向的充分性。公式的读取次序是值、索引、对：在环境 y ∷ x ∷ e 下，该公式被读作 P x y。

module Relation (D C : S) (φ : Formula S 3) (P : S → S → hProp (ℓ-suc ℓ))
                (read : (x y e : S) → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩ → ⟨ P x y ⟩)
                (fill : (x y e : S) → ⟨ P x y ⟩ → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩) where

刻画公式对两个空位作存在量化，并且除给定公式外，还在对象语言中断言第三空位编码前两者的有序对。共享界上的分离施于这个单空位公式，返回作为 L 元素的关系。

opaque
  fo : Formula S 1
  fo = ∃̇ (∃̇ (prAtL (suc (suc zero)) (suc zero) zero ∧̇ φ))

  rel : S
  rel = hasSeparationL (PairBound.bnd D C) fo .fst .fst

反向读取把成员关系换成关于某一对的截断数据。关系的元素 e 由分离规格满足刻画公式；两层存在量化解开得到分量 x、y，以及「e 编码其对子」的证明，经充分性恢复为编码运算自身的形式，而公式部分被读成 P x y。

  out : (e : S) → ⟨ e .fst ∈ rel .fst ⟩
      → ∥ Σ[ x ∶ S ] Σ[ y ∶ S ] ((e .fst ≡ pr (x .fst) (y .fst)) × ⟨ P x y ⟩) ∥₁
  out e h = rec₁ squash₁ (λ { (x , hx) → map₁
    (λ { (y , q , hy) → x , y
       , subst ⟨_⟩ (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ e ∷ [])) q

一切都是截断的，与该关系日后被消耗的形式一致。

       , read x y e hy }) hx })
    (subst ⟨_⟩ (hasSeparationL (PairBound.bnd D C) fo .fst .snd e) h .snd)

正向由谓词构造成员关系。

  into : (x y : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ y .fst ∈ C .fst ⟩ → ⟨ P x y ⟩
       → ⟨ pr (x .fst) (y .fst) ∈ rel .fst ⟩
  into x y mx my h = subst (λ w → ⟨ w ∈ rel .fst ⟩) (prʟ-fst x y)
    (subst ⟨_⟩ (sym (hasSeparationL (PairBound.bnd D C) fo .fst .snd (prʟ x y)))
      ( subst (λ w → ⟨ w ∈ (PairBound.bnd D C) .fst ⟩) (sym (prʟ-fst x y))

x 与 y 的编码对由界的读取器进入共享界；公式的编码条款由编码运算的计算成立，给定公式由充分性成立；分离给出成员关系，并沿编码的定义性相等搬运。

          (PairBound.below D C x y mx my)
      , ∣ x , ∣ y
        , subst ⟨_⟩ (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ prʟ x y ∷ [])))
            (prʟ-fst x y)
        , fill x y (prʟ x y) h ∣₁ ∣₁ ))

对 x 与 y 的真实编码对，反向读取可锐化为非截断的结论。

pair-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ rel .fst ⟩ → ⟨ P x y ⟩
pair-out x y h = rec₁ ((P x y) .snd)
  (λ { (x' , y' , q , h') →
    subst2 (λ a b → ⟨ P a b ⟩)
      (Σ≡Prop (λ v → (isL v) .snd) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .fst)))

其见证把 e 呈现为某对 x'、y' 的编码对；编码的单射性把 x' 的底层元素等同于 x 的底层元素、y' 的等同于 y 的；又因可构造性是命题，这些底层等式提升为载体元素的等式。谓词随即被恰好搬到 P x y。

      (Σ≡Prop (λ v → (isL v) .snd) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .snd))) h' })
  (out (prʟ x y) (subst (λ w → ⟨ w ∈ rel .fst ⟩) (sym (prʟ-fst x y)) h))

复合编码单射

第一个的陪域是第二个的定义域时，两个编码单射可以复合。复合物仍是图，其验证从不重跑替换：两个输入图已作为集合存在，复合物只是从共享界内分离出的一个关系。模块收取两个图，以及各自的三条读取条件。

module Comp (D E C F H : S)
            (svF : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
            (dmF : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ijF : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩)
            (ranF : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩
                  → ⟨ y .fst ∈ E .fst ⟩)
            (svH : ⟨ (H ∷ E ∷ []) ⊨ svAt zero ⟩)
            (dmH : ⟨ (H ∷ E ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ijH : ⟨ (H ∷ E ∷ []) ⊨ injAt zero ⟩)
            (ranH : (y z : S) → ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩
                  → ⟨ z .fst ∈ C .fst ⟩) where

除三条读取条件外，每个图还以模块的独立假设携带值域条款：第一个图的每个编码对的取值落在中间集合，第二个图的每个编码对的取值落在最终陪域。

这两条条款以元语言陈述，而非公式。

每个「码与定义域」的对，正是三条公式条件所需的两槽环境：槽 0 放图，槽 1 放定义域。每个图一个环境。

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

  γH : Vec S 2
  γH = H ∷ E ∷ []

连接关系说：当对象语言能产生中间值 y，使 (x, y) 在第一个图中、(y, z) 在第二个图中时，x 与 z 相关。它的截断继承自存在量词的语义：量词取值于命题，公式的满足只带有量化器内建截断意义上的见证。

private
  Chain : S → S → Type (ℓ-suc ℓ)
  Chain x z = ∥ Σ[ y ∶ S ] (⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩
                           × ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩) ∥₁

刻画公式只有一个存在量化，遍历中间值。其内合取两个应用原子：第一个图以中间值居取值空位、x 居索引空位读取，第二个图以 z 居取值空位、中间值居索引空位读取。这正是 (x, y) ∈ F 与 (y, z) ∈ H 的对象语言形状。

  opaque
    body : Formula S 3
    body = ∃̇ (appC F (suc (suc zero)) zero ∧̇ appC H zero (suc zero))

应用原子的充分性把每个合取项搬到其本意的成员关系：第一个搬到第一个图在 (x, y) 处的成员关系，第二个搬到第二个图在 (y, z) 处的成员关系。剩下的恰是截断形式的连接见证。

    read : (x z p : S) → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩ → Chain x z
    read x z p = map₁ (λ { (y , hf , hh) → y
      , subst ⟨_⟩ (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ [])) hf
      , subst ⟨_⟩ (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ [])) hh })

逆向把连接见证沿同一条充分性的反向搬回对象语言。两个方向合起来说：公式与连接关系互相表达。

    fill : (x z p : S) → Chain x z → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩
    fill x z p = map₁ (λ { (y , hf , hh) → y
      , subst ⟨_⟩ (sym (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ []))) hf
      , subst ⟨_⟩ (sym (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ []))) hh })

有界关系装置被例示一次，宿主谓词取为连接关系；下文一切都从这个唯一实例读出。

  module Composite = Relation D C body (λ x z → Chain x z , squash₁) read fill

复合图就是那个分离出的关系。

K : S
K = Composite.rel

K-out : (x z : S) → ⟨ pr (x .fst) (z .fst) ∈ K .fst ⟩
      → ∥ Σ[ y ∶ S ] (⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩
                    × ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩) ∥₁

其反向读取原样继承：复合物中的一个编码对仅仅地给出中间值 y，使 (x, y) 在第一个图、(y, z) 在第二个图。下文四项验证都由这一条读取驱动。

K-out = Composite.pair-out

正向读取即复合律：给定中间值 y，使两对分别落在两个图中，把截断的见证交给装置，装置便把 x 与 z 的编码对放进复合物。

K-in : (x y z : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩
     → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩
     → ⟨ pr (x .fst) (z .fst) ∈ K .fst ⟩
K-in x y z mx mz hf hh = Composite.into x z mx mz ∣ y , hf , hh ∣₁

复合物现在必须以其自身资格满足四项条件，环境把复合图与第一个定义域配对。先证单值性。

γK : Vec S 2
γK = K ∷ D ∷ []

svK : ⟨ γK ⊨ svAt zero ⟩

设复合把 x 与两个值 y、y' 配对。拆开两个截断的连接得中间值 w 与 w'，(x, w) 与 (x, w') 在第一个图中。

svK = svAt-in zero γK (λ x y y' p q →
  rec₁ (setIsSet (y .fst) (y' .fst))
    (λ { (w , (hf , hh)) → rec₁ (setIsSet (y .fst) (y' .fst))
      (λ { (w' , (hf' , hh')) →
        svAt-out zero γH svH w y y' hh

第一个图的单值性等同 w 与 w'；该同一视被搬入第二个图的对子，其单值性随即等同 y 与 y'。目标是 h-集合中的路径，因而是命题，故两次截断消去都合法。

          (subst (λ t → ⟨ pr t (y' .fst) ∈ H .fst ⟩)
            (sym (svAt-out zero γF svF x w w' hf hf')) hh') })
      (K-out x y' q) })
    (K-out x y p))

接着验证单射性，且两个图的使用次序重要：先用第二个图的单射性，再用第一个图的。

ijK : ⟨ γK ⊨ injAt zero ⟩

设复合把 x 与 x' 都映到 y。两个截断的连接给出中间值 w 与 w'：(x, w) 与 (x', w') 在第一个图中，而 (w, y) 与 (w', y) 都在第二个图中。

ijK = injAt-in zero γK (λ y x x' p q →
  rec₁ (setIsSet (x .fst) (x' .fst))
    (λ { (w , (hf , hh)) → rec₁ (setIsSet (x .fst) (x' .fst))
      (λ { (w' , (hf' , hh')) →
        injAt-out zero γF ijF w x x' hf

第二个图在公共值 y 处的单射性等同 w 与 w'；第一个图在此时公共的中间值处的单射性等同 x 与 x'。

          (subst (λ t → ⟨ pr (x' .fst) t ∈ F .fst ⟩)
            (sym (injAt-out zero γH ijH y w w' hh hh')) hf') })
      (K-out x' y q) })
    (K-out x y p))

复合在定义域上的全域性是一条等价：x 属于第一个定义域，当且仅当它有复合取值。两个方向一并交给引入形式。

dmK : ⟨ γK ⊨ domAt zero (suc zero) ⟩
dmK = domAt-intro zero (suc zero) γK (λ x → fwd x , bwd x)

一个方向直接消去第一个图的定义域条件。

  where
  fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (x .fst) (y .fst) ∈ K .fst) ⟩
      → ⟨ x .fst ∈ D .fst ⟩
  fwd x = rec₁ ((x .fst ∈ D .fst) .snd)
    (λ { (y , p) → rec₁ ((x .fst ∈ D .fst) .snd)

若 x 有复合取值，连接见证给出中间值 w，使 (x, w) 在第一个图中；把定义域原子自身的消去施于该对，即将 x 放入 D。这个方向用不到第二个图。

      (λ { (w , (hf , _)) → domAt-out zero (suc zero) γF dmF x w hf })
      (K-out x y p) })

另一方向串起两条引入。给定 D 中的 x，第一个图的定义域引入给出中间值 w，使 (x, w) 在第一个图中，其值域条款把 w 放入中间集。

  bwd : (x : S) → ⟨ x .fst ∈ D .fst ⟩
      → ⟨ ∃[ y ∶ S ] (pr (x .fst) (y .fst) ∈ K .fst) ⟩
  bwd x mx = rec₁ squash₁
    (λ { (w , hf) → rec₁ squash₁
      (λ { (z , hh) → ∣ z , K-in x w z mx (ranH w z hh) hf hh ∣₁ })

第二个图的定义域引入在 w 处产出 z，使 (w, z) 在第二个图中；第二个图的值域条款把 z 放入 C；复合律把 x 与 z 的对放进复合物。两步都是截断的，结论亦然。

      (domAt-in zero (suc zero) γH dmH w (ranF x w hf)) })
    (domAt-in zero (suc zero) γF dmF x mx)

值域条件是第二个图的值域条款在中间值处的应用。拆开复合对得到连接见证；其第二分量在第二个图内把中间值与 z 配对，条款随即将 z 放入 C。

ranK : (x z : S) → ⟨ pr (x .fst) (z .fst) ∈ K .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩
ranK x z h = rec₁ ((z .fst ∈ C .fst) .snd)
  (λ { (w , (_ , hh)) → ranH w z hh }) (K-out x z h)

三条读取条件连同值域条款，恰是「编码单射可读回为呈现之间的函数」所需。因此复合物也承认这一读取；该模块私下承载它：公开传递出去的只是图与其四项条件，这一读取所需不外乎此。

private module Sm = Small K D C svK dmK ijK ranK

符号化包含

包含不需要新的构造：当 D 包含于 C 时，D 上的恒等映射本来就是到 C 的映射。被编码的是这个映射的图，它在对象语言中写作取值空位与索引空位之间的相等。模块收取两个集合与逐点的包含。

module InclGraph (D C : S)
                 (sub : (z : V ℓ) → ⟨ z ∈ D .fst ⟩ → ⟨ z ∈ C .fst ⟩) where

可定义映射记录由定义域上的恒等填成：函数把每个元素送到自身，逐点包含证明每个取值落入

private
  M : DefinableMap
  M = record
    { dom = D ; cod = C
    ; fn = λ x _ → x

C。

    ; into = λ x mx → sub (x .fst) mx

图公式是两个空位之间的相等，它对函数自身取值成立是定义性的。解的唯一性用的是等式的底层等式：任何解都满足该等式，而那是底层元素之间的相等；又因可构造性是命题，这个底层等式提升为载体元素的等式。排除「与函数取值无关的解」靠的正是这一点。

    ; graph = var zero ≐ var (suc zero)
    ; defines = λ _ _ → refl
    ; only = λ _ _ _ h → Σ≡Prop (λ w → (isL w) .snd) h }

共享构造把该映射变成带三条读取条件的图，但它要从外部收取底层函数为单射的证明。对恒等映射而言这是直接的：该假设等同两个输入的像，而在恒等映射下像的相等就是输入的相等，故所提供的、把等式原样返回的延续恰是所需的证明。

  module I = DefinableInj M (λ _ _ _ _ e → e)
    using ( F; code )

opaque
  G : S
  G = I.F

图连同全部四项条件一并作为从 D 到 C 的单射之码交付；使用者把整个包当作一个单元接收，无需打开。

opaque
  unfolding G
  code : InjCode G D C
  code = I.code

同一个图经共享读取被读回为 D 与 C 的呈现之间的函数。这一读取由一个私有的模块承载：公开传递出去的结果只是图与其四项条件，而这正是该读取所需的全部。

private module Sm = Small G D C (code .fst) (code .snd .fst)
          (code .snd .snd .fst) (code .snd .snd .snd)

导出的函数名为 incl，其路线值得注意。D 呈现的一个索引指名一个底层元素，该元素属于 D，因而由包含属于 C。函数随后取 C 自身呈现在该元素处的纤维：即呈现它的那个 C 索引。索引不是被直接搬运的，而是经由元素与纤维找回。

opaque
  incl : ⟪ D .fst ⟫ → ⟪ C .fst ⟫
  incl = Sm.small

内部存在层面的包含与复合

至此的构造产出图；而内部单射关系只要求某个图存在。提升是直接的：包含给出恒等图作为见证，断言在其外围截断。包含进入基数论证所用的正是这一形式。

inclusion-coded : (a b : S)
                → ((z : V ℓ) → ⟨ z ∈ a .fst ⟩ → ⟨ z ∈ b .fst ⟩)
                → InjL a b
inclusion-coded a b sub = ∣ I.G , I.code ∣₁
  where module I = InclGraph a b sub

复合同样提升：rec2 在局部分支中展开两个见证，构造其复合，再次截断结果，而不作代表的全局选择。

injl-trans : (a b c : S) → InjL a b → InjL b c → InjL a c
injl-trans a b c = rec2 squash₁ step
  where

双重消去局部地拆开两个见证，用已验证的构造组装复合物，再把结果重新截断。它不作任何全局的代表选择：两个见证只作为构造的假设存在，从不被保留。

  step : Σ[ F ∶ S ] InjCode F a b
       → Σ[ H ∶ S ] InjCode H b c
       → InjL a c
  step (F , svF , dmF , ijF , ranF) (H , svH , dmH , ijH , ranH) =
    ∣ K.K , (K.svK , K.dmK , K.ijK , K.ranK) ∣₁

复合模块承载全部验证，因此在这个层面，复合律只有一行。

    where
    module K = Comp a b c F H svF dmF ijF ranF svH dmH ijH ranH

主要实例从序数 C 的元素 D 出发。唯一的假设是 D 属于序数 C；C 的传递性随即断言 D 的每个元素都是 C 的元素，而这正是编码所需的逐点包含。模块对这一对打开包含构造，于是其图、码与导出映射都在同一个名字下可用。

module OrdIncl (C : S) (oC : IsOrd (C .fst))
               (D : S) (D∈C : ⟨ D .fst ∈ C .fst ⟩) where

open InclGraph D C (λ _ z∈D → oC .fst z∈D D∈C) public

小结

三项结果服务于内部基数论证。有限排除表明从 ω 到任何有限序数平方的单射不存在：ω 的元素仅仅地是数码，呈现类型 ⟪ # n ⟫ 与有限集 Fin n 在两个方向上各有一个单射，若假设存在到某个有限平方的单射，抽象追逐便导出从较大有限集到较小有限集的单射。复合把两个编码单射变成一个，经连接关系核验单值性、定义域上的全域性、单射性与值域条款。包含由恒等图把逐点包含编码为单射。在存在层面，两种操作都提升到截断的内部关系，因此基数界限的构造与比较完全可以经由居于 L 内部的图进行。