setmath.tex

\chapter{集合论 (Set theory)}
\label{cha:set-math}

\index{集合|(set|(}%

我们将集合理解为具有特别简单的同伦特征的类型，参见\cref{sec:basics-sets}。这种理解与Zermelo--Fraenkel\index{集合论!Zermelo--Fraenkel(set theory!Zermelo--Fraenkel)}集合论中的集合完全不同，后者形成了一个包含复杂嵌套隶属关系的累积层次结构。对于许多数学目的，同伦理论中的集合与Zermelo--Fraenkel集合一样好用，但它们之间存在重要差异。

我们在本章开始于\cref{sec:piw-pretopos}，展示了范畴$\uset$具有通常集合范畴的（大部分）性质。
\index{数学!构造性(mathematics!constructive)}%
\index{数学!预测性(mathematics!predicative)}%
在构造性、预测性、单值性基础上，它是一个``$\Pi\mathsf{W}$-前拓扑（pretopos）''；而如果我们假设命题的缩放
\index{命题!缩放(propositional!resizing)}%
(\cref{subsec:prop-subsets})，它是一个初等拓扑（elementary topos）\index{拓扑(topos)}，如果我们假设\LEM{}和\choice{}，那么它是Lawvere的\emph{集合范畴的初等理论}的模型\index{Lawvere}。
\index{集合范畴的初等理论(Elementary Theory of the Category of Sets)}%
这足以确保在同伦类型论中的集合行为类似于大多数数学家在集合论之外使用的集合。

在本章的其余部分，我们研究了一些传统上属于“集合论”的主题。在\cref{sec:cardinals,sec:ordinals,sec:wellorderings}中，我们研究了基数和序数。这些通常在集合论中使用全局隶属关系来定义，但我们将看到，单值性公理使得一种同样方便、更具“结构性”的方法成为可能。

最后，在\cref{sec:cumulative-hierarchy}中，我们考虑在同伦类型论内部构建一个具有二元隶属关系的类似于Zermelo--Fraenkel集合论的累积层次结构的可能性。这结合了高阶归纳类型与代数集合论领域的思想。
\index{代数集合论(algebraic set theory)}%
\index{集合论!代数(algebraic)}%

在本章中，我们将经常使用\cref{subsec:prop-trunc}中描述的传统逻辑符号。除了\cref{cha:basics,cha:logic}的基本理论外，我们还使用了\cref{sec:colimits,sec:set-quotients}中关于余极限和商集的高阶归纳类型，以及\cref{cha:hlevels}中关于截断的某些理论，特别是在\cref{sec:image-factorization}中提到的因子分解系统在$n=-1$的情况。在\cref{sec:ordinals}中，我们使用了一个归纳族(\cref{sec:generalizations})来描述良序性，在\cref{sec:cumulative-hierarchy}中，我们使用了一个更复杂的高阶归纳类型来呈现累积层次结构。


\section{集合范畴 (The category of sets)}
\label{sec:piw-pretopos}

回顾在\cref{cha:category-theory}中，我们定义了范畴\uset由所有$0$-类型（在某个宇宙\UU中）及其之间的映射组成，并且观察到它是一个范畴（不仅仅是一个预范畴）。我们将依次考虑\uset所具有的结构层次。

\subsection{极限和余极限 (Limits and colimits)}
\label{subsec:limits-sets}

\index{极限!集合的(limit!of sets)}%
\index{余极限!集合的(colimit!of sets)}%

由于集合在积下是封闭的，\cref{thm:prod-ump}中的积的泛性质立即表明\uset具有有限积。实际上，无穷积也同样容易从等价式中得出：
\[ \Parens{X\to \prd{a:A} B(a)} \eqvsym \Parens{\prd{a:A} (X\to B(a))}.\]
我们在\cref{ex:pullback}中看到，$f:A\to C$和$g:B\to C$的拉回可以定义为$\sm{a:A}{b:B} f(a)=g(b)$；如果$A,B,C$都是集合，则它是一个集合并继承了正确的泛性质。因此，\uset在显然的意义上是一个\emph{完备}范畴。
\index{范畴!完备的(category!complete)}%
\index{完备!范畴(complete!category)}%

由于集合在$+$下是封闭的并包含\emptyt，\uset具有有限余积。同样，由于$\sm{a:A}B(a)$是一个集合，当且仅当$A$和每个$B(a)$是集合时，它在\uset中产生了族$B$的余积。最后，我们在\cref{sec:pushouts}中证明了$n$-类型中的推出存在，这特别包括了\uset。因此，\uset也是\emph{余完备的}。
\index{范畴!余完备的(category!cocomplete)}%
\index{余完备范畴(cocomplete category)}%

\subsection{像 (Images)}
\label{sec:image}

接下来，我们展示\uset是一个\define{正则范畴 (regular category)}，即：
\indexdef{范畴!正则的(category!regular)}%
\indexdef{正则!范畴(regular!category)}%
%
\begin{enumerate}
  \item \uset是有限完备的。\label{item:reg1}
  \item 任何函数$f : A \to B$的核对偶$\proj1,\proj2: (\sm{x,y:A} f(x)= f(y)) \to A$具有余等化子。\label{item:reg2}
  \indexdef{核!对偶(kernel!pair)}
  \item 正则满态射的拉回再次是正则满态射。\label{item:reg3}
\end{enumerate}
%
回想一个\define{正则满态射 (regular epimorphism)}
\indexdef{满态射!正则的(epimorphism!regular)}%
\indexdef{正则!满态射(regular!epimorphism)}%
是某对映射的余等化子。因此在\ref{item:reg3}中，余等化子的拉回需要再次是余等化子，但不一定是被拉回对偶的。

\index{集合余等化子(set-coequalizer)}%
\index{像(image)}%
$f:A\to B$的核对偶的余等化子的明显候选者是$f$的\emph{像}，如\cref{sec:image-factorization}中定义的那样。回想我们定义了$\im(f)\defeq \sm{b:B} \brck{\hfib f b}$，并且定义了$\tilde{f}:A\to\im(f)$和$i_f:\im(f)\to B$，如下所示：
\begin{align*}
  \tilde{f} & \defeq \lam{a} \Pairr{f(a),\,\bproj{\pairr{a,\refl{f(a)}}}}\\
  i_f & \defeq \proj1
\end{align*}
它们构成了一个图：
\begin{equation*}
  \xymatrix{
    **[l]{\sm{x,y:A} f(x)= f(y)}
    \ar@<0.25em>[r]^{\proj1}
    \ar@<-0.25em>[r]_{\proj2}
    &
      {A}
    \ar[r]^(0.4){\tilde{f}}
    \ar[rd]_{f}
    &
      {\im(f)}
    \ar@{..>}[d]^{i_f}
    \\ & &
    B
  }
\end{equation*}

回想一个函数$f:A\to B$称为\emph{满射 (surjective)}，如果
\index{函数!满射(function!surjective)}%
\narrowequation{\fall{b:B}\brck{\hfib f b},}
或者等价地$\fall{b:B} \exis{a:A} f(a)=b$。我们还说过，两个集合之间的函数$f:A\to B$称为\emph{单射 (injective)}，如果
\index{函数!单射(function!injective)}%
$\fall{a,a':A} (f(a) = f(a')) \Rightarrow (a=a')$，或者等价地，如果它的每个纤维是一个简单命题。由于这些是在\cref{cha:hlevels}意义上的$(-1)$-连通和$(-1)$-截断映射，一般理论表明，上述$\tilde f$是满射而$i_f$是单射，并且这种因子分解在拉回下是稳定的。

我们现在将单射性和满射性与适当的范畴理论概念进行比较。首先我们观察到范畴中的单态射和满态射有一个略微更强的等价公式。

\begin{lem}\label{thm:mono}
对于范畴$A$中的一个态射$f:\hom_A(a,b)$，以下条件是等价的。
\begin{enumerate}
  \item $f$是一个\define{单态射 (monomorphism)}：
  \indexdef{单态射(monomorphism)}%
  对于所有$x:A$和${g,h:\hom_A(x,a)}$，如果$f\circ g = f\circ h$，则$g=h$。\label{item:mono1}
  \item （如果$A$有拉回）对角线映射$a\to a\times_b a$是一个同构。\label{item:mono4}
  \item 对于所有$x:A$和$k:\hom_A(x,b)$，类型$\sm{h:\hom_A(x,a)} (k = f\circ h)$是一个简单命题。\label{item:mono2}
  \item 对于所有$x:A$和${g:\hom_A(x,a)}$，类型$\sm{h:\hom_A(x,a)} (f\circ g = f\circ h)$是一个收缩的。\label{item:mono3}
\end{enumerate}
\end{lem}
\begin{proof}
  条件~\ref{item:mono1}和~\ref{item:mono4}的等价性是标准范畴论。现在考虑$\hom_A(x,a)$和$\hom_A(x,b)$之间的函数$(f\circ \blank )$。条件~\ref{item:mono1}表示它是单射，而~\ref{item:mono2}表示它的纤维是简单命题；因此它们是等价的。~\ref{item:mono2}通过取$k\defeq f\circ g$并记住被占用的简单命题是收缩的来隐含~\ref{item:mono3}。最后，~\ref{item:mono3}隐含~\ref{item:mono1}，因为如果$p:f\circ g= f\circ h$，那么$(g,\refl{})$和$(h,p)$都包含在~\ref{item:mono3}中的类型中，因此是相等的，所以$g=h$。
\end{proof}

\begin{lem}\label{thm:inj-mono}
集合之间的一个函数$f:A\to B$是单射的当且仅当它是\uset中的单态射\index{单态射(monomorphism)}。
\end{lem}
\begin{proof}
  留给读者。
\end{proof}

当然，\define{满态射 (epimorphism)}
\indexdef{满态射(epimorphism)}%
\indexsee{满态射(epi)}{满态射(epimorphism)}%
是在对偶范畴中的单态射。我们现在展示，在\uset中，满态射正是满射，同时也正是余等化子（正则满态射）。

两个集合$A$和$B$之间的$f,g:A\to B$的余等化子在$\uset$中定义为一般（同伦）余等化子的$0$-截断。为了清楚起见，我们可以将其称为\define{集合余等化子 (set-coequalizer)}。
\indexdef{集合余等化子(set-coequalizer)}%
\indexsee{集合余等化子(coequalizer!of sets)}{set-coequalizer}%
它的泛性质方便地表达如下。

\begin{lem}
  \index{集合余等化子的泛性质(universal!property!of set-coequalizer)}%
  设$f,g:A\to B$为两个集合$A$和$B$之间的函数。{集合余}等化子$c_{f,g}:B\to Q$具有如下性质：对于任意集合$C$和任意$h:B\to C$，满足$h\circ f = h\circ g$，类型
  \begin{equation*}
    \sm{k:Q\to C} (k\circ c_{f,g} = h)
  \end{equation*}
  是收缩的。
\end{lem}

\begin{lem}\label{epis-surj}
对于集合之间的任意函数$f:A\to B$，以下条件是等价的：
\begin{enumerate}
  \item $f$是一个满态射。
  \item 考虑推出图
  \begin{equation*}
    \xymatrix{
        {A}
      \ar[r]^{f}
      \ar[d]
      &
        {B}
      \ar[d]^{\iota}
      \\
      {\unit}
      \ar[r]_{t}
      &
        {C_f}
    }
  \end{equation*}
  在$\uset$中定义了映射锥\index{映射锥(cone!of a function)}。那么类型$C_f$是收缩的。
  \item $f$是满射。
\end{enumerate}
\end{lem}

\begin{proof}
  设$f:A\to B$为一个集合之间的函数，假设它是一个满态射；我们证明$C_f$是收缩的。$C_f$的构造器$\unit\to C_f$给了我们一个元素$t:C_f$。我们需要证明
  \begin{equation*}
    \prd{x:C_f} x= t.
  \end{equation*}
  请注意$x= t$是一个简单命题，因此我们可以对$C_f$进行归纳。当然，当$x$为$t$时，我们有$\refl{t}:t=t$，所以足以找到
  \begin{align*}
    I_0 & : \prd{b:B} \iota(b)= t\\
    I_1 & : \prd{a:A} \opp{\alpha_1(a)} \ct I_0(f(a))=\refl{t}
  \end{align*}
  其中$\iota:B\to C_f$和$\alpha_1:\prd{a:A} \iota(f(a))= t$是$C_f$的其他构造器。请注意$\alpha_1$是$\iota\circ f$到$\mathsf{const}_t\circ f$的一个同伦，因此我们可以找到元素
  \begin{equation*}
    \pairr{\iota,\refl{\iota\circ f}},\pairr{\mathsf{const}_t,\alpha_1}:
    \sm{h:B\to C_f} \iota\circ f \htpy h\circ f.
  \end{equation*}
  通过\cref{thm:mono}\ref{item:mono3}的对偶（以及函数扩展性），我们有一条路径
  \begin{equation*}
    \gamma:\pairr{\iota,\refl{\iota\circ f}}=\pairr{\mathsf{const}_t,\alpha_1}.
  \end{equation*}
  因此，我们可以定义$I_0(b)\defeq \happly(\projpath1(\gamma),b):\iota(b)=t$。
  我们还有
  \[\projpath2(\gamma) : \trans{\projpath1(\gamma)}{\refl{\iota\circ f}} = \alpha_1。 \]
  此传输涉及$f$的前置，它与$\happly$一起工作。因此，从路径类型中的传输我们得到$I_0(f(a)) = \alpha_1(a)$，对于任何$a:A$，这给了我们$I_1$。

  现在假设$C_f$是收缩的；我们证明$f$是满射。我们首先通过$C_f$上的递归构造一个类型族$P:C_f\to\prop$，这是有效的，因为\prop是一个集合。在点构造器上，我们定义
  \begin{align*}
    P(t) & \defeq \unit\\
    P(\iota(b)) & \defeq \brck{\hfiber{f}b}.
  \end{align*}
  为了完成$P$的构造，我们还需要为所有$a:A$给出一条路径
  \narrowequation{\brck{\hfiber{f}{f(a)}} =_\prop \unit。}
  然而，$\brck{\hfiber{f}{f(a)}}$是由$(f(a),\refl{f(a)})$居住的。由于它是一个简单命题，这意味着它是收缩的——因此是等价的，因此与\unit相等。这完成了$P$的定义。现在，由于$C_f$被假设为收缩的，因此$P(x)$对于任何$x:C_f$都是等价于$P(t)$的。特别是，$P(\iota(b))\jdeq \brck{\hfiber{f}b}$等价于$P(t)\jdeq \unit$，对于每个$b:B$，因此是收缩的。因此，$f$是满射。

  最后，假设$f:A\to B$是满射，并考虑一个集合$C$和两个函数$g,h:B\to C$，它们具有$g\circ f = h\circ f$的性质。由于$f$被假设为满射，因此对于所有$b:B$，类型$\brck{\hfib f b}$是收缩的。因此我们有以下等价：
  \begin{align*}
    \prd{b:B} (g(b)= h(b))
    & \eqvsym \prd{b:B} \Parens{\brck{\hfib f b} \to (g(b)= h(b))}\\
    & \eqvsym \prd{b:B} \Parens{\hfib f b \to (g(b)= h(b))}\\
    & \eqvsym \prd{b:B}{a:A}{p:f(a)= b} g(b)= h(b)\\
    & \eqvsym \prd{a:A} g(f(a))= h(f(a))。
  \end{align*}
  使用在第二行中的事实，即$g(b)=h(b)$是一个简单命题，因为$C$是一个集合。但根据假设，有该类型的一个元素。
\end{proof}

\begin{thm}\label{thm:set_regular}\label{lem:images_are_coequalizers}
范畴$\uset$是正则的。此外，集合之间的满射是正则满态射。
\end{thm}

\begin{proof}
  这是范畴论中的一个标准引理，即范畴是正则的，只要它承认有限极限和稳定于拉回的正交因子分解系统\index{正交因子分解系统(orthogonal factorization system)} $(\mathcal{E},\mathcal{M})$，其中$\mathcal{M}$是单态射，在这种情况下，$\mathcal{E}$自动由正则满态射组成。
  (参见例如\cite[A1.3.4]{elephant}）。
  因子分解系统的存在性在\cref{thm:orth-fact}中得到证明。
\end{proof}

\begin{lem}\label{lem:pb_of_coeq_is_coeq}
在\uset中，正则满态射的拉回是正则满态射。
\end{lem}
\begin{proof}
  我们在\cref{thm:stable-images}中展示了，$n$-连通函数的拉回是$n$-连通的。通过\cref{lem:images_are_coequalizers}，当$n=-1$时应用这一结论就足够了。
\end{proof}

\indexdef{子集的像(image!of a subset)}
\uset作为正则范畴的一个后果是，我们有了“像”运算作用于子集。也就是说，给定$f:A\to B$，任何子集$P:\power A$（即谓词$P:A\to \prop$）都有一个\define{像 (image)}，它是$B$的一个子集。这可以直接定义为$\setof{ y:B | \exis{x:A} f(x)=y \land P(x)}$，或间接地定义为复合函数
\[ \setof{ x:A | P(x) } \to A \xrightarrow{f} B的像。]
\symlabel{subset-image}
我们有时也会使用常见的记号$\setof{f(x) | P(x)}$来表示$P$的像。


\subsection{商 (Quotients)}\label{subsec:quotients}

\index{集合商(set-quotient|(}%
现在我们知道$\uset$是正则的，要表明$\uset$是精确的，我们需要证明每个等价关系都是有效的。
\index{有效!等价关系(effective!equivalence relation|(}%
\index{关系!有效等价(effective equivalence|(}%
换句话说，给定等价关系$R:A\to A\to\prop$，存在一个对偶的余等化子$c_R$，并且$\proj1$和$\proj2$形成$c_R$的核对偶。

我们已经在\cref{sec:set-quotients}中看到了两个构造集合按等价关系$R:A\to A\to\prop$的商的方法。第一个可以描述为
\[ \proj1,\proj2:\Parens{\sm{x,y:A} R(x,y)} \to A的集合余}等化子。]
其商的一个重要性质如下。

\begin{defn}
一个关系$R:A\to A\to\prop$被称为\define{有效的 (effective)}，
\indexdef{有效!关系(effective!relation)}
\indexdef{有效!等价关系(effective!equivalence relation)}%
\indexdef{关系!有效等价(effective equivalence)}%
如果方框
\begin{equation*}
\xymatrix{
{\sm{x,y:A} R (x,y)}
\ar[r]^(0.7){\proj1}
\ar[d]_{\proj2}
&
{A}
\ar[d]^{c_R}
\\
{A}
\ar[r]_{c_R}
&
{A/R}
}
\end{equation*}
是一个拉回。
\end{defn}

由于$c_R$和它本身的标准拉回是$\sm{x,y:A} (c_R(x)=c_R(y))$，通过\cref{thm:total-fiber-equiv}，这相当于要求$c_R(x)=c_R(y)$的典型转换是一个纤维等价。

\begin{lem}\label{lem:sets_exact}
假设$\pairr{A,R}$是一个等价关系。那么对于任何$x,y:A$，有一个等价关系
\begin{equation*}
(c_R(x)= c_R(y))\eqvsym R(x,y)。
\end{equation*}
换句话说，等价关系是有效的。
\end{lem}

\begin{proof}
我们首先通过对$A/R$进行双重归纳将$R$扩展为一个关系$\widetilde{R}:A/R\to A/R\to\prop$，然后我们将证明它与$A/R$上的恒等类型等价。我们定义$\widetilde{R}(c_R(x),c_R(y)) \defeq R(x,y)$。对于$r:R(x,x')$和$s:R(y,y')$，$R$的传递性和对称性给出了$R(x,y)$到$R(x',y')$的一个等价关系。这完成了$\widetilde{R}$的定义。

现在要证明对于每个$w,w':A/R$，$\widetilde{R}(w,w')\eqvsym (w= w')$。
方向$(w=w')\to \widetilde{R}(w,w')$通过传输一次我们证明了$\widetilde{R}$是反射的，这是一种简单的归纳。
另一个方向$\widetilden{R}(w,w')\to (w= w')$是一个简单命题，因此由于$c_R:A\to A/R$是满射，只需要假设$w$和$w'$是$c_R(x)$和$c_R(y)$形式的。但在这种情况下，我们有典型映射$\widetilden{R}(c_R(x),c_R(y)) \defeq R(x,y) \to (c_R(x)=c_R(y))$。（再次注意到编码解码方法的出现。\index{编码解码方法(encode-decode method)}）
\end{proof}

第二个商的构造是作为$R$的等价类的集合（它的幂集的子集）：
\[ A\sslash R \defeq \setof{ P:A\to\prop | P \text{ is an equivalence class of } R}。]
这需要命题缩放\index{命题缩放(propositional resizing)}\index{非预测性商(impredicative!quotient)}\index{缩放(resizing)}来保持在与$A$和$R$相同的宇宙中。

注意，如果我们将$R$视为$A$到$A\to \prop$的函数，那么$A\sslash R$等价于\cref{sec:image}中构造的$\im(R)$。现在在\cref{lem:images_are_coequalizers}中我们已经证明了图像是
余等化子。特别是，我们立即得到余等化子图
\begin{equation*}
\xymatrix{
**[l]{\sm{x,y:A} R (x)= R (y)}
\ar@<0.25em>[r]^{\proj1}
\ar@<-0.25em>[r]_{\proj2}
&
{A}
\ar[r]
&
{A \sslash R。}
}
\end{equation*}
我们可以用这个来给出另一个证明，即任何等价关系是有效的，并且两个商的定义是一致的。

\begin{thm}\label{prop:kernels_are_effective}
对于任意两个集合之间的函数$f:A\to B$，
关系$\ker(f):A\to A\to\prop$由
$\ker(f,x,y)\defeq (f(x)= f(y))$给出是有效的。
\end{thm}
\begin{proof}
我们将使用$\proj1,\proj2: (\sm{x,y:A} f(x)= f(y))\to A$的余等化子$\im(f)$。
注意，函数
\[c_f\defeq\lam{a} \Parens{f(a),\brck{\pairr{a,\refl{f(a)}}}}
: A \to \im(f)
\]
的核对偶由两个投影
\begin{equation*}
\proj1,\proj2:\Parens{\sm{x,y:A} c_f(x)= c_f(y)}\to A。
\end{equation*}
对于任何$x,y:A$，我们有等价
\begin{align*}
(c_f(x)= c_f(y))
& \eqvsym \Parens{\sm{p:f(x)= f(y)} \trans{p}{\brck{\pairr{x,\refl{f(x)}}}} =\brck{\pairr{y,\refl{f(y)}}}}\\
& \eqvsym (f(x)= f(y))，
\end{align*}
其中最后一个等价关系成立，因为
$\brck{\hfiber{f}b}$对于任何$b:B$来说是一个简单命题。
因此，我们得到
\begin{equation*}
\Parens{\sm{x,y:A} c_f(x)= c_f(y)}\eqvsym \Parens{\sm{x,y:A} f(x)= f(y)}
\end{equation*}
并且我们可以得出结论，对于任何函数$f$，$\ker f$是一个有效的关系。
\end{proof}

\begin{thm}
等价关系是有效的，并且$A/R \eqvsym A\sslash  R$。
\end{thm}

\begin{proof}
我们需要分析余等化子图
\begin{equation*}
\xymatrix{
**[l]{\sm{x,y:A} R (x)= R (y)}
\ar@<0.25em>[r]^{\proj1}
\ar@<-0.25em>[r]_{\proj2}
&
{A}
\ar[r]
&
{A \sslash R}
}
\end{equation*}
通过单值化公理，类型$R(x) = R(y)$等价于从$R(x)$到$R(y)$的同伦类型，并且进一步等价于
\narrowequation{\prd{z:A} R (x,z)\eqvsym R (y,z)}。
由于$R$是一个等价关系，后者空间等价于$R(x,y)$。总之，我们得到$(R(x) = R(y)) \eqvsym R(x,y)$，因此$R$是有效的，因为它等价于一个有效的关系。此外，图
\begin{equation*}
\xymatrix{
**[l]{\sm{x,y:A} R(x, y)}
\ar@<0.25em>[r]^{\proj1}
\ar@<-0.25em>[r]_{\proj2}
&
{A}
\ar[r]
&
{A \sslash R。}
}
\end{equation*}
是一个余等化子图。由于余等化子是等价的，因此可以得出$A/R \eqvsym A\sslash  R$。
\end{proof}

我们通过提到商的第三种可能的构造来结束本节。考虑一个以$A$为对象的预范畴，其同态集为$R$；此预范畴的Rezk完成\index{完成!Rezk}（参见\cref{sec:rezk}）的对象类型将是该等价关系的商。读者可以检查详细信息。

\index{有效!等价关系|)}%
\index{关系!有效等价|)}%
\index{集合商|)}%

\subsection{\texorpdfstring{$\uset$}{Set}是一个\texorpdfstring{$\Pi\mathsf{W}$}{ΠW}-前拓扑范畴}
\label{subsec:piw}

\index{结构化!集合论|(}%

所谓的\emph{$\Pi\mathsf{W}$-前拓扑范畴} \index{PiW-pretopos@$\Pi\mathsf{W}$-pretopos}%
\indexsee{前拓扑范畴}{$\Pi\mathsf{W}$-pretopos}是一种局部笛卡尔闭范畴
\index{局部笛卡尔闭范畴(locally cartesian closed category)}%
\index{范畴!局部笛卡尔闭(locally cartesian closed)}%
具有不相交的有限上积，有效等价关系，以及多项式自函子的初始代数的范畴——这被认为是一种“预测性”的拓扑概念，即“预测性集合”的范畴，可用于构造数学
\index{数学!构造性}%
就像通常的集合范畴对于经典数学
\index{数学!经典}%
的用途一样。

通常，在构造性类型论中，求助于“集合体”——一种精确补全——的外部构造来获得具有此类闭包性质的范畴。
\index{集合体}\index{补全!精确}%
特别是，良好行为的商在数学中通常涉及（非构造性）幂集的许多构造中是必需的。值得注意的是，统一基础通过更高归纳类型（higher inductive types）提供了这些内部构造，而无需此类外部构造。这代表了我们方法的强大优势，我们将在后续示例中看到。

\begin{thm}
\index{PiW-pretopos@$\Pi\mathsf{W}$-pretopos}
范畴$\uset$是一个$\Pi\mathsf{W}$-前拓扑范畴。
\end{thm}
\begin{proof}
我们有一个初始对象
\index{初始!集合}%
$\emptyt$和有限、不相交的上积$A+B$。这些在拉回时保持稳定，原因很简单，因为拉回有一个右伴随\index{伴随!函子}。事实上，$\uset$是局部笛卡尔闭的，因为对于集合之间的任何映射$f:A\to B$，使用“纤维化替换”\index{纤维化替换(fibrant replacement)}$\sm{a:A}f(a)=b$等价于$A$（在$B$上），并且我们有该替换的依赖函数类型。
我们刚刚展示了$\uset$是正则的（\cref{thm:set_regular}），并且商是有效的（\cref{lem:sets_exact}）。因此，我们有一个局部笛卡尔闭前拓扑范畴。最后，由于$n$-类型在\cref{ex:ntypes-closed-under-wtypes}中通过多项式自函子的初始代数（\cref{thm:w-hinit}）构成，我们看到$\uset$是一个$\Pi\mathsf{W}$-前拓扑范畴。
\end{proof}

\index{拓扑|(}
人们自然会想知道，有什么（如果有的话）阻止$\uset$成为一个（基本）拓扑？
除了已经提到的结构，拓扑还具有一个\emph{子对象分类器}：
\indexdef{子对象分类器(subobject classifier)}%
\index{分类器!子对象(classifier!subobject)}%
\index{幂集(power set)}%
这是一个指示对象，用于分类（等价类的）单态射（monomorphisms）。实际上，在具有子对象分类器的情况下，事情变得稍微简单一些：仅需要笛卡尔闭包即可获得余积。
在同伦类型论中，单值化公理表明，类型$\prop \defeq \sm{X:\UU}\isprop(X)$确实分类单态射（通过类似于\cref{sec:object-classification}的论证），但通常它与周围的宇宙$\UU$一样大。因此，它在某种意义上是一个“集合”，因为它是一个$0$-类型，但它不是“小的”，因为它不是$\UU$的对象，因此不是范畴$\uset$的对象。然而，如果我们假设一种适当形式的命题缩放（见\cref{subsec:prop-subsets}），那么我们可以找到$\prop$的一个小版本，使得$\uset$成为一个基本的拓扑范畴。

\begin{thm}\label{thm:settopos}
\index{命题!缩放(propositional resizing)}%
如果存在一个类型$\Omega:\UU$，包含所有简单命题，那么范畴$\uset_\UU$是一个基本拓扑范畴。
\end{thm}
\index{拓扑|)}

一个足够的条件是排中律，在“简单命题”形式中，我们称之为 \LEM{}；因为在这种情况下，我们有 $\prop = \bool$，这是“小的”，并且可以分类所有的简单命题。此外，拓扑理论中一个众所周知的充分条件是选择公理，这是经典\index{数学!经典} 集合论中经常假设的公理。在下一节中，我们将简要探讨这些条件在我们环境下的关系。

\index{结构化!集合论|)}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{选择公理蕴含排中律}
\label{subsec:emacinsets}

我们从以下引理开始。

\begin{lem}\label{prop:trunc_of_prop_is_set}
如果 $A$ 是一个简单命题，那么其悬挂 $\susp(A)$ 是一个集合，并且 $A$ 等价于 $\id[\susp(A)]{\north}{\south}$。
\end{lem}

\begin{proof}
为了证明 $\susp(A)$ 是一个集合，我们定义一个族 $P:\susp(A)\to\susp(A)\to\type$，使得对于每个 $x,y:\susp(A)$，$P(x,y)$ 是一个简单命题，并且它等价于 $\susp(A)$ 上的同一类型 $\idtypevar{\susp(A)}$。
%
我们做以下定义：
\begin{align*}
P(\north,\north) & \defeq \unit &
P(\south,\north) & \defeq A\\
P(\north,\south) & \defeq A &
P(\south,\south) & \defeq \unit。
\end{align*}
我们需要检查定义是否保持路径。对于任何 $a : A$，有一个子午线 $\merid(a) : \north = \south$，因此我们应该有
%
\begin{equation*}
P(\north, \north) = P(\north, \south) = P(\south, \north) = P(\south, \south)。
\end{equation*}
%
但由于 $A$ 由 $a$ 占据，它等价于 $\unit$，因此我们有
%
\begin{equation*}
P(\north, \north) \eqvsym P(\north, \south) \eqvsym P(\south, \north) \eqvsym P(\south, \south)。
\end{equation*}
%
单值化公理将这些转换为所需的相等性。此外，$P(x,y)$ 对于所有 $x, y : \susp(A)$ 是一个简单命题，这通过对 $x$ 和 $y$ 的归纳以及简单命题是一个简单命题这一事实来证明。

注意，$P$ 是一个自反关系。因此，我们可以应用 \cref{thm:h-set-refrel-in-paths-sets}，因此只需构造 $\tau : \prd{x,y:\susp(A)}P(x,y)\to(x=y)$。我们通过双重归纳来实现。当 $x$ 是 $\north$ 时，我们定义 $\tau(\north)$ 为
%
\begin{equation*}
\tau(\north,\north,u) \defeq \refl{\north}
\qquad\text{以及}\qquad
\tau(\north,\south,a) \defeq \merid(a)。
\end{equation*}
%
如果 $A$ 由 $a$ 占据，那么 $\merid(a) : \north = \south$，因此我们还需要
\narrowequation{
\trans{\merid(a)}{\tau(\north, \north)} = \tau(\north, \south)。
}
通过函数外延性，我们使用以下事实来完成这一步：
%
\begin{multline*}
\trans{\merid(a)}{\tau(\north,\north,x)} =
\tau(\north,\north,x) \ct \opp{\merid(a)} \jdeq \\
\refl{\north} \ct \merid(a) =
\merid(a) =
\merid(x) \jdeq
\tau(\north, \south, x)。
\end{multline*}
以对称的方式，我们可以通过以下方式定义 $\tau(\south)$：
%
\begin{equation*}
\tau(\south,\north, a) \defeq \opp{\merid(a)}
\qquad\text{以及}\qquad
\tau(\south,\south, u) \defeq \refl{\south}。
\end{equation*}
%
为了完成 $\tau$ 的构造，我们需要检查 $\trans{\merid(a)}{\tau(\north)} = \tau(\south)$，对于任何 $a : A$。验证过程与上述类似，通过对 $\tau$ 的第二个参数的归纳来进行。

因此，通过 \cref{thm:h-set-refrel-in-paths-sets} 我们得出 $\susp(A)$ 是一个集合，并且对于所有 $x,y:\susp(A)$ 有 $P(x,y) \eqvsym (\id{x}{y})$。取 $x\defeq \north$ 和 $y\defeq \south$ 即可得到所需的 $A \eqvsym (\id[\susp(A)]\north\south)$。
\end{proof}

\begin{thm}[Diaconescu 定理]\label{thm:1surj_to_surj_to_pem}
\index{选择公理(axiom of choice)}%
\index{排中律(excluded middle)}%
\index{Diaconescu's theorem(迪亚孔涅斯库定理)}\index{theorem!Diaconescu's(迪亚孔涅斯库定理)}%
选择公理蕴含排中律。
\end{thm}

\begin{proof}
我们使用在 \cref{thm:ac-epis-split} 中给出的选择公理的等价形式。考虑一个简单命题 $A$。定义一个函数 $f:\bool\to\susp(A)$，其定义为 $f(\bfalse) \defeq \north$ 和 $f(\btrue) \defeq \south$。这个函数是满射的。实际上，我们有 $\pairr{\bfalse,\refl{\north}} : \hfiber{f}{\north}$ 和 $\pairr{\btrue,\refl{\south}} :\hfiber{f}{\south}$。由于 $\bbrck{\hfiber{f}{x}}$ 是一个简单命题，通过归纳法可以得出所需的满射性。

根据 \cref{prop:trunc_of_prop_is_set}，悬挂 $\susp(A)$ 是一个集合，因此根据选择公理，存在一个从 $\susp(A)$ 到 $\bool$ 的截面 $g: \susp(A) \to \bool$。由于 $\bool$ 上的相等性是可判定的，我们得到
\begin{equation*}
(g(f(\bfalse))= g(f(\btrue))) +
\lnot (g(f(\bfalse))= g(f(\btrue))),
\end{equation*}
并且，由于 $g$ 是 $f$ 的一个截面，因此是单射，
\begin{equation*}
(f(\bfalse) = f(\btrue)) +
\lnot (f(\bfalse) = f(\btrue))。
\end{equation*}
最后，由于 $(f(\bfalse)=f(\btrue)) = (\north=\south) = A$ 根据 \cref{prop:trunc_of_prop_is_set}，我们有 $A+\neg A$。
\end{proof}

% This conclusion needs only \LEM{}, see \cref{ex:lemnm}.

% \begin{cor}\label{cor:ACtoLEM0}
%   If the axiom of choice \choice{} holds then $\brck{A + \neg A}$ for every set $A$.
% \end{cor}

% \begin{proof}
%   There is a surjection
%   \[
%   A + \neg A \epi \brck{A} + \brck{\neg A} \epi
%   \brck{(\brck{A} + \brck{\neg A})} = \brck{A} \vee \brck{\neg A} = \brck{A} \vee \neg \brck{A} = \unit,
%   \]
%   %
%   where in the last step excluded middle is available as a consequence of the axiom of choice.
%   Again by the axiom of choice there merely exists a section of the surjection, but this
%   is none other than an inhabitant of $A + \neg A$. Therefore $\brck{A+\neg A}$.
% \end{proof}

\index{denial(否定)}
\begin{thm}\label{thm:ETCS}
\index{Elementary Theory of the Category of Sets(集合范畴的初等理论)}%
\index{category!well-pointed(范畴!良好定点)}%
如果选择公理成立，则类别 $\uset$ 是一个带选择的良好定点布尔初等拓扑。
\end{thm}

\begin{proof}
由于 \choice{} 蕴含 \LEM{}，通过 \cref{thm:settopos} 以及后面的注释，我们可以得到一个带选择的布尔初等拓扑。我们将良好定点性的证明留给读者作为练习 (\cref{ex:well-pointed})。
\end{proof}

\begin{rmk}
定理中提到的关于范畴的条件被称为 Lawvere 用于“集合范畴的初等理论”的公理~\cite{lawvere:etcs-long}。
\end{rmk}

\section{基数 (Cardinal numbers)}
\label{sec:cardinals}

\begin{defn}\label{defn:card}
\define{基数类型 (type of cardinal numbers)}
\indexdef{type!of cardinal numbers}%
\indexdef{cardinal number}%
\indexsee{number!cardinal}{cardinal number}%
是集合类型 (\set) 的 0-截断：
\[ \card \defeq \pizero{\set} \]
因此，一个 \define{基数 (cardinal number)}，或称 \define{基数 (cardinal)}，是 $\card\jdeq \pizero\set$ 的一个元素。
技术上，当然每个宇宙 \type 都有一个单独的基数类型 $\card_\UU$ 。
\end{defn}

%\begin{rmk}

% , but with these conventions we can state theorems beginning with ``for all cardinal numbers\dots''\ and give them exactly the same sort of meaning as those beginning ``for all types\dots''.
%\end{rmk}

和通常的截断一样，如果 $A$ 是一个集合，那么 $\cd{A}$ 表示其在从集合类型到 0-截断 $\trunc0\set \jdeq \card$ 的标准映射下的像；我们称 $\cd{A}$ 为 $A$ 的 \define{基数 (cardinality)}\indexdef{cardinality}。
根据定义，\card 是一个集合。
它还继承了来自 \set 的半环结构。

\begin{defn}
\define{基数加法 (cardinal addition)}
\indexdef{addition!of cardinal numbers}%
\index{cardinal number!addition of}%
的运算定义为截断上的归纳：
\[ (\blank+\blank) : \card \to \card \to \card \]
定义为：
\[ \cd{A} + \cd{B} \defeq \cd{A+B}.\]
\end{defn}
\begin{proof}
由于 $\card\to\card$ 是一个集合，要为所有 $\alpha:\card$ 定义 $(\alpha+\blank):\card\to\card$，通过归纳，只需要假设 $\alpha$ 是某个 $A:\set$ 的 $\cd{A}$。
现在我们想要定义 $(\cd{A}+\blank) :\card\to\card$，即我们想要为所有 $\beta:\card$ 定义 $\cd{A}+\beta :\card$。
然而，由于 \card 是一个集合，通过归纳，只需要假设 $\beta$ 是某个 $B:\set$ 的 $\cd{B}$。
但是现在我们可以定义 $\cd{A}+\cd{B}$ 为 $\cd{A+B}$。
\end{proof}

\begin{defn}
类似地，\define{基数乘法 (cardinal multiplication)}
\indexdef{multiplication!of cardinal numbers}%
\index{cardinal number!multiplication of}%
的运算定义为截断上的归纳：
\[ (\blank\cdot\blank) : \card \to \card \to \card \]
定义为：
\[ \cd{A} \cdot \cd{B} \defeq \cd{A\times B} \]
\end{defn}

\begin{lem}\label{card:semiring}
\card 是一个交换半环 (commutative semiring)\index{semiring}，即对于 $\alpha,\beta,\gamma:\card$ 我们有以下性质。
\begin{align*}
(\alpha+\beta)+\gamma &= \alpha+(\beta+\gamma)\\
\alpha+0 &= \alpha\\
\alpha + \beta &= \beta + \alpha\\
(\alpha \cdot \beta) \cdot \gamma &= \alpha \cdot (\beta\cdot\gamma)\\
\alpha \cdot 1 &= \alpha\\
\alpha\cdot\beta &= \beta\cdot\alpha\\
\alpha\cdot(\beta+\gamma) &= \alpha\cdot\beta + \alpha\cdot\gamma
\end{align*}
其中 $0 \defeq \cd{\emptyt}$ 且 $1\defeq\cd{\unit}$。
\end{lem}
\begin{proof}
我们证明乘法的交换性，即 $\alpha\cdot\beta = \beta\cdot\alpha$；其他性质的证明完全类似。
由于 \card 是一个集合，类型 $\alpha\cdot\beta = \beta\cdot\alpha$ 是一个纯命题，并且特别地是一个集合。
因此，通过截断上的归纳，只需要假设 $\alpha$ 和 $\beta$ 分别是某些 $A,B:\set$ 的 $\cd{A}$ 和 $\cd{B}$。
现在 $\cd{A}\cdot \cd{B} \jdeq \cd{A\times B}$ 和 $\cd{B}\cdot\cd{A} \jdeq \cd{B\times A}$，所以只需要证明 $A\times B = B\times A$。
最后，通过同一性原理 (univalence)，只需要给出一个等价 $A\times B \eqvsym B\times A$。
这很简单：取 $(a,b) \mapsto (b,a)$ 及其显然的逆映射即可。
\end{proof}

\begin{defn}
\define{基数指数 (cardinal exponentiation)} 的运算同样定义为截断上的归纳：
\indexdef{exponentiation, of cardinal numbers}%
\index{cardinal number!exponentiation of}%
\[ \cd{A}^{\cd{B}} \defeq \cd{B\to A}. \]
\end{defn}

\begin{lem}\label{card:exp}
对于 $\alpha,\beta,\gamma:\card$ 我们有以下性质：
\begin{align*}
\alpha^0 &= 1\\
1^\alpha &= 1\\
\alpha^1 &= \alpha\\
\alpha^{\beta+\gamma} &= \alpha^\beta \cdot \alpha^\gamma\\
\alpha^{\beta\cdot \gamma} &= (\alpha^{\beta})^\gamma\\
(\alpha\cdot\beta)^\gamma &= \alpha^\gamma \cdot \beta^\gamma
\end{align*}
\end{lem}
\begin{proof}
证明与 \cref{card:semiring} 类似。
\end{proof}

\begin{defn}
\define{基数不等式 (cardinal inequality)}
\index{order!non-strict}%
\index{cardinal number!inequality of}%
的关系定义为截断上的归纳：
\symlabel{inj}
\[ \cd{A} \le \cd{B} \defeq \brck{\inj(A,B)} \]
其中 $\inj(A,B)$ 是从 $A$ 到 $B$ 的单射 (injections) 的类型。
\index{function!injective}%
换句话说，$\cd{A} \le \cd{B}$ 意味着从 $A$ 到 $B$ 仅仅存在一个单射。
\end{defn}

\begin{lem}
基数不等式是一个预序 (preorder)，即对于 $\alpha,\beta:\card$ 我们有：
\index{preorder!of cardinal numbers}%
\begin{gather*}
\alpha \le \alpha\\
(\alpha \le \beta) \to (\beta\le\gamma) \to (\alpha\le\gamma)
\end{gather*}
\end{lem}
\begin{proof}
同前，通过截断上的归纳。
例如，类型 $(\alpha \le \beta) \to (\beta\le\gamma) \to (\alpha\le\gamma)$ 是一个纯命题，因此通过 0-截断上的归纳，我们可以假设 $\alpha$、$\beta$ 和 $\gamma$ 分别是 $\cd{A}$、$\cd{B}$ 和 $\cd{C}$。
现在，由于 $\cd{A} \le \cd{C}$ 是一个纯命题，通过 $(-1)$-截断上的归纳，我们可以假设给定了从 $A$ 到 $B$ 的单射 $f$ 和从 $B$ 到 $C$ 的单射 $g$。
但是，$g\circ f$ 是从 $A$ 到 $C$ 的一个单射，因此 $\cd{A} \le \cd{C}$ 成立。
反身性 (reflexivity) 更容易证明。
\end{proof}

我们还可以证明基数不等式与半环运算的兼容性。

\begin{lem}\label{thm:injsurj}
\index{function!injective}%
\index{function!surjective}%
考虑以下命题：
\begin{enumerate}
\item 存在从 $A$ 到 $B$ 的一个单射。\label{item:cle-inj}
\item 存在从 $B$ 到 $A$ 的一个满射。\label{item:cle-surj}
\end{enumerate}
那么，在假设排中律 (excluded middle) 的情况下：
\index{excluded middle}%
\index{axiom!of choice}%
\begin{itemize}
\item 给定 $a_0:A$，我们有 \ref{item:cle-inj}$\to$\ref{item:cle-surj}。
\item 因此，如果 $A$ 是居留 (merely inhabited) 的，我们有 \ref{item:cle-inj} $\to$ 仅仅存在 \ref{item:cle-surj}。
\item 假设选择公理 (axiom of choice)，我们有 \ref{item:cle-surj} $\to$ 仅仅存在 \ref{item:cle-inj}。
\end{itemize}
\end{lem}
\begin{proof}
如果 $f:A\to B$ 是一个单射，则定义 $g:B\to A$ 如下。
由于 $f$ 是单射，因此 $f$ 在 $b$ 处的纤维是一个纯命题。
因此，根据排中律，要么存在 $a:A$ 满足 $f(a)=b$，要么不存在。
在第一种情况下，定义 $g(b)\defeq a$；否则设定 $g(b)\defeq a_0$。
那么对于任何 $a:A$，我们有 $a = g(f(a))$，所以 $g$ 是满射。

第二条是通过截断上的归纳得到的。
对于第三条，如果 $g:B\to A$ 是满射，那么根据选择公理，仅仅存在一个函数 $f:A\to B$ 满足对所有的 $a$ 有 $g(f(a)) = a$。
但此时 $f$ 必然是单射。
\end{proof}

\begin{thm}[Schroeder--Bernstein (施罗德–贝尔斯坦定理)]
\index{theorem!Schroeder--Bernstein}%
\index{Schroeder--Bernstein theorem}%
在假设排中律的情况下，对于集合 $A$ 和 $B$ 我们有：
\[ \inj(A,B) \to \inj(B,A) \to (A\cong B) \]
\end{thm}
\begin{proof}
常见的“来回反复 (back-and-forth)”论证在此仍然适用。
注意，这实际上构造了一个同构 $A\cong B$（假设排中律，以便我们可以决定给定元素是属于循环、无限链、从 $A$ 开始的链，还是从 $B$ 开始的链）。
\end{proof}

\begin{cor}
在假设排中律的情况下，基数不等式是一个偏序 (partial order)，即对于 $\alpha,\beta:\card$ 我们有：
\[ (\alpha\le\beta) \to (\beta\le\alpha) \to (\alpha=\beta). \]
\end{cor}
\begin{proof}
由于 $\alpha=\beta$ 是一个纯命题，通过截断上的归纳，我们可以假设 $\alpha$ 和 $\beta$ 分别是 $\cd{A}$ 和 $\cd{B}$，并且我们有从 $A$ 到 $B$ 的单射 $f$ 和从 $B$ 到 $A$ 的单射 $g$。
但根据施罗德–贝尔斯坦定理，我们得到了一个同构 $A\cong B$，因此得到了一个等式 $\cd{A}=\cd{B}$。
\end{proof}

最后，我们可以重现康托尔 (Cantor) 定理，证明对于每个基数，都存在一个更大的基数。

\begin{thm}[康托尔定理 (Cantor's theorem)]
\index{Cantor's theorem}%
\index{theorem!Cantor's}%
对于 $A:\set$，不存在满射 $A \to (A\to \bool)$。
\end{thm}
\begin{proof}
假设 $f:A \to (A\to \bool)$ 是任意一个函数，定义 $g:A\to \bool$ 为 $g(a) \defeq \neg f(a)(a)$。
如果 $g = f(a_0)$，那么 $g(a_0) = f(a_0)(a_0)$ 但 $g(a_0) = \neg f(a_0)(a_0)$，这就矛盾了。
因此，$f$ 不是满射。
\end{proof}

\begin{cor}
在假设排中律的情况下，对于任意 $\alpha:\card$，存在一个基数 $\beta$ 使得 $\alpha\le\beta$ 且 $\alpha\neq\beta$。
\end{cor}
\begin{proof}
令 $\beta = 2^\alpha$。
现在我们想要证明一个纯命题，所以通过归纳我们可以假设 $\alpha$ 是 $\cd{A}$，因此 $\beta\jdeq \cd{A\to \bool}$。
在排中律的帮助下，我们定义了一个函数 $f:A\to (A\to \bool)$，定义为：
\[f(a)(a') \defeq
\begin{cases}
\btrue &\quad a=a'\\
\bfalse &\quad a\neq a'.
\end{cases}
\]
如果 $f(a)=f(a')$，那么 $f(a')(a) = f(a)(a) = \btrue$，所以 $a=a'$；因此 $f$ 是单射。
因此，$\alpha \jdeq \cd{A} \le \cd{A\to \bool} \jdeq 2^\alpha$。

另一方面，如果 $2^\alpha \le \alpha$，那么我们将有一个单射 $(A\to\bool)\to A$。
根据 \cref{thm:injsurj}，由于我们有 $(\lam{x} \bfalse):A\to \bool$ 和排中律，那么就会有一个从 $A$ 到 $(A\to \bool)$ 的满射，这与康托尔定理相矛盾。
\end{proof}
\section{序数 (Ordinal numbers)}
\label{sec:ordinals}

\index{ordinal|(}%

\begin{defn}\label{defn:accessibility}
设 $A$ 为一个集合，且
\[(\blank<\blank):A\to A\to \prop\]
是 $A$ 上的一个二元关系。
我们通过归纳定义 $a:A$ 的元素对 $<$ 是 \define{可达 (accessible)} 的：
\indexdef{accessibility}%
\indexsee{accessible}{accessibility}%
\begin{itemize}
\item 如果对所有 $b<a$ 的 $b$ 都是可达的，则 $a$ 是可达的。
\end{itemize}
我们写作 $\acc(a)$ 表示 $a$ 是可达的。
\end{defn}

乍一看，这样的归纳定义似乎无法成立，但如果 $a$ 具有这样一个性质，即不存在 $b$ 使得 $b<a$，那么 $a$ 是可达的，这实际上是成立的。

注意，这是一个类型族的归纳定义，类似于在 \cref{sec:generalizations} 中考虑的向量类型。
更确切地说，它只有一个构造器，记为 $\acc_<$，其类型为
\[ \acc_< : \prd{a:A} \Parens{\prd{b:A} (b<a) \to \acc(b)} \to \acc(a). \]
\index{induction principle!for accessibility}%
$\acc$ 的归纳原理表明，对于任意 $P:\prd{a:A} \acc(a) \to \type$，如果我们有
\[f:\prd{a:A}{h:\prd{b:A} (b<a) \to \acc(b)}
\Parens{\prd{b:A}{l:b<a} P(b,h(b,l))} \to
P(a,\acc_<(a,h)),
\]
那么我们就有通过归纳定义的 $g:\prd{a:A}{c:\acc(a)} P(a,c)$，其中
\[g(a,\acc_<(a,h)) \jdeq f(a,\,h,\,\lam{b}{l} g(b,h(b,l))).\]
这个公式很繁琐，但通常我们只在 $P:A\to\type$ 只依赖于 $A$ 时使用它的简化形式。
在这种情况下，$f$ 的第二和第三个参数可以合并，因此我们要证明的是
\[f:\prd{a:A} \Parens{\prd{b:A} (b<a) \to \acc(b) \times P(b)}
\to P(a).
\]
也就是说，我们假设每个 $b<a$ 都是可达的，且 $g(b):P(b)$ 已定义，然后从这些定义 $g(a):P(a)$。

省略 $P$ 的第二个参数是通过以下引理来证明的，这也是我们唯一一次使用归纳原理的更一般形式。

\begin{lem}
可达性 (Accessibility)\index{accessibility} 是一个纯属性。
\end{lem}
\begin{proof}
我们必须证明，对于任意 $a:A$ 和 $s_1,s_2:\acc(a)$，有 $s_1=s_2$。
我们通过 $s_1$ 的归纳来证明这一点，其归纳假设为
\[P_1(a,s_1) \defeq \prd{s_2:\acc(a)} (s_1=s_2)。 \]
因此，我们必须证明，对于任意 $a:A$ 和 ${h_1:\prd{b:A} (b<a) \to \acc(b)}$ 以及
\[ k_1:{\prd{b:A}{l:b<a}{t:\acc(b)} h_1(b,l) = t},\]
我们有 $\acc_<(a,h) = s_2$ 对于任意 $s_2:\acc(a)$。
我们将这个陈述视为 $\prd{a:A}{s_2:\acc(a)} P_2(a,s_2)$，其中
\[P_2(a,s_2) \defeq
\prd{h_1 : \cdots } %{h_1:\prd{b:A} (b<a) \to \acc(b)}
{k_1 : \cdots} % \Parens{\prd{b:A}{l:b<a}{t:\acc(b)} h_1(b,l) = t} \to
(\acc_<(a,h_1) = s_2);
\]
因此，我们可以通过 $s_2$ 的归纳来证明它。
因此，我们假设 $h_2 : \prd{b:A} (b<a) \to \acc(b)$，并且 $k_2$ 具有一个复杂但无关紧要的类型，
% \begin{narrowmultline*}
%   k_2:\prd{b:A}{l:b<a}
%   \prd{h_1:\prd{b':A} (b'<b) \to \acc(b')}
%   \narrowbreak
%   \Parens{\prd{b':A}{l':b'<b}{t':\acc(b')} h_1(b',l') = t'} \to
%   (\acc_<(b,h_1) = h_2(b,l)).
% \end{narrowmultline*}
并且必须证明，对于任意类型为上述类型的 $h_1$ 和 $k_1$，
我们有 $\acc_<(a,h_1) = \acc_<(a,h_2)$。
根据函数外延性 (function extensionality)，只需证明 $h_1(b,l) = h_2(b,l)$ 对于所有 $b:A$ 和 $l:b<a$。
这是由 $k_1$ 推出的。
\end{proof}

\begin{defn}
集合 $A$ 上的二元关系 $<$ 是 \define{良基 (well-founded)} 的
\indexdef{relation!well-founded}%
\indexdef{well-founded!relation}%
如果 $A$ 的每个元素都是可达的。
\end{defn}

良基性的意义在于，对于 $P:A\to \type$，我们可以使用 $\acc$ 的归纳原理得出 $\prd{a:A} \acc(a) \to P(a)$，然后应用良基性得出 $\prd{a:A} P(a)$。
换句话说，如果从 $\fall{b:A} (b<a) \to P(b)$ 我们可以证明 $P(a)$，那么 $\fall{a:A} P(a)$ 成立。
这称为 \define{良基归纳 (well-founded induction)}\indexdef{well-founded!induction}。

\begin{lem}
良基性是一个纯属性。
\end{lem}
\begin{proof}
$<$ 的良基性是类型 $\prd{a:A} \acc(a)$，它是一个纯命题，因为每个 $\acc(a)$ 是一个纯命题。
\end{proof}

\begin{eg}\label{thm:nat-wf}
也许最为熟悉的良基关系是自然数 \nat 上的通常的严格排序。
要证明这是良基的，我们必须证明对于每个 $n:\nat$，$n$ 是可达的。
\index{strong!induction}%
这只是从 \nat 上的普通归纳得出的“强归纳” (strong induction) 的常规证明。

具体来说，我们通过对 $n:\nat$ 的归纳证明 $k\le n$ 的所有 $k$ 都是可达的。
基本情况只是 $0$ 是可达的，这在逻辑上成立，因为没有任何元素严格小于 $0$。
对于归纳步骤，我们假设 $k\le n$ 的所有 $k$ 都是可达的，这就是说，对于所有 $k<n+1$，因此根据定义 $n+1$ 也是可达的。

\nat 上的一个不同关系也可以是良基的，即设定仅 $n < \suc(n)$ 对于所有 $n:\nat$。
这个关系的良基性几乎正是 \nat 的普通归纳原理。
\end{eg}

\begin{eg}\label{thm:wtype-wf}
设 $A:\set$ 且 $B : A \to \set$ 是集合的一个族。
回忆 \cref{sec:w-types} 中的 $W$-类型 $\wtype{a:A} B(a)$ 是由单个构造器归纳生成的
\begin{itemize}
\item $\supp : \prd{a:A} (B(a) \to \wtype{x:A} B(x)) \to \wtype{x:A} B(x)$
\end{itemize}
我们通过其第二个参数递归地定义 $\wtype{x:A} B(x)$ 上的关系 $<$：
\begin{itemize}
\item 对于任意 $a:A$ 和 $f:B(a) \to \wtype{x:A} B(x)$，我们定义 $w<\supp(a,f)$ 表示仅存在一个 $b:B(a)$ 使得 $w = f(b)$。
\end{itemize}
现在我们使用 $\wtype{x:A}B(x)$ 的通常归纳原理证明对该关系的每个 $w:\wtype{x:A} B(x)$ 是可达的。
这意味着我们假设给定了 $a:A$ 和 $f:B(a) \to \wtype{x:A} B(x)$，以及一个提升 $f' : \prd{b:B(a)} \acc(f(b))$。
但根据 $<$ 的定义，对于所有 $w<\supp(a,f)$，我们有 $\acc(w)$；因此 $\supp(a,f)$ 是可达的。
\end{eg}

良基性允许我们通过递归定义函数，并通过归纳证明陈述，例如以下内容。
回忆 \cref{subsec:prop-subsets} 中 $\power B$ 表示幂集 $\power B \defeq (B\to\prop)$。

\begin{lem}\label{thm:wfrec}
假设 $B$ 是一个集合，并且我们有一个函数
\[ g : \power B \to B \]
那么，如果 $<$ 是 $A$ 上的一个良基关系，那么存在一个函数 $f:A\to B$，使得对所有 $a:A$ 我们有
\begin{equation*}
f(a) = g\Big(\setof{ f(a') | a'<a }\Big)。
\end{equation*}
\end{lem}
\noindent
（我们使用了 \cref{sec:image} 中关于子集的像的记法。）
\begin{proof}
我们首先定义，对于每个 $a:A$ 和 $s:\acc(a)$，一个元素 $\bar f(a,s):B$。
根据归纳假设，我们假设 $s$ 是一个函数，将每个 $a'<a$ 分配给一个证据 $s(a'):\acc(a')$，并且对每个这样的 $a'$，我们有一个元素 $\bar f(a',s(a')):B$。
在这种情况下，我们定义
\begin{equation*}
\bar f(a,s) \defeq g\Big(\setof{ \bar f(a',s(a')) | a'<a }\Big)。
\end{equation*}

现在，由于 $<$ 是良基的，我们有一个函数 $w:\prd{a:A} \acc(a)$。
因此，我们可以定义 $f(a)\defeq \bar f (a,w(a))$。
\end{proof}
在经典逻辑中，良基性有一个更为人所熟知的重新表述。在以下内容中，我们说一个子集 $B: \power A$ 是\define{非空的 (nonempty)} \indexdef{nonempty subset}，如果它不等于空子集 $(\lam{x}\bot) : \power X$。我们留给读者验证，在假设排中律的前提下，这与单纯的可居住性是等价的，即满足条件 $\exis{x:A} x\in B$。

\begin{lem}\label{thm:wfmin}
\index{excluded middle}%
假设排中律，$<$ 是良基的当且仅当每个非空子集 $B: \power A$ 都仅有一个最小元素。
\end{lem}
\begin{proof}
首先假设 $<$ 是良基的，并假设 $B\subseteq A$ 是一个没有最小元素的子集。
也就是说，对于任何 $a:A$ 使得 $a\in B$，仅存在一个 $b:A$ 使得 $b<a$ 且 $b\in B$。

我们断言，对于任意 $a:A$ 和 $s:\acc(a)$，我们有 $a\notin B$。
通过归纳，我们可以假设 $s$ 是一个函数，将每个 $a'<a$ 分配给一个证明 $s(a'):\acc(a')$，并且对每个这样的 $a'$，我们有 $a'\notin B$。
如果 $a\in B$，那么根据假设，必然存在一个 $b<a$ 且 $b\in B$，这与假设矛盾。
因此，$a\notin B$；这完成了归纳。
由于 $<$ 是良基的，我们有 $a\notin B$ 对所有 $a:A$ 成立，即 $B$ 是空的。

现在假设每个非空子集都仅有一个最小元素。
设 $B = \setof{ a:A | \neg \acc(a) }$。
那么，如果 $B$ 是非空的，它仅有一个最小元素。
因此，仅存在一个 $a:A$ 使得 $a\in B$，并且对所有 $b<a$，我们有 $\acc(b)$。
但是根据定义（以及对截断的归纳），$a$ 是仅可达的，因此是可达的，这与 $a\in B$ 矛盾。
因此，$B$ 是空的，所以 $<$ 是良基的。
\end{proof}

\begin{defn}
集合 $A$ 上的良基关系 $<$ 是\define{外延 (extensional)} 的
\indexdef{relation!extensional}%
\indexdef{extensional!relation}%
如果对于任意 $a,b:A$，我们有
\[ \Parens{\fall{c:A} (c<a) \Leftrightarrow (c<b)} \to (a=b)。 \]
\end{defn}

注意，由于 $A$ 是一个集合，外延性是一个纯属性。
这种“外延性”的概念与函数外延性 (function extensionality) 无关，也与等式类型的外延性无关。
\index{axiom!of extensionality}%
相反，它是经典集合论中外延公理的“局部”对应。

\begin{thm}
外延良基关系的类型是一个集合。
\end{thm}
\begin{proof}
根据公理 (univalence axiom)，如果 $(A,<)$ 是外延和良基的，并且 $f:(A,<) \cong (A,<)$，那么我们必须证明 $f=\idfunc[A]$。
\index{automorphism!of extensional well-founded relations}%
我们通过对 $<$ 进行归纳来证明对于所有 $a:A$，$f(a)=a$。
归纳假设是，对于所有 $a'<a$，我们有 $f(a')=a'$。

现在，由于 $A$ 是外延的，为了得出 $f(a)=a$，我们只需证明
\[\fall{c:A}(c<f(a)) \Leftrightarrow (c<a)。\]
但是，由于 $f$ 是一个自同构，我们有 $(c<a) \Leftrightarrow (f(c)<f(a))$。
但 $c<a$ 意味着根据归纳假设 $f(c)=c$，因此 $(c<a) \to (c<f(a))$。
另一方面，如果 $c<f(a)$，那么 $f^{-1}(c)<a$，因此 $c = f(f^{-1}(c)) = f^{-1}(c)$ 再次根据归纳假设；因此 $c<a$。
因此，我们有 $(c<a) \Leftrightorrow (c<f(a))$ 对于任意 $c:A$，所以 $f(a)=a$。
\end{proof}

\begin{defn}\label{def:simulation}
如果 $(A,<)$ 和 $(B,<)$ 是外延良基的关系，$f:A\to B$ 是一个\define{模拟 (simulation)}
\indexdef{simulation}%
\indexsee{function!simulation}{simulation}%
如果满足以下条件：
\begin{enumerate}
\item 如果 $a<a'$，那么 $f(a)<f(a')$，并且\label{item:sim1}
\item 对于所有 $a:A$ 和 $b:B$，如果 $b<f(a)$，那么仅存在一个 $a'<a$ 使得 $f(a')=b$。\label{item:sim2}
\end{enumerate}
\end{defn}

\begin{lem}
任何模拟都是单射的。
\end{lem}
\begin{proof}
我们通过双重良基归纳证明，对于任意 $a,b:A$，如果 $f(a)=f(b)$，那么 $a=b$。
归纳假设对于 $a:A$ 表示，对于任意 $a'<a$ 和任意 $b:B$，如果 $f(a')=f(b)$，那么 $a=b$。
内部归纳假设对于 $b:A$ 表示，对于任意 $b'<b$，如果 $f(a)=f(b')$，那么 $a=b'$。

假设 $f(a)=f(b)$；我们必须证明 $a=b$。
根据外延性，为了证明 $f(a)=b$，我们只需证明 $\fall{c:A}(c<a) \Leftrightarrow (c<b)$。

但是，由于 $f$ 是一个模拟，如果 $c<a$，那么我们有 $f(c)<f(a)$ 根据 \cref{def:simulation}\ref{item:sim1}。
因此 $f(c)<f(b)$，所以根据 \cref{def:simulation}\ref{item:sim2}，仅存在一个 $c':A$ 使得 $c'<b$ 且 $f(c)=f(c')$。
根据归纳假设 $a$，我们有 $c=c'$，因此 $c<b$。
对称的论证也是对称的。
\end{proof}

特别地，这意味着在 \cref{def:simulation}\ref{item:sim2} 中可以去掉“仅”一词而不改变意义。

\begin{cor}
如果 $f:A\to B$ 是一个模拟，那么对于所有 $a:A$ 和 $b:B$，如果 $b<f(a)$，那么\emph{必然}存在一个 $a'<a$ 使得 $f(a')=b$。
\end{cor}
\begin{proof}
由于 $f$ 是单射的，$\sm{a:A} (f(a)=b)$ 是一个纯命题。
\end{proof}

我们说一个子集 $C :\power B$ 是\define{初始段 (initial segment)} \indexdef{initial!segment} \indexsee{segment, initial}{initial segment}，如果 $c\in C$ 并且 $b<c$，那么 $b\in C$。模拟的像必须是一个初始段，而任何初始段的包含是一个模拟。因此，根据公理 (univalence axiom)，每个 $A\to B$ 的模拟\emph{等同于} $B$ 的某个初始段的包含。

\begin{thm}
对于一个集合 $A$，设 $P(A)$ 为 $A$ 上的外延良基关系的类型。
如果 $\mathord{<_A} : P(A)$ 和 $\mathord{<_B} : P(B)$ 并且 $f:A\to B$，令 $H_{\mathord{<_A}\mathord{<_B}}(f)$ 是 $f$ 是一个模拟的纯命题。
那么 $(P,H)$ 是一个标准的结构概念，属于 \uset 中的结构，见 \cref{sec:sip}。
\end{thm}
\begin{proof}
我们留给读者验证，恒等是模拟，并且模拟的复合也是模拟。
因此，我们有了一个结构的概念。
对于标准性，我们必须证明如果 $<$ 和 $\prec$ 是两个集合 $A$ 上的外延良基关系，并且 $\idfunc[A]$ 是双向模拟，那么 $<$ 和 $\prec$ 是相等的。
由于外延性和良基性是纯命题，对于这一点我们仅需有 $\fall{a,b:A} (a<b) \Leftrightarrow (a\prec b)$。
但这由 \cref{def:simulation}\ref{item:sim1} 对于 $\idfunc[A]$ 来证明。
\end{proof}

\begin{cor}\label{thm:wfcat}
有一个范畴，其对象是带有外延良基关系的集合，其态射是模拟。
\end{cor}

实际上，这个范畴是一个偏序集。

\begin{lem}
对于外延和良基的 $(A,<)$ 和 $(B,<)$，至多存在一个从 $A$ 到 $B$ 的模拟。
\end{lem}
\begin{proof}
假设 $f,g:A\to B$ 是模拟。
由于是模拟是一个纯命题，我们只需证明 $\fall{a:A}(f(a)=g(a))$。
通过对 $<$ 进行归纳，我们可以假设对于所有 $a'<a$，$f(a')=g(a')$。
由于 $B$ 的外延性，为了证明 $f(a)=g(a)$，我们只需有 $\fall{b:B}(b<f(a)) \Leftrightarrow (b<g(a))$。

但由于 $f$ 是一个模拟，如果 $b<f(a)$，那么我们有 $a'<a$ 使得 $f(a')=b$。
根据归纳假设，我们也有 $g(a')=b$，因此 $b<g(a)$。
对称的论证也是对称的。
\end{proof}

因此，如果 $A$ 和 $B$ 都装备有外延和良基的关系，我们可以写作 $A\le B$ 表示存在一个从 $A$ 到 $B$ 的模拟。
\cref{thm:wfcat} 意味着如果 $A\le B$ 并且 $B\le A$，那么 $A=B$。

\begin{defn}
一个\define{序数 (ordinal)} \indexdef{ordinal} \indexsee{number!ordinal}{ordinal} 是一个集合 $A$，具有一个外延良基关系，并且该关系是\emph{传递的}，即满足 $\fall{a,b,c:A}(a<b)\to (b<c) \to (a<c)$。
\end{defn}

\begin{eg}
当然，\nat 上的通常严格序是传递的。
它也容易看出是外延的；因此它是一个序数。
如常所示，我们用 $\omega$ 来表示这个序数。
\end{eg}

\symlabel{ord}
令 \ord 表示序数的类型。
根据之前的结果，\ord 是一个集合，并且具有一个自然的偏序关系。
我们现在证明 \ord 还承认一个良基关系。

\symlabel{initial-segment}
如果 $A$ 是一个序数，并且 $a:A$，令 $\ordsl A a \defeq \setof{ b:A | b<a}$ 表示初始段。
\index{initial!segment}%
注意，如果 $\ordsl A a = \ordsl A b$ 作为序数，那么该同构必然尊重它们在 $A$ 中的包含（因为模拟构成一个偏序集），因此它们作为 $A$ 的子集是相等的。
因此，由于 $A$ 是外延的，$a=b$。
因此函数 $a\mapsto \ordsl A a$ 是一个从 $A$ 到 \ord 的单射。

\begin{defn}
对于序数 $A$ 和 $B$，一个模拟 $f:A\to B$ 称为\define{有界的 (bounded)} \indexdef{simulation!bounded} \indexdef{bounded!simulation} 如果存在 $b:B$ 使得 $A = \ordsl B b$。
\end{defn}

上述评论意味着当它存在时，这样的 $b$ 是唯一的，因此有界性是一个纯命题。

我们写作 $A<B$ 表示存在一个从 $A$ 到 $B$ 的有界模拟。
由于模拟是唯一的，$A<B$ 也是一个纯命题。

\begin{thm}\label{thm:ordord}
$(\ord,<)$ 是一个序数。
\end{thm}

\noindent
更精确地说，这个定理表明，序数类型 \ord_{\UU_i} 在一个宇宙中本身也是下一个更高宇宙中的一个序数，即 $(\ord_{\UU_i},<):\ord_{\UU_{i+1}}$。

\begin{proof}
设 $A$ 是一个序数；我们首先证明对于所有 $a:A$，$\ordsl A a$ 是可达的（在 \ord 中）。
通过对 $A$ 进行良基归纳，假设对于所有 $b<a$，$\ordsl A b$ 是可达的。
根据可达性的定义，我们必须证明对于所有 $B<\ordsl A a$，$B$ 是可达的。
但是，如果 $B<\ordsl A a$，那么存在一些 $b<a$ 使得 $B = \ordsl{(\ordsl A a)}{b} = \ordsl A b$，这是通过归纳假设可达的。
因此，$\ordsl A a$ 对所有 $a:A$ 是可达的。

现在为了证明 $A$ 在 \ord 中是可达的，根据定义，我们必须证明对于所有 $B<A$，$B$ 是可达的。
但如前所述，$B<A$ 意味着 $B=\ordsl A a$ 对于某个 $a:A$，它是我们刚刚证明的可达的。
因此，\ord 是良基的。

对于外延性，假设 $A$ 和 $B$ 是序数，并且
\narrowequation{\prd{C:\ord} (C<A) \Leftrightarrow (C<B).}
那么对于每个 $a:A$，由于 $\ordsl A a<A$，我们有 $\ordsl A a<B$，因此存在 $b:B$ 使得 $\ordsl A a = \ordsl B b$。
定义 $f:A\to B$ 将每个 $a$ 映射到相应的 $b$；很容易验证 $f$ 是一个同构。
因此 $A\cong B$，因此根据公理 $A=B$。

最后，很容易看出 $<$ 是传递的。
\end{proof}

将 \ord 视为一个序数通常非常方便，但它也有一些陷阱。
例如，考虑下面的引理，我们注意到如何使用宇宙。

\begin{lem}\label{thm:ordsucc}
令 \bbU 为一个宇宙。
对于任何 $A:\ord_\bbU$，存在一个 $B:\ord_\bbU$ 使得 $A<B$。
\end{lem}
\begin{proof}
令 $B=A+\unit$，其中元素 $\ttt:\unit$ 大于 $A$ 的所有元素。
那么 $B$ 是一个序数，并且很容易看出 $A\cong \ordsl B \ttt$。
\end{proof}

在 \cref{thm:ordsucc} 的证明中构造的序数 $B$ 被称为 $A$ 的\define{后继 (successor)}\indexdef{successor!of an ordinal}。

这个引理说明了在使用“典型含糊 (typically ambiguous)”\index{typical ambiguity} 的风格来使用 \UU 表示一个任意、未指定的宇宙时可能出现的陷阱。
考虑下面的另一种证明方法。

\begin{proof}[另一个 \cref{thm:ordsucc} 的证明]
注意 $C<A$ 当且仅当 $C=\ordsl A a$ 对于某个 $a:A$。
这给出了一个同构 $A \cong \ordsl \ord A$，因此 $A<\ord$。
因此我们可以取 $B\defeq\ord$。
\end{proof}

第二种证明方法在我们以典型含糊的风格陈述 \cref{thm:ordsucc} 时是有效的。
但是得到的引理将不那么有用，因为第二个证明将限制引理陈述中的第二个“\ord”与第一个相比指的是更高的宇宙级别。
第一个证明允许两个宇宙是相同的。

类似的评论适用于下一个引理，它可以通过观察到对于任何 $A:\ord$，$A\le \ord$ 来证明。
\begin{lem}\label{thm:ordunion}
  令 \bbU 为一个宇宙。
  对于任何 $X:\type$ 和 $F:X\to \ord_\bbU$，存在一个 $B:\ord_\bbU$ 使得 $Fx\le B$ 对于所有 $x:X$。
\end{lem}
\begin{proof}
  令 $B$ 为等价关系 $\eqr$ 在 $\sm{x:X} Fx$ 上的商集（见 \cref{rmk:quotient-of-non-set}）定义如下：
  \[ (x,y) \eqr (x',y')
  \;\defeq\;
  \Big(\ordsl{(Fx)}{y} \cong \ordsl{(Fx')}{y'}\Big).
  \]
  定义 $(x,y)<(x',y')$ 如果 $\ordsl{(Fx)}{y} < \ordsl{(Fx')}{y'}$。
  这显然传递到商集，并且可以看出使得 $B$ 成为一个序数。
  此外，对于每个 $x:X$，诱导的映射 $Fx\to B$ 是一个模拟。
\end{proof}

\section{经典良序 (Classical well-orderings)}
\label{sec:wellorderings}

\index{denial|(}%
现在我们来展示我们定义的序数 (ordinal) 与更为熟悉的经典良序 (classical well-orderings) 之间的等价性。

\begin{lem}
\index{排中律 (excluded middle)}%
在假设排中律的情况下，每一个序数 (ordinal) 都是三分性的 (trichotomous)：
\index{trichotomy of ordinals (序数的三分性)}%
\index{ordinal (序数)!trichotomy of (三分性)}%
\[ \fall{a,b:A} (a<b) \vee (a=b) \vee (b<a). \]
\end{lem}
\begin{proof}
通过对 $a$ 进行归纳，我们可以假设对于每一个 $a'<a$ 和每一个 $b':A$，我们有 $(a'<b') \vee (a'=b') \vee (b'<a')$。
现在通过对 $b$ 进行归纳，我们可以假设对于每一个 $b'<b$，我们有 $(a<b') \vee (a=b') \vee (b'<a)$。

根据排中律，存在一个 $b'<b$ 使得 $a<b'$，或者存在一个 $b'<b$ 使得 $a=b'$，或者对于所有的 $b'<b$ 我们有 $b'<a$。
在第一种情况下，仅 $a<b$ 通过传递性成立，因此 $a<b$ 作为一个命题成立。
同样地，在第二种情况下，$a<b$ 通过传递成立。
因此，假设 $\fall{b':A}(b'<b)\to (b'<a)$。

现在类似地，要么存在 $a'<a$ 使得 $b<a'$，要么存在 $a'<a$ 使得 $a'=b$，要么对于每个 $a'<a$ 我们有 $a'<b$。
在第一种和第二种情况下，$b<a$，因此我们可以假设 $\fall{a':A}(a'<a)\to (a'<b)$。
然而，通过外延性 (extensionality)，我们的两个假设现在意味着 $a=b$。
\end{proof}

\begin{lem}
一个良基关系 (well-founded relation) 不包含循环，也就是说
\[ \fall{n:\mathbb{N}}{a:\mathbb{N}_n\to A} \neg\Big((a_0<a_1) \wedge \dots \wedge (a_{n-1}<a_n)\wedge (a_n<a_0)\Big). \]
\end{lem}
\begin{proof}
我们通过对 $a:A$ 进行归纳证明不存在包含 $a$ 的循环。
因此，假设通过归纳，对于所有的 $a'<a$，不存在包含 $a'$ 的循环。
但是在任何包含 $a$ 的循环中，都存在一些元素小于 $a$ 并包含在相同的循环中。
\end{proof}

\indexdef{relation!irreflexive (反自反的关系)}%
\index{irreflexivity (反自反性)!of well-founded relation (良基关系的反自反性)}%
特别是，一个良基关系必须是\define{反自反的} (irreflexive)，即对于所有的 $a$，$\neg(a<a)$。

\begin{thm}\label{thm:wellorder}
在假设排中律的情况下，$(A,<)$ 是一个序数 (ordinal) 当且仅当每个非空子集 $B\subseteq A$ 都有一个最小元素。
\end{thm}
\begin{proof}
如果 $A$ 是一个序数，那么根据 \cref{thm:wfmin}，每个非空子集仅存在一个最小元素。
但是三分性 (trichotomy) 意味着任何最小元素都是一个最小元素。
此外，最小元素存在时是唯一的，因此仅有一个最小元素等同于存在一个最小元素。

反之，如果每个非空子集都有一个最小元素，那么根据 \cref{thm:wfmin}，$A$ 是良基的。
我们也有三分性，因为对于任何 $a,b$，子集
$ \setof{a,b} \defeq \setof{x:A | x=a \lor x=b} $
仅有一个最小元素，这个元素必定是 $a$ 或者 $b$。
这意味着传递性 (transitivity)，因为如果 $a<b$ 并且 $b<c$，那么 $a=c$ 或者 $c<a$ 将产生一个循环。
类似地，它也意味着外延性，因为如果 $\fall{c:A}(c<a)\Leftrightarrow (c<b)$，那么 $a<b$ 意味着 (取 $c$ 为 $a$) $a<a$，这将产生一个循环，反之亦然；因此 $a=b$。
\end{proof}

在经典\index{mathematics!classical (数学!经典的)}数学中，\cref{thm:wellorder} 中的特征被视为\emph{良序} (well-ordering) 的定义，其中\emph{序数} (ordinals) 是同构类的良序的一个典型代表。在我们的语境中，结构同一性原理 (structure identity principle) 意味着不需要寻找这样的代表：任何一个良序与另一个都是同样好的。

我们现在继续讨论选择公理 (axiom of choice) 的后果。
对于任何集合 $X$，让 $\powerp X$ 表示 $X$ 的仅有居住的子集类型：
\symlabel{inhabited-powerset (居住的幂集)}
\[ \powerp X \defeq \setof{ Y : \power X | \exis{x:X} x\in Y}. \]
在假设排中律的情况下，这等价于 $X$ 的\emph{非空} (nonempty) 子集的类型，并且我们有 $\power X \eqvsym (\powerp X) + \unit$。

\begin{thm}\label{thm:wop}
\index{axiom!of choice (选择公理)}%
\index{排中律 (excluded middle)}%
在假设排中律的情况下，以下条件等价：
\begin{enumerate}
\item 对于每个集合 $X$，仅存在一个函数
$ f: \powerp X \to X $
使得对于所有 $Y:\powerp X$ 有 $f(Y)\in Y$。\label{item:wop1}
\item 每个集合仅具有序数结构。\label{item:wop2}
\end{enumerate}
\end{thm}

\noindent
当然，~\ref{item:wop1} 是选择公理的一种标准经典\index{mathematics!classical (数学!经典的)}版本；参见 \cref{ex:choice-function}。

\begin{proof}
一个方向是容易的：假设~\ref{item:wop2}。
因为我们要证明仅作为命题的~\ref{item:wop1}，我们可以假设 $A$ 是一个序数。
但随后我们可以定义 $f(B)$ 为 $B$ 的最小元素。

现在假设~\ref{item:wop1}。
同样，由于~\ref{item:wop2} 是一个命题，我们可以假设给定这样的一个 $f$。
我们将 $f$ 扩展为一个函数
\[ \bar f:\power X \eqvsym (\powerp X) + \unit \longrightarrow X+\unit \]
以显而易见的方式。
现在对于任何一个序数 $A$，我们可以通过良基递归定义 $g_A:A\to X+\unit$：
\[ g_A(a) \defeq
\bar f\Big(X \setminus \setof{ g_A(b) | \strut (b<a) \wedge (g_A(b) \in X) }\Big)
\]
(将 $X$ 视为 $X+\unit$ 的一个子集显然)。

设 $A'\defeq \setof{a:A | g_A(a) \in X}$ 为 $g_A$ 的预像；然后我们声明 $g_A':A' \to X$ 是单射 (injective)。
因为如果 $a,a':A$ 且 $a\neq a'$，那么根据三分性，我们可以假设 $a'<a$。
因此 $g_A(a') \in \setof{ g_A(b) | b<a }$，所以由于对于所有 $Y$ 有 $f(Y)\in Y$，我们有 $g_A(a) \neq g_A(a')$。

此外，$A'$ 是 $A$ 的一个初始片段 (initial segment)。
因为 $g_A(a)$ 落在 \unit 中当且仅当 $\setof{g_A(b)|b<a} = X$，并且如果这是成立的，那么对于任何 $a'>a$ 这也是成立的。
因此，$A'$ 本身是一个序数。

最后，由于 \ord 是一个序数，我们可以取 $A\defeq\ord$。
设 $X'$ 为 $g_\ord':\ord' \to X$ 的像；然后 $g_\ord'$ 的逆函数给出了一个单射 $H:X'\to \ord$。
根据 \cref{thm:ordunion}，存在一个序数 $C$ 使得对于所有 $x:X'$，$Hx\le C$。
然后根据 \cref{thm:ordsucc}，存在一个更大的序数 $D$ 使得 $C<D$，因此对于所有 $x:X'$，$Hx<D$。
现在我们有
\begin{align*}
g_{\ord}(D) &= \bar f\Big( X \setminus \setof{ g_\ord(B) | \rule{0pt}{1em} B<D \wedge (g_\ord(B) \in X)} \Big)\\
&=\bar f\Big( X \setminus \setof{ g_\ord(B) | \rule{0pt}{1em} g_\ord(B) \in X} \Big)
\end{align*}
因为如果 $B:\ord$ 并且 $(g_\ord(B) \in X)$，那么 $B = Hx$ 对于某些 $x:X'$，因此 $B<D$。
现在如果
\[\setof{ g_\ord(B) | \rule{0pt}{1em} g_\ord(B) \in X}\]
不是全部的 $X$，那么 $g_\ord(D)$ 将在 $X$ 中但不在这个子集中，这将与 $D$ 自己作为 $B$ 的一个可能值相矛盾。
所以这个集合必须是全部的 $X$，因此 $g_\ord'$ 是满射 (surjective) 的同时也是单射的。
因此，我们可以将 \ord' 上的序数结构传递给 $X$。
\end{proof}

\begin{rmk}
如果我们使用了错误的 \cref{thm:ordsucc} 或 \cref{thm:ordunion} 的证明，那么 \cref{thm:wop} 的结果证明将是无效的：将无法一致地分配宇宙级别\index{universe level (宇宙级别)}。如现在所示，我们需要命题调整 (propositional resizing)（这由 \LEM{} 导出）来确保 $X'$ 处于与 $X$ 相同的宇宙中（直到等价）。
\end{rmk}

\begin{cor}
在假设选择公理的情况下，函数 $\ord\to\set$（它忽略了序结构）是一个满射。
\end{cor}

注意，\ord 是一个集合，而 \set 是一个1类型 (1-type)。
一般来说，没有理由让一个1类型接受来自集合的任何满射。
即使选择公理似乎也不意味着\emph{每一个}1类型都如此（尽管参见 \cref{ex:acnm-surjset}），但它很容易意味着对从 \set 构造出的1类型（例如在 \cref{sec:sip} 中的结构的类别对象类型）是如此。
以下的推论也适用于这样的类别。

\begin{cor}
\index{weak equivalence (弱等价)!of precategories (的前类)}%
在假设 \choice{} 的情况下，\uset 接受来自严格类别的弱等价函子。
\end{cor}
\begin{proof}
设 $X_0\defeq \ord$，并且对于 $A,B:X_0$，设 $\hom_X(A,B) \defeq (A\to B)$。
那么 $X$ 是一个严格类别，因为 \ord 是一个集合，并且上述满射 $X_0 \to \set$ 扩展为一个弱等价函子 $X\to \uset$。
\end{proof}

现在回顾 \cref{sec:cardinals}，我们有进一步的满射 $\cd{\blank}:\set\to\card$，因此有一个复合满射 $\ord\to\card$ 将每个序数映射到其基数 (cardinality)。

\begin{thm}
在假设 \choice{} 的情况下，满射 $\ord\to\card$ 有一个截面 (section)。
\end{thm}
\begin{proof}
有一个简单且错误的证明：因为 \ord 和 \card 都是集合，\choice{} 意味着任何满射之间\emph{仅}有一个截面。
然而，我们实际上有一个规范的\emph{指定}截面：因为 \ord 是一个序数，每个非空子集都有一个唯一指定的最小元素。
因此，我们可以将每个基数映射到对应纤维中的最小元素。
\end{proof}

在集合论中，传统上将基数与其在 \ord 中的像相识别：具有该基数的最小序数。

这意味着 \card 也可以规范地接受一个序数结构：实际上，它与 \ord 同构。
具体来说，我们通过良基递归定义了一个函数 $\aleph:\ord\to\ord$，使得 $\aleph(A)$ 是具有大于 $\aleph({\ordsl A a})$ 的基数的最小序数，对于所有 $a:A$。
然后（假设 \choice{}），$\aleph$ 的像正好是 \card 的像。

\index{denial|)}%

\index{ordinal|)}%

\section{累积层次 (The cumulative hierarchy)}
\label{sec:cumulative-hierarchy}

\index{bargaining|(}%
我们可以将给定宇宙 $\UU$ 中的所有集合的累积层次 $V$ 定义为一个高阶归纳类型 (higher inductive type)，使得 $V$ 再次是一个集合（在更大的宇宙 $\UU'$ 中），配备一个二元“成员”关系 $x\in y$，它满足集合论的通常定律。

\begin{defn}\label{defn:V}
相对于类型宇宙 $\UU$ 的\define{累积层次 (cumulative hierarchy)}
\indexdef{cumulative (累积)!hierarchy, set-theoretic (层次，集合论)}%
\indexdef{hierarchy (层次)!cumulative, set-theoretic (累积，集合论)}%
$V$ 是由以下构造函数生成的高阶归纳类型：
%
\begin{enumerate}
\item 对于每个 $A : \UU$ 和 $f : A \to V$，有一个元素 $\vset(A, f) : V$。
\item 对于所有 $A, B : \UU$，$f : A \to V$ 和 $g : B \to V$，满足
%
\begin{narrowmultline} \label{eq:V-path}
\big(\fall{a:A} \exis{b:B} \id[V]{f(a)}{g(b)}\big) \land \narrowbreak
\big(\fall{b:B} \exis{a:A} \id[V]{f(a)}{g(b)}\big)
\end{narrowmultline}
%
存在一个路径 $\id[V]{\vset(A,f)}{\vset(B,g)}$。
\item 0-截断构造函数：对于所有 $x,y:V$ 和 $p,q:x=y$，我们有 $p=q$。
\end{enumerate}
\end{defn}

在集合论的语言中，$\vset(A,f)$ 可以理解为（经典集合论意义上的）集合，它是 $A$ 在 $f$ 下的像，即 $\setof{ f(a) | a \in A }$。
然而，我们将避免这种表示法，因为它会与我们的子类型 (subtypes) 表示法发生冲突（但参见~\eqref{eq:class-notation} 和 \cref{def:TypeOfElements}）。

层次 $V$ 是从空映射 $\rec\emptyt(V) : \emptyt \to V$ 启动的，它给出了空集 $\emptyset = \vset(\emptyt,\rec\emptyt(V))$。
然后通过 $\unit \to V$ 的定义 $\ttt \mapsto \emptyset$ 进入 $V$，以此类推。
（该定义也可以调整为包括任意的“原子” (atoms) 或“无元素” (urelements) 集合，通过添加额外的点构造函数。）
类型 $V$ 存在于与基础宇宙 $\UU$ 相同的宇宙中。

$V$ 的第二个构造函数的形式与我们以前见过的任何东西都不同：它不仅涉及 $V$ 中的路径（在 \cref{sec:hittruncations} 中我们声称这些路径稍有问题），而且还涉及它们的和的截断。
显然，它不符合在 \cref{sec:naturality} 中描述的一般方案，因此其归纳原理是什么可能并不明显。
幸运的是，就像我们在 \cref{sec:hittruncations} 中对 0-截断的第一次定义一样，它可以通过辅助高阶归纳类型重新表达。
我们将细节留给读者去思考（参见 \cref{ex:cumhierhit}）。

\index{induction principle!for cumulative hierarchy (累积层次的归纳原理)}%
最后，$V$ 的归纳原理（用模式匹配语言书写）表明，给定 $P:V\to \set$，为了构造 $h:\prd{x:V} P(x)$，只需给出以下内容即可。
\begin{enumerate}
\item 对于任意 $f:A\to V$，构造 $h(\vset(A,f))$，假设给定了所有 $a:A$ 的 $h(f(a))$。
\item 验证如果 $f : A \to V$ 和 $g : B \to V$ 满足~\eqref{eq:V-path}，则 $\dpath{P}{q}{h(\vset(A,f))}{h(\vset(B,g))}$，其中 $q$ 是从 $V$ 的第二个构造函数和~\eqref{eq:V-path} 中生成的路径，假设 $h(f(a))$ 和 $h(g(b))$ 已经为所有 $a:A$ 和 $b:B$ 定义，并且满足以下条件：
\begin{eqnarray*}
&       & \big(\fall{a:A} \exis{b:B} \exis{p:f(a)=g(b)} \dpath{P}{p}{h(f(a))}{h(g(b))}\big) \\
& \land & \big(\fall{b:B} \exis{a:A} \exis{p:f(a)=g(b)} \dpath{P}{p}{h(f(a))}{h(g(b))}\big)
\end{eqnarray*}
\end{enumerate}
第二个条款检查正在定义的映射是否尊重在 \eqref{eq:V-path} 中引入的路径。
像往常一样，当我们使用模式匹配来陈述高阶归纳原理时，它可能看起来像是一种同义反复，但实际上并非如此。
关键在于“$h(f(a))$”本质上是一个形式符号，我们不能窥视其内部，$h(\vset(A,f))$ 必须根据其定义。
因此，在第二个条款中，我们在适当的时候假设这些形式符号的等价性，并验证由第一条款的构造产生的元素是否也相等。
当然，如果 $P$ 是一个命题族，那么第二条款是自动成立的。

注意，通过归纳，对于每个 $v:V$，仅存在 $A:\UU$ 和 $f:A\to V$ 使得 $v=\vset(A,f)$。
因此，定义 $V$ 上的\define{成员关系 (membership relation)} $x\in v$ 是合理的：
%
% Note: "membership" rather than "elementhood", because "element" is taken.
%
\symlabel{V-membership (V 的成员关系)}
\begin{equation*}
(x \in \vset(A,f)) \defeq (\exis{a : A} x = f(a)).
\end{equation*}
%
要证明该定义是有效的，我们必须使用 $V$ 的递归原理。因此，假设我们有一个通过~\eqref{eq:V-path} 构造的路径 $\vset(A, f) = \vset(B, g)$。
如果 $x \in \vset(A,f)$，则仅有一个 $a : A$ 使得 $x = f(a)$，但是根据~\eqref{eq:V-path} 仅有一个 $b : B$ 使得 $f(a) = g(b)$，因此 $x = g(b)$ 并且 $x \in \vset(B,g)$。
反之亦然。

\define{子集关系 (subset relation)}
\indexdef{subset (子集)!relation on the cumulative hierarchy (累积层次上的关系)}%
$x\subseteq y$ 在 $V$ 上的定义与通常一样
%
\begin{equation*}
(x \subseteq y) \defeq \fall{z : V} z \in x \Rightarrow z \in y.
\end{equation*}

\define{类 (class)}
\indexdef{class (类)}%
可以被认为是 $V$ 上的一个命题谓词。我们可以说一个类 $C : V \to \prop$ 是一个\define{$V$-集合 ($V$-set)}，
\indexdef{set (集合)!in the cumulative hierarchy (在累积层次中)}%
如果仅存在 $v:V$ 使得
%
\begin{equation*}
\fall{x : V} C(x) \Leftrightaway x \in v.
\end{equation*}
我们还可以使用类的常规表示法，它与我们的标准子类型 (subtypes) 表示法相匹配：
\begin{equation}
\setof{ x | C(x) } \defeq \lam{x}C(x).\label{eq:class-notation}
\end{equation}
%
一个类 $C: V\to \prop$ 将被称为\define{$\UU$-小} ($\UU$-small)，
\indexdef{class (类)!small (小)}%
\indexdef{small (小)!class (类)}%
如果其所有值 $C(x)$ 都处于 $\UU$ 中，特别是 $C: V\to \prop_{\UU}$。
由于 $V$ 存在于与基础宇宙 $\UU$ 相同的宇宙 $\UU'$ 中，因此对于任何 $v,w:V$，它们的同一性类型 $v=_V w$ 也是如此。为了在没有命题调整的情况下获得良好表现，
\index{propositional!resizing (命题调整)}%
\index{resizing (调整)}%
我们可以定义一个 $\UU$-小的“调整”身份关系，我们可以通过归纳如下定义。

\begin{defn}\label{def:bisimulation (双模拟)}
定义\define{双模拟 (bisimulation)}%
\indexdef{bisimulation (双模拟)}%
关系
%
\begin{equation*}
\mathord\bisim : V \times V \longrightarrow \prop_{\UU}
\end{equation*}
%
通过在 $V$ 上进行双重归纳，其中对于 $\vset(A,f)$ 和 $\vset(B,g)$ 我们有：
\begin{narrowmultline*}
\vset(A,f)  \bisim \vset(B,g) \defeq \narrowbreak
\big(\fall{a:A}\exis{b:B} f(a)  \bisim g(b)\big) \land
\big(\fall{b:B}\exis{a:A} f(a) \bisim g(b)\big).
\end{narrowmultline*}
\end{defn}
%
要验证该定义的正确性，我们只需检查它是否尊重通过~\eqref{eq:V-path} 构造的路径，但这是显而易见的，并且 $\prop_{\UU}$ 是一个集合，这也是显而易见的。请注意，$u \bisim v$ 是在构造中处于 $\propU$ 的。

\begin{lem}\label{lem:BisimEqualsId}
对于任意 $u,v:V$ 我们有 $(u=_V v) = (u \bisim v)$。
\end{lem}

\begin{proof}
一个简单的归纳法表明 $\bisim$ 是自反的，因此通过传递性，我们有 $(u=_V v)\to (u \bisim v)$。
因此，剩下的要证明的是 $(u \bisim v)\to (u=_V v)$。
通过对 $u$ 和 $v$ 的归纳，我们可以假设它们分别是 $\vset(A,f)$ 和 $\vset(B,g)$。
（我们可以忽略 $V$ 的路径构造子，因为 $(u \bisim v)\to (u=_V v)$ 是一个单纯命题。）
然后根据定义，$\vset(A,f)\bisim\vset(B,g)$ 意味着 $(\fall{a:A}\exis{b:B}f(a)  \bisim g(b))$，反之亦然。
但是根据归纳假设，我们可以得出 $(\fall{a:A}\exis{b:B}f(a) = g(b))$，反之亦然。
所以根据 $V$ 的路径构造子，我们有 $\vset(A,f) =_V \vset(B,g)$。
\end{proof}

有人可能会认为我们可以省略 $V$ 的 0-截断构造子，并通过将 \cref{thm:h-set-refrel-in-paths-sets} 应用于仿真来\emph{证明} $V$ 是 0-截断的。
然而，在 \cref{lem:BisimEqualsId} 的证明中，我们使用了 $V$ 是 0-截断的事实，得出 $(u \bisim v)\to (u=_V v)$ 是一个单纯命题，因此在归纳中我们可以假设 $u$ 和 $v$ 是 $\vset(A,f)$ 和 $\vset(B,g)$。

现在我们可以使用调整大小的恒等关系来得到以下有用的原理。

\begin{lem}\label{lem:MonicSetPresent}
对于每个 $u:V$，存在一个给定的 $A_u:\UU$ 和单射 $m_u: A_u \mono V$，使得 $u = \vset(A_u, m_u)$。
\end{lem}

\begin{proof}
取任意表示 $u = \vset(A,f)$ 并将 $f:A\to V$ 分解为一个满射后跟一个单射：
%
\begin{equation*}
f = m_u\circ e_u : A \epi A_u \mono V.
\end{equation*}
%
显然，如果 $A_u$ 仍在 $\UU$ 中，则 $u = \vset(A_u, m_u)$ 成立，这在 $e_u : A \epi A_u$ 的核在 $\UU$ 中时成立。但是 $e_u : A \epi A_u$ 的核是 $f : A\to V$ 上的恒等的拉回，我们刚刚证明它在等价的意义下是 $\UU$-小的。现在，从 $u:V$ 构造出 $m_u :A_u \mono V$ 和 $u = \vset(A_u, m_u)$ 的对 $(A_u, m_u)$ 是在 $V$ 上等价的唯一的，因此通过单一选择原理 \eqref{cor:UC}，存在一个映射 $c : V\to\sm{A:\UU}(A\to V)$，使得 $c(u) = (A_u, m_u)$，其中 $m_u :A_u \mono V$ 并且 $u = \vset(c(u))$，如所述。
\end{proof}

\begin{defn}\label{def:TypeOfElements}
对于 $u:V$，刚刚构造的单射表示 $m_u: A_u \mono V$ 使得 $u = \vset(A_u, m_u)$ 可以称为 $u$ 的\define{成员类型 (type of members)}，记为 $m_u : [u] \mono V$，或者简写为 $[u] \mono V$。我们可以将 $[u]$ 视为“由 $u$ 的成员组成的 $V$ 的子类”。
\end{defn}

\begin{thm}\label{thm:VisCST}
\index{axiom!of set theory, for the cumulative hierarchy}%
以下关于 $(V, {\in})$ 成立：
%
\begin{enumerate}
\item \emph{外延性 (extensionality):}
%
\begin{equation*}
\fall{x, y : V} x \subseteq y \land y \subseteq x \Leftrightarrow x = y.
\end{equation*}
%
\item \emph{空集 (empty set):} 对于所有 $x:V$，我们有 $\neg (x\in \emptyset)$。
%
\item \emph{配对 (pairing):} 对于所有 $u, v:V$，类 $\{u, v\} \defeq \setof{ x | x = u \vee x = v}$ 是一个 $V$-集合。
%
\item \emph{无穷 (infinity):}\index{axiom!of infinity} 存在 $v:V$ 使得 $\emptyset\in v$ 且 $x\in v$ 意味着 $x\cup \{x\}\in v$。
%
\item \emph{并集 (union):} 对于所有 $v:V$，类 $\cup v\defeq \setof{ x | \exis{u:V} x \in u \in v}$ 是一个 $V$-集合。
%
\item \emph{函数集 (function set):} 对于所有 $u, v:V$，类 $v^u \defeq \setof{ x | x : u\to v}$ 是一个 $V$-集合。%
\footnote{这里 $x:u\to v$ 的意思是 $x$ 是一组适当的有序对，根据集合论中编码函数的常规方式。}
%
\item \emph{$\in$-归纳 (induction):} 如果 $C : V \to \prop$ 是一个类，并且当对所有 $x\in a$ 都有 $C(x)$ 时 $C(a)$ 成立，那么对于所有 $v:V$，$C(v)$ 成立。
%
\item \emph{替代 (replacement):}\index{axiom!of replacement} 给定任何 $r : V \to V$ 和 $x : V$，类
%
\begin{equation*}
\setof{ y | \exis{z : V} z \in x \land y = r(z)}
\end{equation*}
%
是一个 $V$-集合。
%
\item \emph{分离 (separation):}\index{axiom!of separation} 给定任何 $a : V$ 和 $\UU$-小 $C : V \to \propU$，类
%
\begin{equation*}
\setof{ x | x \in a \land C(x)}
\end{equation*}
%
是一个 $V$-集合。
\end{enumerate}
\end{thm}

\begin{proof}[证明 (Sketch of proof)]
\mbox{}
%
\begin{enumerate}
\item \emph{外延性 (Extensionality):} 如果 $\vset(A,f) \subseteq \vset(B, g)$，那么对于每个 $a : A$，有 $f(a) \in \vset(B, g)$，因此对于每个 $a : A$，仅存在 $b : B$ 使得 $f(a) = g(b)$。假设 $\vset(B, g) \subseteq \vset(A, f)$ 得到了 \eqref{eq:V-path} 的另一半，因此 $\vset(A,f) = \vset(B,g)$。

\item \emph{空集 (Empty set):} 假设 $x\in \emptyset = \vset(\emptyt,\rec\emptyt(V))$。那么 $\exis{a:\emptyt}x=\, \rec\emptyt(V,a)$，这是荒谬的。

\item \emph{配对 (Pairing):} 给定 $u$ 和 $v$，令 $w=\vset(\bool,\rec\bool(V,u,v))$。
\index{pair!unordered}

\item \emph{无穷 (Infinity):} 取 $w = \vset(\nat,I)$，其中 $I: \nat \to V$ 由递归 $I(0) \defeq \emptyset$ 和 $I(n+1) \defeq I(n)\cup \{I(n)\}$ 给出。

\item \emph{并集 (Union):} 取任意 $v:V$ 和任意表示 $f :A\to V$，使得 $v=\vset(A,f)$。然后令 $\tilde{A} \defeq \sm{a:A}[fa]$，其中 $m_{fa} : [fa] \mono V$ 是来自 \cref{def:TypeOfElements} 的成员类型。显然 $\tilde{A}$ 是 $\UU$-小的，我们定义 $\cup v \defeq \vset(\tilde{A}, \lam{x} m_{f(\proj1(x))}(\proj2(x)))$。

\item \emph{函数集 (Function set):} 给定 $u, v:V$，取成员类型 $[u] \mono V$ 和 $[v] \mono V$ 以及函数类型 $[u]\to [v]$。我们想要定义一个映射
\[
r: ([u]\to [v])\ \longrightarrow\ V
\]
其中“$r(f) = \setof{ \pairr{x, f(x)} | x : [u] }$”，但为了使其有意义，我们首先必须定义有序对 $\pairr{x, y}$，然后我们取映射 $r': x \mapsto \pairr{x, f(x)}$，然后我们可以定义 $r(f)\defeq \vset([u], r')$。但有序对可以根据通常的无序配对定义。

\item \emph{$\in$-归纳 ($\in$-induction):} 令 $C : V \to \prop$ 为一个类，假设当对所有 $x\in a$ 都有 $C(x)$ 时 $C(a)$ 成立，并且取任意 $v=\vset(B,g)$。为了通过归纳证明 $C(v)$，假设对所有 $b:B$，有 $C(g(b))$。对于每个 $x\in v$，仅存在 $b:B$，使得 $x = g(b)$，因此 $C(x)$ 成立。因此 $C(v)$ 成立。

\item \emph{替代 (Replacement):} 令 $C$ 表示上述的类。
声明“$C$ 是一个 $V$-集合”是一个单纯命题，因此我们可以通过如下归纳进行推导。假设 $x$ 是 $\vset(A, f)$，我们断言 $w
\defeq \vset(A, r \circ f)$ 是我们寻找的集合。如果 $C(y)$ 成立，那么仅存在
$z : V$ 和 $a : A$ 使得 $z = f(a)$ 且 $y = r(z)$，因此 $y \in w$。
反之，如果 $y \in w$，那么仅存在 $a : A$ 使得 $y = r(f(a))$，因此
如果我们取 $z \defeq f(a)$，我们可以看到 $C(y)$ 成立。

\item 令我们称一个类 $C: V\to\prop$ 是\define{可分离的 (separable)}，如果对于任何 $a:V$，类
%
\symlabel{class-intersection}
\begin{equation*}
a \cap C \defeq\setof{x | x\in a \wedge C(x)}
\end{equation*}
%
是一个 $V$-集合。
我们需要证明任何 $\UU$-小的 $C: V \to \propU$ 是可分离的。事实上，给定 $a=\vset(A,f)$，令 $A' = \sm{x:A}C(fx)$，并取 $f' = f\circ i$，其中 $i : A' \to A$ 是明显的包含映射。然后我们可以取 $a' = \vset(A',f')$，并且有 $x\in a\wedge C(x) \Leftrightarrow x\in a'$，如所述。我们需要假设 $C$ 的值域在 $\UU$ 中，以便 $A' = \sm{x:A}C(fx)$ 在 $\UU$ 中。\qedhere
\end{enumerate}
\end{proof}

我们还可以使用一个严格的句法标准来判断可分离性，以便从类的表达式中读出它是否产生了一个 $V$-集合。一个熟悉的条件是 $\Delta_0$，这意味着表达式是由等式 $x=_V y$ 和隶属关系 $x\in y$ 通过仅限于单纯命题的连接词 $\neg$，$\land$，$\lor$，$\Rightarrow$ 和量词 $\forall$，$\exists$ （即所谓的\define{有界量词 (bounded quantifiers)}）构建的。

\begin{cor}\label{cor:Delta0sep}
如果类 $C: V \to \prop$ 是上述意义上的 $\Delta_0$，那么它是可分离的。
\end{cor}
\index{axiom!of $\Delta_0$-separation}%

\begin{proof}
记住我们有一个 $\UU$-小的 $\bisim$ 恒等关系 $x = y$。由于 $x\in y$ 是根据 $x=y$ 定义的，我们也有一个 $\UU$-小的隶属关系的调整大小
%
\symlabel{resized-membership}
\begin{equation*}
x\bin\vset(A,f) \defeq \exis{a:A} x \bisim f(a)。
\end{equation*}
%
现在，设 $\Phi$ 为 $C$ 的 $\Delta_0$ 表达式，因此作为类 $\Phi = C$（严格来说，我们应该区分表达式和它们的意义，但我们将模糊它们之间的差异）。令 $\widetilde{\Phi}$ 为将所有出现的 $=$ 和 $\in$ 替换为它们的调整后的等价物 $\bisim$ 和 $\bin$ 的结果。显然，$\widetilde{\Phi}$ 也表达了 $C$，就类 $x:V$ 而言，$\widetilde{\Phi}(x) \Leftrightarrow C(x)$，因此根据同一性原理，$\widetilde{\Phi}=C$。现在只需要证明 $\widetilde{\Phi}$ 是 $\UU$-小的，因为这样它将通过定理成为可分离的。

我们通过对表达式的构造进行归纳来证明 $\widetilde{\Phi}$ 是 $\UU$-小的。基础情况是 $x \bisim y$ 和 $x\bin y$，它们已经被调整大小为 $\UU$。显然，$\UU$ 在单纯命题操作（和 $(-1)$-截断）下是封闭的，因此剩下的只是检查有界量词 $\exists(x\in a)$ 和 $\forall(y\in b)$。根据定义，
\begin{align*}
\exists(x\in a) P(x) &\defeq \Brck {\sm{x:V}(x\bin a \land P(x))},\\
\forall(y\in b) P(x) &\defeq  \prd{x:V}(x\bin a \to P(x))。
\end{align*}
我们考虑 $\brck {\sm{x:V}(x\bin a \land P(x))}$。尽管主体 $(x\bin a \land P(x))$ 是 $\UU$-小的，因为根据归纳假设，$P(x)$ 也是如此，但是对 $V$ 的量化不一定保持在 $\UU$ 内。然而，在当前情况下，我们可以用对 $a$ 的成员类型 $[a]\mono V$ 的量化替代它，并且很容易证明
\begin{equation*}
\sm{x:V}(x\bin a \land P(x)) = \sm{x:[a]} P(x)。
\end{equation*}
右侧确实保持在 $\UU$ 内，因为 $[a]$ 和 $P(x)$ 都在 $\UU$ 内。$\prd{x:V}(x\bin a \to P(x))$ 的情况类似，使用 $\prd{x:V}(x\bin a \to P(x)) = \prd{x:[a]}P(x)$。
\end{proof}

我们已经证明在具有一个宇宙 $\UU$ 的类型论中，累积层次 $V$ 是“构造性集合论”\index{constructive!set theory}的一个模型，具有许多标准公理。
然而，据我们所知，它缺少 \emph{强收集 (strong collection)}\index{axiom!strong collection}和 \emph{子集收集 (subset collection)}\index{axiom!subset collection}公理，这些公理包含在 \CZF{}~\cite{AczelCZF} 中。
在类型论中，强收集可能由于其他原因而成立。
我们不知道这些公理是否在我们的模型 $(V,\in)$ 中成立，但这似乎不太可能。
由于 $V$ 是系统内部的一个更高阶归纳类型，而不是一个外部构造，这在某些方面与先前的解释有所不同。

最后，考虑在我们的类型论中添加集合的选择公理，即 \cref{subsec:emacinsets} 中的 $\choice{}$。这会导致 $\LEM{}$ 成立，由 \cref{thm:1surj_to_surj_to_pem} 可知，因此 $\set$ 是一个带有子对象分类器 $\bool$ 的拓扑\index{topos}，由 \cref{thm:settopos} 得出。在这种情况下，我们有 $\prop = \bool:\UU$，因此\emph{所有类都是可分离的}。
因此我们得出：

\begin{lem}\label{lem:fullsep}
在具有 $\choice{}$ 的类型论中，\define{完全分离 (full separation)}\indexdef{separation!full}对于 $V$ 成立：给定\emph{任何}类 $C : V \to \prop$ 和 $a : V$，类 $a \cap C$ 是一个 $V$-集合。
\end{lem}

\begin{thm}\label{thm:zfc}
在具有 $\choice{}$ 和一个宇宙 $\UU$ 的类型论中，累积层次 $V$ 是带选择的 Zermelo--Fraenkel 集合论 (ZFC) 的一个模型。
\end{thm}

\begin{proof}
我们已经有 \cref{thm:VisCST} 中列出的所有公理，加上完全分离，因此我们只需要证明对于所有 $a:V$，存在幂集 $\power a:V$。但是由于我们有 $\LEM{}$，这些仅仅是函数类型 $\power a = (a\to\bool)$。因此 $V$ 是 Zermelo--Fraenkel 集合论 ZF 的一个模型。我们将选择公理的验证作为一个简单的练习留给读者。
\end{proof}

\index{bargaining|)}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\sectionNotes

关于集合范畴的基本性质可以追溯到早期的初等拓扑论的日子。
\cref{subsec:emacinsets} 中提到的 \emph{集合范畴的初等理论 (Elementary theory of the category of sets)} 是由 Lawvere\index{Lawvere} 在 \cite{lawvere:etcs-long} 中引入的，作为集合论的范畴论公理化。
\index{Elementary Theory of the Category of Sets}%
\cite{MoerdijkPalmgren2002} 中介绍了 $\Pi W$-预拓扑的概念，作为初等拓扑的一个预判版本；另请参阅~\cite{palmgren:cetcs}。

\cref{sec:piw-pretopos} 中关于集合范畴的处理大致遵循了~\cite{RijkeSpitters} 中的处理方式。
\cref{epis-surj} 中的结果，即上同态是满射在经典数学中是众所周知的，但作为一个\emph{预判性的}证明，它并不像看起来那样简单。
\index{mathematics!predicative}%
\cite{Mines/R/R:1988} 中的证明使用了幂集操作（这是不可判定的），尽管它也可以被视为一个在更高宇宙 $\UU_{i+1}$ 中的映射是满射的预判性证明。
Wilander~\cite{Wilander2010} 给出了集合论的一个预判性证明。
我们的证明类似于 Wilander 的证明，但通过使用推出和同一性避免了集合论。

\cref{thm:1surj_to_surj_to_pem} 中从 $\choice{}$ 到 $\LEM{}$ 的推导是 Diaconescu~\cite{Diaconescu} 在拓扑论中的一个定理在同伦类型论中的改编，Bishop~\cite[Problem~2]{Bishop1967} 早在其问题中就提出了这一问题。

关于序数的直觉主义理论，请参见~\cite{taylor:ordinals,Taylor99} 以及 \cite{JoyalMoerdijk1995}。
在类型论中，通过归纳原理定义良基性，包括可达性\index{accessibility}的归纳谓词，已经在~\cite{Huet80,Paulson86,Nordstrom88} 中进行了研究，尽管这一想法可以追溯到 Gentzen 关于算术一致性\index{consistency!of arithmetic}的证明~\cite{Gentzen36}。

代数集合论的思想启发了我们在 \cref{sec:cumulative-hierarchy} 中对累积层次的展开，这一思想源于~\cite{JoyalMoerdijk1995}，但其起源于早期的~\cite{AczelCZF} 的工作。
\index{algebraic set theory}%
\index{set theory!algebraic}%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\sectionExercises

\begin{ex}\label{ex:utype-ct}
按照 $\uset$ 的模式，我们想要构造一个所有类型和它们之间的映射的范畴 $\utype$（在给定的宇宙 $\UU$ 中）。然而，为了使其成为 \cref{sec:cats} 中意义上的范畴，我们必须首先定义 $\hom(X,Y) \defeq \pizero{X\to Y}$，其组合通过从普通组合 $(Y\to Z) \to (X\to Y) \to (X\to Z)$ 的截断归纳来定义。这在 \cref{ct:hoprecat} 中定义为\emph{类型的同伦前范畴}。然而，它仍然不是一个范畴，而只是一个前范畴（它的对象类型 $\UU$ 甚至不是一个 $0$-类型）。通过 Rezk 完全性（见 \cref{ct:hocat}），其类型可以与 $\trunc1\type$ 识别。证明所得的范畴 $\utype$，不像 $\uset$，不是一个预拓扑。
\end{ex}

\begin{ex}\label{ex:surjections-have-sections-impl-ac}
证明，如果在 $\uset$ 范畴中每个满射都有一个截面，那么选择公理成立。
\end{ex}

\begin{ex}\label{ex:well-pointed}
证明：在 $\LEM{}$ 成立的情况下，范畴 $\uset$ 是良定点的，
\indexdef{category!well-pointed}%
这意味着以下陈述成立：对于任何 $f, g : A\to B$，如果 $f \neq g$，则存在一个函数 $a : 1\to A$ 使得 $f(a) \neq g(a)$。
证明切片范畴
\index{category!slice}%
$\uset/\bool$ 由 $A\to \bool$ 的函数和交换三角形组成，不具有此属性。
（提示：$\uset/\bool$ 中的终对象是恒等函数 $\bool \to \bool$，因此在这个范畴中，可能存在没有元素 $1\to X$ 的对象 $X$。）
\end{ex}

\begin{ex}\label{ex:add-ordinals}
\index{addition!of ordinal numbers}%
证明：如果 $(A,<_A)$ 和 $(B,<_B)$ 是良基的，外延的，或序数，那么 $A+B$ 也是良基的，外延的，或序数，其中 $<$ 定义为
\begin{align*}
(a<a') &\defeq (a<_A a') & \text{对于 }& a,a':A\\
(b<b') &\defeq (b<_B b') & \text{对于 }& b,b':B\\
(a<b) &\defeq \unit      & \text{对于 }& (a:A),(b:B)\\
(b<a) &\defeq \emptyt    & \text{对于 }& (a:A),(b:B)。
\end{align*}
\end{ex}
% \begin{proof}
%   我们首先通过对 $<_A$ 的归纳证明 $A$ 中的每个元素在 $A+B$ 中是可达的。
%   这很容易，因为 $A+B$ 中小于 $a:A$ 的唯一元素也在 $A$ 中。
%   然后我们通过对 $<_B$ 的归纳证明 $B$ 中的每个元素在 $A+B$ 中是可达的。
%   这很容易，因为我们已经证明 $A$ 中的每个元素是可达的。
% \end{proof}

\begin{ex}\label{ex:multiply-ordinals}
\index{multiplication!of ordinal numbers}%
证明：如果 $(A,<_A)$ 和 $(B,<_B)$ 是良基的，外延的，或序数，那么 $A\times B$ 也是良基的，外延的，或序数，其中 $<$ 定义为
\[ ((a,b) <(a',b')) \defeq (a<_A a') \vee ((a=a') \wedge (b<_B b'))。 \]
\end{ex}
% \begin{proof}
%   我们通过对 $<_A$ 的归纳证明，对于每个 $a:A$，形式为 $(a,b)$ 的每个元素在 $A\times B$ 中是可达的。
%   归纳假设是，对于所有 $a'<_A a$，形式为 $(a',b)$ 的对是可达的。
%   在这个归纳过程中，我们通过对 $<_B$ 的归纳证明 $B$ 中的每个元素在 $A+B$ 中是可达的。
%   内嵌的归纳假设是，对于每个 $b'<_B b$，$(a,b')$ 是可达的。
%   但是现在，如果 $(a',b')< (a,b)$，那么要么 $a<_A a'$，在这种情况下，$(a',b')$ 根据第一个归纳假设是可达的，要么 $a=a'$ 并且 $b'<_B b$，在这种情况下，$(a,b')$ 根据第二个归纳假设是可达的。
%   因此，根据可达性的定义，$(a,b)$ 是可达的。
%   这完成了两个归纳。
% \end{proof}

\begin{ex}\label{ex:algebraic-ordinals}
定义序数的通常代数运算，并证明它们满足通常的性质。
\end{ex}

\begin{ex}\label{ex:prop-ord}
请注意 $\bool$ 是一个序数，在显然的关系 $<$ 下，只有 $\bfalse<\btrue$ 成立。
\begin{enumerate}
\item 定义 $\prop$ 上的一个关系 $<$，使其成为一个序数。
\item 证明 $\id[\ord]\bool\prop$ 当且仅当 \LEM{} 成立。
\end{enumerate}
\end{ex}

\begin{ex}\label{ex:ninf-ord}
回想一下，当我们将 $\nat$ 视为序数时，我们将其记为 $\omega$；因此我们也有序数 $\omega+1$。
另一方面，定义
\[ \nat_\infty \defeq \setof{a:\nat\to\bool | \fall{n:\nat} (a_n \le a_{\suc(n)}) } \]
其中 $\le$ 表示 $\bool$ 上的显然部分顺序，其中 $\bfalse\le\btrue$。
\begin{enumerate}
\item 定义 $\nat_\infty$ 上的一个关系 $<$，使其成为一个序数。
\item 证明 $\id[\ord]{\omega+1}{\nat_\infty}$ 当且仅当有限全知原理~\eqref{eq:lpo} 成立。%
\index{limited principle of omniscience}%
\end{enumerate}
\end{ex}

\begin{ex}\label{ex:well-founded-extensional-simulation}
证明：如果 $(A,<)$ 是良基的且外延的，并且 $A:\UU$，那么存在一个仿真 $A\to V$，其中 $(V,\in)$ 是根据宇宙 $\UU$ 构建的累积层次 \cref{sec:cumulative-hierarchy}。
\end{ex}

\begin{ex}\label{ex:choice-function}
证明 \cref{thm:wop}\ref{item:wop1} 与选择公理~\eqref{eq:ac} 等价。
\end{ex}

\begin{ex}\label{ex:cumhierhit}
给定类型 $A$ 和 $B$，定义\define{双全关系 (bitotal relation)}%
\indexsee{bitotal relation}{relation, bitotal}%
\indexdef{relation!bitotal}%
为 $R:A\to B\to \prop$，使得
\[ \Big(\fall{a:A}\exis{b:B} R(a,b) \Big) \land \Big(\fall{b:B}\exis{a:A} R(a,b) \Big)。 \]
对于这样的 $A,B,R$，令 $A\sqcup^R B$ 为以下更高阶归纳类型生成的类型：
\begin{itemize}
\item $i:A\to A\sqcup^R B$
\item $j:B\to A\sqcup^R B$
\item 对于每个 $a:A$ 和 $b:B$，如果 $R(a,b)$ 成立，则存在路径 $i(a)=j(b)$。
\end{itemize}
证明：累积层次 $V$ 可以通过以下更直接的构造生成，并且所得的归纳原理就是在 \cref{sec:cumulative-hierarchy} 中给出的原理。
\begin{itemize}
\item 对于每个 $A : \UU$ 和 $f : A \to V$，存在一个元素 $\vset(A, f) : V$。
\item 对于任何 $A,B:\UU$ 和双全关系
\index{relation!bitotal}%
$R:A\to B\to \prop$，以及任何映射 $h:A\sqcup^R B \to V$，存在路径 $\id{\vset(A,h\circ i)}{\vset(B,h\circ j)}$。
\item 0-截断构造子。
\end{itemitemize}
\end{ex}

\begin{ex}\label{ex:strong-collection}
在 \CZF 中，\define{强收集公理 (axiom of strong collection)}%
\indexdef{axiom!strong collection}%
\indexdef{collection!strong}%
\indexdef{strong!collection}%
的形式如下：
\begin{multline*}
\Parens{\fall{x\in v}\exis{y} R(x,y)} \Rightarrow \\
\exis{w}\big[\big(\fall{x\in v}\exis{y\in w}R(x,y)\big)\land \big(\fall{y\in w}\exis{x\in v}R(x,y) \big)\big]
\end{multline*}
它在累积层次 $V$ 中成立吗？（我们不知道答案。）
\end{ex}

\begin{ex}\label{ex:choice-cumulative-hierarchy-choice}
验证：如果我们假设 $\choice{}$，那么累积层次 $V$ 满足通常的集合论选择公理，其形式如下：
\[
\fall{x:V} \Parens{(\fall{y\in x}\exis{z:V} z\in y) \Rightarrow  \exis{c\in(\cup x)^x}\fall{y\in x} c(y)\in y}
\]
\end{ex}

\begin{ex}\label{ex:plump-ordinals}
假设命题重设，证明存在一个单纯谓词 $\mathsf{isPlump}:\ord\to\prop$，使得对于任何 $A:\ord$，我们有
\begin{multline*}\label{eq:plump}
\mathsf{isPlump}(A) = \Parens{\fall{B<A} \mathsf{isPlump}(B)} \wedge\narrowbreak
\Parens{\fall{C,B:\ord} C\le B < A \wedge \mathsf{isPlump}(C) \Rightarrow C < A}。
\end{multline*}
请注意，$\mathsf{isPlump}$ 不能通过对 \ord 的简单良基归纳来定义；你必须使用不同的良基关系。
我们说一个序数 $A$ 是 \define{丰满的 (plump)}~\cite{taylor:ordinals,Taylor99} 如果 $\mathsf{isPlump}(A)$ 成立。
\index{plump!ordinal}\index{ordinal!plump}%
\end{ex}

\begin{ex}\label{ex:not-plump}
证明：\LEM{} 与“所有序数都是丰满的”这一陈述等价。
\end{ex}

\begin{ex}\label{ex:plump-successor}
定义序数 $A$ 的\define{丰满后继 (plump successor)}\index{plump!successor}\indexdef{successor!plump}为
\[ t(A) \defeq \setof{ B:\ord | (B\le A) \wedge \mathsf{isPlump}(B) } \]
\begin{enumerate}
\item 根据定义，$t(A)$ 属于更高的宇宙。
证明：假设命题重设，它等于与 $A$ 在同一宇宙中的一个序数。
\item 再次假设命题重设，证明如果 $A$ 是丰满的（见 \cref{ex:plump-ordinals}），那么 $t(A)$ 也是丰满的。
\end{enumerate}
\end{ex}

\begin{ex}\label{ex:ZF-algebras}
相对于一个宇宙 $\UU_i$，一个 \define{ZF-代数 (ZF-algebra)}~\cite{JoyalMoerdijk1995}%
\index{ZF-algebra}%
是一个偏序集（见 \cref{ct:orders}）$V:\UU_{i+1}$，它具有所有由类型 $\UU_i$ 索引的上确界，并且配备了一个“后继”函数 $s:V\to V$（不一定以任何方式尊重 $\le$）。
\begin{enumerate}
\item 证明：累积层次 $(V_{\UU_i},\subseteq,s)$ 是初始 ZF-代数，其中 $s(x)$ 是单元集 $\setof{x}$。
\item 证明：$(\ord_{\UU_i},\le,s)$ 是具有 $x\le s(x)$ 对于所有 $x$ 成立的初始 ZF-代数，其中 $s(A)=A+\unit$ 是 \cref{thm:ordsucc} 中的后继\index{successor!of an ordinal}。
\item 假设命题重设，证明 $\Parens{\setof{A:\ord_{\UU_i} | \mathsf{isPlump}(A) },\le,t}$ 是具有 $(x\le y) \Rightarrow (t(x)\le t(y))$ 对于所有 $x,y$ 成立的初始 ZF-代数，其中 $t$ 是 \cref{ex:plump-successor} 中的丰满后继。
\end{enumerate}
\end{ex}

\begin{ex}\label{ex:monos-are-split-monos-iff-LEM-holds}
对于一个范畴 $A$，如果存在一个态射 $g: \hom_A(b,a)$ 使得 $\id{g \circ f}{1_a}$，则态射 $f: \hom_A(a,b)$ 称为\define{分裂单态射 (split monomorphism)}。 (这样的 $g$ 称为 $f$ 的\define{重traction}。)
证明以下陈述逻辑等价。
\begin{enumerate}
\item $\LEM{}$。
\item 对于范畴 $\uset$ 中的每对集合 $A$ 和 $B$，如果 $A$ 是非空的，那么对于 $\uset$ 中的每个单态射 $f: A \to B$，$f$ 也是 $\uset$ 中的分裂单态射。
\endenumerate}
\end{ex}

\index{set|)}%

% 本地变量:
% TeX-主模式: "hott-online"
% 结束: