用户: Trebor/泛等公理的 Voevodsky 模型

简单介绍一下 Voevodsky 提出的最早的泛等公理模型. 其实没那么复杂. 可以依靠仔细检查语言的使用直接避免融贯问题的出现, 无需应用复杂的融贯定理, 代价是需要很仔细.

1集合族

先来回顾集合模型的定义. 我们希望将类型解释为集合, 而依值类型则是集合族, 也就是形如 $A\to \text{Set}$ 的函数. 不过实际上, 所有类型 $\Gamma ⊢A$ 都是依值类型, 依赖于语境 $\Gamma$. 所以正确的解释是将语境解释为集合, 而类型解释为集合族.

给定集合 $\Gamma ,\Delta$ 与函数 $\sigma :\Delta \to \Gamma$, 这对应类型论中两个语境之间的变量代换. 如果有集合族 $A:\Gamma \to \text{Set}$ 表示 $\Gamma$ 下的类型, 那么代换可以得到另一个集合族 $A\sigma :\Delta \to \text{Set}$, 定义是 $x\mapsto A(\sigma (x))$. 这给出了映射 $\text{Ty}(\Gamma )\to \text{Ty}(\Delta )$. 也就是说, $\text{Ty}$ 是集合范畴上的反变函子. 按定义显然有 $A(\sigma \circ \delta )=(A\sigma )\delta$, 即 $\text{Ty}$ 的函子性等式成立.

在数学上, 往往喜欢不用集合族而用集合映射. 这两者之间的转换关系如下.

•	给定集合族 $A:\Gamma \to \text{Set}$, 考虑并集 ${⨆}_{x\in \Gamma }A(x)$, 记作 $\int A$. 有显然的投影映射 $\int A\to \Gamma$, 这是其对应的集合映射.
•	给定集合映射 $p:E\to \Gamma$, 考虑集合族 $A(x)=p^{-1}(\{x\})$, 也就是 $A(x)=\{y\mid p(y)=x\}$. 这是其对应的集合族.

这两个转换关系并不是严格互逆的, 也就是说从集合族到映射再回到集合族, 得到的东西不完全相等, 而只是同构; 反之亦然. 集合映射中, 代换对应的操作是拉回. 给定映射 $p:E\to \Gamma$ 与 $\sigma :\Delta \to \Gamma$, 代换得到的结果是 $E^{\prime }\to \Delta$, 其中$$E^{\prime }=\{(e,y)\in E\times \Delta \mid p(e)=\sigma (y)\}.$$这个构造可以写作 ${\sigma }^{\ast }p$ 或者 $E{\times }_{\Gamma }\Delta$. 这时候, 代换操作的函子性等式就不成立了. 我们有$$(\sigma \circ \delta {)}^{\ast }p=\{(e,z)\in E\times \Sigma \mid p(e)=\sigma (\delta (z))\}$$而$${\delta }^{\ast }({\sigma }^{\ast }p)=\{((e,y),z)\mid p(e)=\sigma (y),y=\delta (z)\}.$$虽然两者几乎是一样的, 有显然的典范双射, 但是作为集合它们仍然是不同的.

总结一下, 用集合映射的优点是不用引入新概念, 一切都仍然在集合范畴内部进行, 所以集合的定理都能直接用. 而集合族的优点则是许多东西都是严格成立的等式, 而这是类型论的模型需要的.

最后, 给定集合族 $A:\Gamma \to \text{Set}$, 可以定义它的截面, 截面就是一个函数 $f$, 输入 $x\in \Gamma$, 输出 $A(x)$. 在类型论的模型里面表示这个依值类型的元素构成的集合, 对应 $\Gamma ⊢f:A$. 因为 $f$ 可以用到 $\Gamma$ 里的变量, 所以截面也定义成一个依值函数.

2单纯集

单形 ${\Delta }^0,{\Delta }^1,{\Delta }^2,{\Delta }^3,\dots$ 是点、线段、三角形、四面体等的推广. 而单纯集则是将一系列这些东西拼在一起构成的图形. 这样得到的东西优点是完全组合的, 不存在拓扑空间中的种种反例, 适合用于发展同伦论.

定义 2.1. 单纯集 $X$ 包含以下资料.

•	一族集合 $X_n$, 其中 $n$ 是自然数, 表示 $n$ 维单形的集合. 有时候因为公式的下标写起来比较方便, 规定 $X_{-1}$ 是只有一个元素的集合.
•	一些映射 ${\partial }_i:X_n\to X_{n-1}$, 其中 $0\le i\le n$, 称为面映射, 表示 $n$ 维单形的第 $i$ 个面 (从零数起).
•	一些映射 $s_i:X_n\to X_{n+1}$, 其中 $0\le i\le n$, $s_i(x)$ 表示第 $i$ 个顶点和第 $(i+1)$ 个顶点相同的退化 $(n+1)$ 维单形.
•	这些映射满足一些等式.

假设读者已经了解单纯集的基本直观. 接下来要定义的是依值单纯集, 类比前一节中的集合族. 在传统的理论中, 用的都是单纯集之间的映射 $E\to X$, 但是我们现在需要一些严格的等式成立, 所以改写成依值单纯集. 各种定理都仍然是成立的, 不过需要一点点改动.

定义 2.2. 给定单纯集 $X$, 依值单纯集 $A$ 包含以下资料.

•	对于每个元素 $x\in X_n$, 赋予集合 $A_n(x)$.
•	一些映射 ${\partial }_i:A_n(x)\to A_{n-1}({\partial }_{i}x)$, 其中 $0\le i\le n$.
•	一些映射 $s_i:A_n(x)\to A_{n+1}(s_{i}x)$, 其中 $0\le i\le n$.
•	这些映射满足与单纯集一样的等式.

定义 2.3. 给定单纯集 $X$ 与其上的依值单纯集 $A$, 可以定义其全空间 $\int A$ 为另一单纯集. 它的 $n$ 维单形是 $\{(x,a)\mid x\in X_n,a\in A_n(x)\}$. 面映射和退化映射分别在两个分量上同时作用.

如果有函数 $f$, 输入元素 $x\in X_n$, 输出 $A_n(x)$ 的元素, 满足等式 $f({\partial }_{i}x)={\partial }_{i}f(x)$ 与 $f(s_{i}x)=s_{i}f(x)$, 就说 $f$ 是 $A$ 的截面. 截面构成的集合记作 $\mathrm{El}(A)$.

这两个定义都在集合族里有直接类比, 上面已经提到. 注意截面只构成一个集合, 而不构成单纯集.

上面讲了单纯集的优点, 但是它也有缺点. 最主要的缺点是有些该有的边没有. 例如可以有 3 个顶点 $x,y,z$ 与线段 $x\to y$, $y\to z$, 但是不存在线段 $x\to z$. 所以单纯集里要表达正确的同伦关系, 需要手动处理一串线段构成的道路.

Kan 复形说的是一个单纯集中所有想要的拼接关系都已经加进去了. 例如上面的两条线段, 可以表达为映射 ${\Lambda }_1^2\to X$, 其中 ${\Lambda }_1^2$ 是一个三角形 ${\Delta }^2$ 去掉中心和一条边. 我们希望将它补全成一个三角形 ${\Delta }^2\to X$. 这就是说显然的复合操作 $\mathrm{hom}({\Delta }^2,X)\to \mathrm{hom}({\Lambda }_1^2,X)$ 是个满射.

对于依值单纯集 $\Gamma ⊢A$ 的情况, 也有类似的条件. 这个条件中, 我们不要求 $\Gamma$ 是 Kan 复形, 只要求 “$A$ 的部分” 满足 Kan 复形的条件. 我们把这个叫做依值 Kan 复形. 具体来说, 考虑 ${\Lambda }_i^n\subseteq {\Delta }^n$ 为 $n$ 维单形去掉第 $i$ 个面以及中心. 假如 $\Gamma$ 中选定一个 $n$ 维单形 ${\Delta }^n\to \Gamma$, 限制到 ${\Lambda }_i^n\subseteq {\Delta }^n$ 上, 在 $A$ 中任意选择截面, 都能拓展到 ${\Delta }^n$ 上 $A$ 的截面, 那么就称 $A$ 是依值 Kan 复形.

这个概念在同伦论中也是熟知的, 但是一般只在映射的语言里表述, 而不用集合族的语言. 依值 Kan 复形对应到映射 $\int A\to \Gamma$ 中的等价条件, 叫做 Kan 纤维化. 如果 $\Gamma =1$ 只有一个点, 表示空语境, 那么 Kan 纤维化就退化成普通的 Kan 复形的条件.

模型范畴

还是逃不掉一些模型范畴的理论, 大概讲一讲.

在同伦论中有三大类映射.

•	纤维化, 上面已经讲过了.
•	余纤维化, 表示 “性质良好的子空间”. 在有排中律的前提下, 单纯集中所有的单射都是余纤维化. 这是单纯集的优点在技术上的具体体现.
•	弱等价, 表示两个空间纯同伦意义下相同.

如果一个映射同时是纤维化和弱等价, 就称为平凡纤维化. 这表示一个依值类型, 在每个点处都可缩 (同伦意义下等价于单元素类型). 如果映射同时是余纤维化和弱等价, 就称为平凡余纤维化.

上面提到的 Kan 纤维化条件, 在范畴语言里写出来是这样的:$${\Lambda }_i^{n}E{\Delta }^{n}Bip$$给定两个横向映射使得正方形交换, 就存在斜向的映射使得两个三角形分别交换. 如果有两个竖向的映射 $i,p$ 满足这个条件 (对于任何将它们横向补成正方形的方式, 都存在斜着的映射), 就写作 $i⋔p$. 在实际操作中, 往往会遇到需要多次用到 $i⋔p$ 这个条件, 组合出一个更大的映射的情况. 例如考虑 $j:{\Lambda }_i^n+{\Lambda }_j^n\to {\Delta }^n+{\Delta }^n$. 运用两次这个条件就能得到 $j⋔p$ 也成立. 那么, 有哪些映射 $j$ 满足 $j⋔p$ 对所有的 Kan 纤维化都成立呢? 答案恰好是所有的平凡余纤维化.

同样的, 映射 $p$ 满足 $j⋔p$ 对所有的平凡余纤维化 $j$ 都成立, 就等价于 $p$ 是 Kan 纤维化. 反过来, $j⋔p$ 对所有的平凡纤维化 $p$ 成立, 等价于 $j$ 是余纤维化; $j⋔p$ 对所有的余纤维化 $j$ 成立, 等价于 $p$ 是平凡纤维化. 这是用映射而不是依值单纯集的另一个好处: 所有的条件都非常对称.

3Voevodsky 模型

我们将 Voevodsky 的模型表述为具族范畴. 语境解释成单纯集, 空语境就是单元素的单纯集. 因为单纯集本身是预层, 而具族范畴里面的类型 $\text{Ty}$ 又是语境范畴上的预层, 所以这里的类型就是预层的预层, 比较可怕. 因此我们尽量不把单纯集看作预层.

将某个语境 $\Gamma$ 中的类型解释为 $\Gamma$ 上的依值 Kan 复形. 注意 $\Gamma$ 本身不一定是 Kan 复形. 变量代换在类型上是严格满足等式的. $\Gamma$ 中的元素 $\text{Tm}(\Gamma )$ 自然就是每个类型的元素的并$$\text{Tm}(\Gamma )=\underset{A\in \text{Ty}(\Gamma )}{⨆}\mathrm{El}(A).$$而 $\mathrm{El}(A)$ 就是上面定义的截面集合. $\text{Tm}$ 上变量代换也可以验证是严格满足等式的. 给定 $\Gamma ⊢A$, 语境扩展 $(\Gamma ,A)$ 自然就是依值 Kan 复形的全空间 $\int A$. 它要满足的性质也是按定义成立的.

我们需要略微处理一下集合大小问题. 假设有三个集合宇宙 ${\text{Set}}_{\alpha }\in {\text{Set}}_{\beta }\in {\text{Set}}_{\gamma }\in \text{Set}$, 使得这三个宇宙都对我想做的一切操作封闭, 例如取幂集或者函数集等. 如果你的元语言是类型论, 那直接取三个类型宇宙也可. 我们设语境的单纯集是 ${\text{Set}}_{\gamma }$ 里的单纯集, 这样语境就构成一个小范畴 ${\text{sSet}}_{\gamma }$. 而语境中的类型则需要构成预层 $\text{Ty}:{\text{sSet}}_{\gamma }^{\text{op}}\to \text{Set}$. 最简单的办法就是采用 ${\text{Set}}_{\gamma }$ 里的依值 Kan 复形, 不过实际上只需要不比 $\gamma$ 大即可, 这里我们定义为 ${\text{Set}}_{\beta }$ 里的依值 Kan 复形. 这是为了留下一点操作空间. 剩下一个 (集合) 宇宙则是用来构造模型里的 (类型) 宇宙的.

