编码单射的复合与包含

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

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

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; _≐_; _∧̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

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

open import V.Coding {ℓ} using ( pr; pr-inj )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd )

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

open import L.Ordinal {ℓ} using ( ω-ord; #∈ω )
import L.Ordinal.SquareLaw {ℓ} lem as SQ
open SQ using ( module FiniteBase )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )

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

open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro )
open import L.Coding.Model {ℓ} using ( appC; appC-adequate ) public
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-out; injAt-in; module Small )

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

open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.DefinableInjection {ℓ} lem
  using ( DefinableMap ) renaming ( module Inj to DefinableInj )

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

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Nat using ( ℕ )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )

有的证明让一对的两个分量同时变动，二元的搬运正为此服务。在两个集合的呈现类型之间，等价把函数与单射搬运过去；集合之间的路径给出这样的等价。外围层级是本章一切成员陈述所读取的载体。

open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Foundations.Equiv as Equiv
open Equiv using ( equivFun; invEq; 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 import Cubical.Functions.Logic using ( ∃[∶]-syntax )

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

open hPropStructure 𝒮ʟ 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) → ⟨ fst (g i) ∈ fst bnd ⟩
    below = smallDom I g .snd

排除有限目标

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

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

ω-limit : (γ : V ℓ) → ⟨ γ ∈ ω ⟩ → ⟨ sucV γ ∈ ω ⟩
ω-limit γ γ∈ω = PT.rec (snd (sucV γ ∈ ω)) 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) → Empty.⊥
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) → Empty.⊥
finite-excl-ω β oβ β∈ω f finj =
  PT.rec Empty.isProp⊥ go (ω-mem→numeral β β∈ω)

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

  where

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

  go : Σ[ n ∈ ℕ ] (β ≡ # n) → Empty.⊥
  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 = ⟪ fst D ⟫ × ⟪ fst C ⟫

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

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

    toC : ⟪ fst C ⟫ → S

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

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

该族把每对索引送到两个实现元素的编码有序对，共享界装置对这个族一次施用：一个可构造集合包含由 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) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst z ∈ fst C ⟩
        → ⟨ pr (fst x) (fst z) ∈ fst bnd ⟩
  below x z mx mz = subst (λ w → ⟨ w ∈ fst bnd ⟩) pa (SB.below i)
    where

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

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

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

    i : Ix
    i = fD .fst , fC .fst
    pa : fst (pw i) ≡ pr (fst x) (fst z)
    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) → ⟨ fst e ∈ fst rel ⟩
        → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] ((fst e ≡ pr (fst x) (fst y)) × ⟨ P x y ⟩) ∥₁
    out e h = PT.rec squash₁ (λ { (x , hx) → PT.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) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst y ∈ fst C ⟩ → ⟨ P x y ⟩
         → ⟨ pr (fst x) (fst y) ∈ fst rel ⟩
    into x y mx my h = subst (λ w → ⟨ w ∈ fst rel ⟩) (prʟ-fst x y)
      (subst ⟨_⟩ (sym (hasSeparationL (PairBound.bnd D C) fo .fst .snd (prʟ x y)))
        ( subst (λ w → ⟨ w ∈ fst (PairBound.bnd D C) ⟩) (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 (fst x) (fst y) ∈ fst rel ⟩ → ⟨ P x y ⟩
  pair-out x y h = PT.rec (snd (P x y))
    (λ { (x' , y' , q , h') →
      subst2 (λ a b → ⟨ P a b ⟩)
        (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .fst)))

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

        (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .snd))) h' })
    (out (prʟ x y) (subst (λ w → ⟨ w ∈ fst rel ⟩) (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 (fst x) (fst y) ∈ fst F ⟩
                  → ⟨ fst y ∈ fst E ⟩)
            (svH : ⟨ (H ∷ E ∷ []) ⊨ svAt zero ⟩)
            (dmH : ⟨ (H ∷ E ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ijH : ⟨ (H ∷ E ∷ []) ⊨ injAt zero ⟩)

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

            (ranH : (y z : S) → ⟨ pr (fst y) (fst z) ∈ fst H ⟩
                  → ⟨ fst z ∈ fst C ⟩) where

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

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

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

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

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

刻画公式只有一个存在量化，遍历中间值。其内合取两个应用原子：第一个图以中间值居取值空位、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 = PT.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 = PT.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 (fst x) (fst z) ∈ fst K ⟩
        → ∥ Σ[ y ∈ S ] (⟨ pr (fst x) (fst y) ∈ fst F ⟩
                      × ⟨ pr (fst y) (fst z) ∈ fst H ⟩) ∥₁

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

  K-out = Composite.pair-out

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

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

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

  γK : 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 →
    PT.rec (setIsSet (fst y) (fst y'))
      (λ { (w , (hf , hh)) → PT.rec (setIsSet (fst y) (fst y'))
        (λ { (w' , (hf' , hh')) →
          svAt-out zero γH svH w y y' hh

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

            (subst (λ t → ⟨ pr t (fst y') ∈ fst H ⟩)
              (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 →
    PT.rec (setIsSet (fst x) (fst x'))
      (λ { (w , (hf , hh)) → PT.rec (setIsSet (fst x) (fst x'))
        (λ { (w' , (hf' , hh')) →
          injAt-out zero γF ijF w x x' hf

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

            (subst (λ t → ⟨ pr (fst x') t ∈ fst F ⟩)
              (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 (fst x) (fst y) ∈ fst K) ⟩
        → ⟨ fst x ∈ fst D ⟩
    fwd x = PT.rec (snd (fst x ∈ fst D))
      (λ { (y , p) → PT.rec (snd (fst x ∈ fst D))

若 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) → ⟨ fst x ∈ fst D ⟩
        → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst K) ⟩
    bwd x mx = PT.rec squash₁
      (λ { (w , hf) → PT.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 (fst x) (fst z) ∈ fst K ⟩ → ⟨ fst z ∈ fst C ⟩
  ranK x z h = PT.rec (snd (fst z ∈ fst C))
    (λ { (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 ∈ fst D ⟩ → ⟨ z ∈ fst C ⟩) where

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

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

C。

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

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

      ; graph = var zero ≐ var (suc zero)
      ; defines = λ _ _ → refl
      ; only = λ _ _ _ h → Σ≡Prop (λ w → snd (isL w)) 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 : ⟪ fst D ⟫ → ⟪ fst C ⟫
    incl = Sm.small

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

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

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

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

injl-trans : (a b c : S) → InjL a b → InjL b c → InjL a c
injl-trans a b c = PT.rec2 PT.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 (fst C))
               (D : S) (D∈C : ⟨ fst D ∈ fst C ⟩) where

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

小结

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