类型

大部分类型都很容易构造, 显然的那个做法就是对的. 主要问题是需要验证的事情非常多, 建议开一个定理证明器形式化一下. 不需要把细节输进去, 例如 “是 Kan 复形” 这个命题不需要具体定义出来, 就直接作为无定义的一个常量, 只是让定理证明器提醒你还有这样一个东西需要证.

具体来说, 定义类型需要验证的事情有:

•	构造对应的依值单纯集.
•	验证单纯集需要满足的 ${\partial }_i,s_i$ 等式.
•	验证这些依值单纯集是依值 Kan 复形.
•	验证类型构造子在代换下满足的等式, 例如 $(A+B)\sigma =A\sigma +B\sigma$.
•	定义需要的单纯集之间的映射, 例如 $\text{inl}:A\to (A+B)$.
•	定义这些单纯集映射需要满足的 ${\partial }_i,s_i$ 等式.
•	验证这些在代换下满足的等式, 例如 $\text{inl}(x)\sigma =\text{inl}(x\sigma )$.
•	验证类型论中的判值相等在单纯集里对应的等式, 例如 $(\lambda x.u)t=u[x/t]$.

先来考虑最简单的依值类型, $\Sigma$ 类型. 我们有单纯集 $\Gamma$, 还有 $\Gamma$ 上的依值 Kan 复形 $A$ 与 $(\Gamma ,A)$ 上的依值 Kan 复形 $B$. 那么类型 $\Sigma AB$ 应该定义成 $\Gamma$ 上的依值单纯集. 给定 $x\in {\Gamma }_n$, 它对应的 $n$ 维依值单形集合$$(\Sigma AB{)}_n(x)=\{(a,b)\mid a\in A_n(x),b\in B_n(x,a)\}.$$它的 ${\partial }_i$ 与 $s_i$ 都是两个分量分别作用的, 因此等式显然满足.

接下来证明这是依值 Kan 复形. 这也不难, 只需要先用 $A$ 是依值 Kan 复形的条件构造出 $A$ 上的单形, 再用 $B$ 是依值 Kan 复形的条件构造出 $B$ 上的单形, 两者组合起来即可.

至于代换下的等式, 即 $(\Sigma AB)\sigma =\Sigma (A\sigma )(B{\sigma }^{\prime })$, 其中 ${\sigma }^{\prime }:(\Delta ,A\sigma )\to (\Gamma ,A)$ 是代换的弱化. 这很容易验证, 因为$$((\Sigma AB)\sigma {)}_n(x)=\{(a,b)\mid a\in A_n(\sigma (x)),b\in B_n(\sigma (x),a)\}.$$所以这个等式也严格成立. 其余的事务留给读者.

对于 $\Pi$ 类型, 构造略微有一些繁琐. 先来说说函数类型. 在单纯集中, 指数对象的构造如下: 因为 $B^A$ 的 $n$ 维单形与映射 $\mathrm{hom}({\Delta }^n,B^A)$ 构成双射, 我们只需要计算后者是什么即可. 而由指数对象的定义, $\mathrm{hom}({\Delta }^n,B^A)\cong \mathrm{hom}({\Delta }^n\times A,B)$. 所以我们可以构造$$(B^A{)}_n=\mathrm{hom}({\Delta }^n\times A,B).$$可以验证这个符合要求. 对依值单纯集的 $\Pi$ 类型, 也是同样的道理. 假设 $x\in {\Gamma }_n$, 那么考虑 $(\Gamma ,A)$ 上的另一个依值单纯集, 记作 $A^{\ast }x$. 这用映射的语言比较好说, 就是 $x$ 看作 ${\Delta }^n\to \Gamma$, 与映射 $(\Gamma ,A)\to \Gamma$ 的拉回 $E\to (\Gamma ,A)$, 再看作依值单纯集. 这也可以直接用依值单纯集的语言描述, 但是比较麻烦. 而 $\Pi$ 类型中, 我们定义 $x$ 上的依值 $n$ 单形集合 $(\Pi AB{)}_n(x)$ 为 $A^{\ast }x\to B$, 即这两个关于 $(\Gamma ,A)$ 的依值单纯集之间的映射的集合. 如果全部用依值单纯集的语言描述, 得到的东西就是满足严格的代换等式 $(\Pi AB)\sigma =\Pi (A\sigma )(B{\sigma }^{\prime })$ 的.

用更加范畴的语言描述, 这就是关于 $(\Gamma ,A,B)\to (\Gamma ,A)$ 与 $(\Gamma ,A)\to \Gamma$ 取前推映射 $(\Gamma ,\Pi AB)\to \Gamma$. 这在任何局部积闭范畴中都存在, 而 $\text{sSet}$ 作为预层范畴自然也有.

我们需要证明 Kan 纤维化的前推映射总是 Kan 纤维化. 这一点依赖于 $\text{sSet}$ 作为模型范畴的重要性质, 即 right properness ^暂无翻译. 这是说将弱等价映射沿着纤维化拉回, 得到的还是弱等价. 由于 $\text{sSet}$ 中余纤维化就是所有的单射, 所以余纤维化的拉回也是余纤维化. 二者结合起来, 说明将平凡余纤维化沿着纤维化拉回, 得到的还是平凡余纤维化.

在前面提到的 $⋔$ 正方形中, 如果有一对伴随函子 $F⊣G$, 那么读者可以试着验证 $F(i)⋔p$ 等价于 $i⋔G(p)$. 这就是直接反复使用伴随函子的性质. 设 $F$ 是关于 $(\Gamma ,A)\to \Gamma$ 取拉回. 那么 $G$ 就是取前推的函子. 我们知道 $F$ 保持平凡余纤维化, 因此如果 $p$ 是纤维化, 则 $F(i)⋔p$ 对所有平凡余纤维化 $i$ 都成立, 所以 $i⋔G(p)$ 对所有平凡余纤维化 $i$ 都成立, 说明 $G(p)$ 也是纤维化. 这就证明了 $\Pi AB$ 是依值 Kan 复形.

别的事务都不需要模型范畴的知识, 只需形式化地操作即可.

宇宙类型

定义 3.1. 在类型论的模型中, 宇宙类型的模型由如下资料组成:

•	一个类型 $\text{U}:1\to \text{Ty}$, 这由在空语境中的元素 $U\in \text{Ty}(1)$ 完全决定, 我们也用 $U$ 表示只有这一个类型的语境.
•	这个类型的元素构成的预层是 ${\text{U}}^{\ast }\text{Tm}=よ(U)$. 我们需要映射 $\text{el}:よ(U)\to \text{Ty}$, 将宇宙类型的元素映射到真正的类型.

$\text{el}$ 也可以看作是 $\text{Ty}(U)$ 的元素, 即在 $x:U$ 这个语境下给出一个类型. 这样, 我们可以考虑 $(x:U,y:\text{el}(x))$ 这个语境, 也就是将 $\text{Tm}\to \text{Ty}$ 沿着 $\text{el}$ 拉回得到的东西, 记作 $\tilde{U}$.

对于宇宙类型, 我们需要构造一个单纯集 $U_{\alpha }$, 然后定义对应的常依值单纯集作为类型 ${\text{U}}_{\alpha }\in \text{Ty}(\Gamma )$. 具体来说, 就是对于单纯集 $\Gamma$, 定义一个 $n$-单形 $s\in {\Gamma }_n$ 上的依值 $n$-单形集合为 $(U_{\alpha }{)}_n$, 不依赖于 $s$. 这样定义出的依值单纯集, 全空间是 $\int {\text{U}}_{\alpha }=U_{\alpha }\times \Gamma$, 符合直觉. 而这个依值单纯集是 Kan 复形, 当且仅当原来的单纯集 $U_{\alpha }$ 是 Kan 复形.

要定义单纯集 $U_{\alpha }$, 就得定义它的 $n$-单形 $(U_{\alpha }{)}_n$ 都有哪些. 因为 $U_{\alpha }$ 的元素应该表示类型, 而类型又解释成了 Kan 复形, 所以 $(U_{\alpha }{)}_n$ 应该解释成 ${\Delta }^n$ 上的依值 Kan 复形 (并且处在 ${\text{Set}}_{\alpha }$ 宇宙中). 对应的面映射 $(U_{\alpha }{)}_n\to (U_{\alpha }{)}_{n-1}$ 就是将 ${\Delta }^n$ 上的依值 Kan 复形限制到一个面 ${\Delta }^{n-1}\subseteq {\Delta }^n$ 上, 以此类推. 这样, $U_{\alpha }$ 是严格满足单纯集需要满足的等式的.

接下来, 我们需要证明 $U_{\alpha }$ 本身是个 Kan 复形. 这一点需要用到一点点极小纤维化的理论. 极小纤维化大致说的是依值 Kan 复形中不存在任何多余的边. 如果两个依值极小 Kan 复形同伦等价, 那么它们就直接同构. 这在传统的同伦论中就已经极其方便. 在这里, 我们要用到的性质是: 任何 Kan 纤维化 $p:E\to B$ 都能分解成 $E\stackrel{g}{\to }F\stackrel{q}{\to }B$, 其中 $q$ 是极小纤维化, 而 $g$ 是平凡纤维化.

给定 $f:{\Lambda }_i^n\to U_{\alpha }$, 我们需要将它延拓到 ${\Delta }^n\to U_{\alpha }$. 根据 $U_{\alpha }$ 的定义, $f$ 对应于 ${\Lambda }_i^n$ 上的依值 Kan 复形. 我们将它分解成平凡纤维化和极小纤维化. (...)

注 3.2. 我们可以计算 $\Gamma \to U_{\alpha }$ 的映射, 与 $\Gamma$ 上的 ${\text{Set}}_{\alpha }$ 大小的依值 Kan 复形是一一对应的. 这是因为依值 Kan 复形的条件是一个单形一个单形地给出的, 所以只要如 $U_{\alpha }$ 的构造中那样, 保证限制到 $\Gamma$ 的每个 $n$ 单形时都给出依值 Kan 复形, 就可以保证整体也是依值 Kan 复形.

敏锐的读者可能注意到, 因为我们一开始构造 $\text{Ty}$ 的时候用的是 ${\text{Set}}_{\beta }$ 宇宙中的依值 Kan 复形, 所以实际上 $\text{Ty}\cong よ(U_{\beta })$! 也就是说, $\text{Tm}\to \text{Ty}$ 其实也是一个 “大宇宙” ${\tilde{U}}_{\beta }\to U_{\beta }$.

道路类型

定义 3.3. 给定 $\Gamma ⊢A$ 与两个元素 $\Gamma ⊢s,t:A$, 可以构造道路类型 $\Gamma ⊢{\text{Id}}_A(s,t)$, 配备了元素$$\frac{\Gamma ⊢r:A}{\Gamma ⊢\text{refl}(r):{\text{Id}}_A(r,r)}$$使得$$\frac{\begin{array}{c}\Gamma ,x:A,y:A,p:{\text{Id}}_A(x,y)⊢C\Gamma ,z:A⊢r:C[z/x,z/y,\text{refl}(z)/p]\\ \Gamma ⊢s:A\Gamma ⊢t:A\Gamma ⊢q:{\text{Id}}_A(s,t)\end{array}}{\Gamma ⊢{\text{J}}_C(z.r,s,t,q):C[s/x,t/y,q/p]}$$满足 ${\text{J}}_C(z.r,s,s,\text{refl}(s))=r[\text{refl}(s)/z]$.

道路类型在直观上应该是有一个区间对象 $\mathbb{I}$, 然后 $\mathbb{I}\to A$ 的映射就是道路的元素. 在单纯集中, 区间对象就是 ${\Delta }^1$. 但是需要注意的是, ${\Delta }^1$ 不是 Kan 复形, 所以不能直接沿用 $\Pi$ 类型一节的证明. 不过, 由于 $\mathbb{I}$ 本身并不依赖于语境 $\Gamma$, 所以一些东西可以简化.

先暂时忽略宇宙大小的问题. 如果我们能给出以下 “万有” 的道路类型的构造, 就能在变量代换下自动给出所有具体的道路类型.

$$A:\text{Ty},x:A,y:A⊢{\text{Id}}_A(x,y)$$$$A:\text{Ty},x:A⊢\text{refl}(x):{\text{Id}}_A(x,x)$$

尽管 $\text{Ty}$ 并不是类型, 但是根据注 3.2 $\text{Ty}=よ(U_{\beta })$, 因此它的确能视作合法的语境. 这样依赖, 类似地, $(A:\text{Ty},x:A)$ 这个语境对应的是对象 ${\tilde{U}}_{\beta }$. $(A:\text{Ty},x:A,y:A)$ 同构于 ${\tilde{U}}_{\beta }{\times }_{U_{\beta }}{\tilde{U}}_{\beta }$. 故 $\text{Id}$ 类型对应语境 ${\tilde{U}}_{\beta }{\times }_{U_{\beta }}{\tilde{U}}_{\beta }$ 下的某个类型. 给定具体的语境下的类型 $\Gamma ⊢A$ 与元素 $\Gamma ⊢s,t:A$, 它们共同决定一个映射 $\Gamma \to {\tilde{U}}_{\beta }{\times }_{U_{\beta }}{\tilde{U}}_{\beta }\to U_{\beta }$, 沿着它代换即可.

$\text{J}$ 消去子的 “万有” 形式如下:$$\frac{\begin{array}{c}A:\text{Ty},x:A,y:A,p:{\text{Id}}_A(x,y)⊢C\\ A:\text{Ty},z:A⊢c:C\rho \end{array}}{A:\text{Ty},x:A,y:A,p:{\text{Id}}_A(x,y)⊢\text{J}(c):C}$$其中 $\rho$ 将 $(A,x,y,p)$ 分别代入为 $(A,z,z,\text{refl}(z))$. 使得 $J(c)\rho =c$. 如果画出交换图, 就是$${\tilde{U}}_{\beta }{\tilde{U}}_{\beta }({\tilde{U}}_{\beta }{\times }_{U_{\beta }}{\tilde{U}}_{\beta },\text{Id})U_{\beta }c\rho \pi C$$这里我们将 $\text{Tm}\to \text{Ty}$ 利用可表性化为范畴里的对象 (而不是广义对象). 这样整个条件就变成了证明 $\rho ⋔\pi$.

警告 3.4. 在立方集构成的构造主义模型中, 正规性往往不能成立, 即上面交换图中左上侧的三角形不能严格交换, 只能在道路类型意义下交换. 但是下面介绍的单纯集构造中是满足严格交换性的.

我们先证明 $\text{Tm}\to \text{Ty}$ (实际上是 ${\tilde{U}}_{\beta }\to U_{\beta }$ 这个单纯形之间的映射) 是 Kan 纤维化. 展开 $U_{\beta }$ 的定义, 这几乎是按定义成立的同义反复.

(...)

4验证泛等公理

验证泛等公理稍微有点繁琐. 具体来说, 在我们构造的模型中, 空语境下泛等公理这个类型对应一个单纯集, 我们需要验证这个单纯集非空. 因为泛等公理本身的表述就比较复杂, 所以要算出这个单纯集具体是什么就有点困难. 我们先提出一个在 $\text{sSet}$ 中比较自然的同伦论命题, 作为泛等公理的单纯集版本, 然后先证明这个命题和类型论里的泛等公理解释到 $\text{sSet}$ 中得到的东西等价, 最后再证明这个命题本身成立.

5哪里用了排中律?

首先, $\text{sSet}$ 构成模型范畴这件事是需要排中律的. 只要余纤维化定义成全体单射, 这个模型范畴就不能构造性地存在. 不过, 如果我们将余纤维化 $A\to B$ 定义成单射, 使得一个单形 $x\in B_n$ 是否在其像中可判定, 并且如果 $x$ 不在其像中, 那么它是否是退化单形可判定, 就仍然能补成一个模型结构. 这样的缺点是许多证明中原本显然的东西不能直接使用了. 例如 $X$ 是 Kan 复形时 $X^K$ 也总是 Kan 复形. 这在构造主义中的版本就需要加上 $0\to K$ 是余纤维化的条件. 另一方面, 在极小纤维化的理论中用了不少排中律和选择公理. 不过, 可以修改证明避免这一点, 参见此 MathOverflow 回答.

对于构造性的单纯形模型的考量, 读者可以参考 [Gambino–Henry 2022].

参考文献

Nicola Gambino, Simon Henry (2022). “Towards a constructive simplicial model of Univalent Foundations”. Journal of the London Mathematical Society 105 (2), 1073–1109. (doi) (web)