用户: 算，就使劲算/如何把你的类型论变成一个范畴

读者最好了解依赖类型论 (dependent type theory) 和范畴论的基本概念. 没有的话也无妨, 您可以随便逛逛. 我们将始终要求涉及的类型论 $\mathbb{T}$ 是依赖类型论.

1句法范畴

对于一个类型论 $\mathbb{T}$, 我们可以纯粹通过 $\mathbb{T}$ 中的语句定义一个范畴. 它的对象是类型论 $\mathbb{T}$ 中的语境 (context):$$\Gamma =(a_1:A_1,a_2:A_2,...,a_n:A_n)$$

而态射 $\sigma :\Gamma \to \Delta$ 则是这两个语境间的 substitution:$$\sigma =({\sigma }_1,{\sigma }_2,...,{\sigma }_m)\Delta =(x_1:X_1,x_2:X_2,...,x_m:X_m)$$其中 ${\sigma }_i$ 满足:$$\begin{gathered} \Gamma ⊢{\sigma }_1:X_1 \\ \Gamma ⊢{\sigma }_2:X_2[{\sigma }_1/x_1] \\ ... \\ \Gamma ⊢{\sigma }_m:X_m[{\sigma }_1/x_1,{\sigma }_2/x_2,...,{\sigma }_{m-1}/x_{m-1}] \end{gathered}$$

恒等态射 $\mathsf{id}:\Gamma \to \Gamma$ 是保持所有变量不变的 substitution:$$\mathsf{id}=(a_1,a_2,...,a_n)\Gamma =(a_1:A_1,a_2:A_2,...,a_n:A_n)$$

而给定态射 $\sigma :\Gamma \to \Delta$ 和 $\tau :\Delta \to \Phi$:$$\Delta =(x_1:X_1,x_2:X_2,...,x_n:X_n)$$$$\sigma =({\sigma }_1,{\sigma }_2,...,{\sigma }_n)\tau =({\tau }_1,{\tau }_2,...,{\tau }_m)$$

它们的复合 $\tau \circ \sigma =((\tau \circ \sigma {)}_i)$ 则是将 $\tau$ 用 $\sigma$ 进行 substitute:$$(\tau \circ \sigma {)}_i={\tau }_i[{\sigma }_1/x_1,{\sigma }_2/x_2,...,{\sigma }_n/x_n]$$

定义 1.1. 这个范畴叫做 $\mathbb{T}$ 的句法范畴 (syntactic category) ¹, 记作 $\mathsf{C}\mathsf{TX}(\mathbb{T})$.

1.	又称为 category of contexts.

注 1.2. 句法范畴中 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 态射复合的结合律 (也就是 substitution 的结合律) 一般被称为 substitution lemma.

我们用 $\bullet$ 表示空语境, 也就是不包含任何类型的语境 $()$.

定理 1.3. 空语境 $\bullet$ 是句法范畴的一个终对象 (terminal object).

证明. 没什么可大惊小怪的, 只是定义而已.

$\square$

注 1.4. 不同的语境在句法范畴中可能是同构的对象. 例如, 任取两个闭类型 $A$ 和 $B$, 通过交换自由变量我们可以得到一个表现对称性的同构:$$(a:A,b:B)\simeq (b:B,a:A)$$之后我们会看到更多例子. 这说明句法范畴实际上并不能完全地还原句法.

最后, 任何闭类型 (closed type)$A$, 也就是在空语境下合法定义的类型:$$⊢A\mathrm{type}$$都可以通过语境 $(a:A)$ 来将其看做是句法范畴中的一个对象. 所有闭类型组成 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 的一个满子范畴, 记作 $\mathsf{T}\mathsf{YPE}(\mathbb{T})$.$$\mathsf{T}\mathsf{YPE}(\mathbb{T})\hookrightarrow \mathsf{C}\mathsf{TX}(\mathbb{T})$$

一般来说, 这是一个真子范畴. 不过之后我们会看到, 如果 $\mathbb{T}$ 包含 $\text{𝟙}$ 类型和 $\Sigma$ 类型的话, 这两个范畴就自然等价了. 按照定义, 空语境到闭类型的态射 $\bullet \to A$ 实际上就是所谓的闭 term(closed term).

来个简单的例子:

例 1.5. 假设类型论 $\mathbb{T}$ 包含一个自然数对象 $\mathbb{N}$. 考虑 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的这两个态射:$$\bullet (m:\mathbb{N},n:\mathbb{N})\mathbb{N}(1,1)m+n$$它们的复合就是 $2:\bullet \to \mathbb{N}$.

预层与 Judgement

对于一个类型论 $\mathbb{T}$ 而言, 句法范畴上的预层范畴 $\mathcal{P}(\mathsf{C}\mathsf{TX}(\mathbb{T}))$ 也很重要. 一种简单的说法是, 类型论 $\mathbb{T}$ 中的每一类与 substitution 交换的 judgement 都会对应一个预层 $\mathcal{F}:\mathsf{C}\mathsf{TX}(\mathbb{T}{)}^{\mathsf{op}}\to \mathbf{Set}$, 并且每一个语境 $\Gamma$ 上的此类 judgement(商去某种自然定义的 judgemental equality 后): $$\Gamma ⊢\mathcal{J}$$都会精确对应预层上的一个元素: $$\mathcal{J}\in \mathcal{F}(\Gamma )$$反之任何预层也可看做是一类关于 $\mathbb{T}$ 的 judgement 类. 而 judgement 类之间的推导规则: $$\frac{\Gamma ⊢\mathcal{J}}{\Gamma ⊢{\mathcal{J}}^{\prime }}$$则对应预层之间的自然变换: $$\mathcal{F}\to {\mathcal{F}}^{\prime }$$从这个角度来说,$\mathcal{P}(\mathsf{C}\mathsf{TX}(\mathbb{T}))$ 可以被视作一种 logical framework, 它提供了描述 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 的元语言. 而 Yoneda 嵌入$$\mathsf{よ}:\mathsf{C}\mathsf{TX}(\mathbb{T})\to \mathcal{P}(\mathsf{C}\mathsf{TX}(\mathbb{T}))$$则是将语言嵌入元语言的映射. 方便起见, 我们之后不会在记号上区分 $\Gamma$ 和 $\mathsf{よ}(\Gamma )$.

为了进一步阐明这一点, 我们来考虑类型论中两种最基本的 judgement: $$\Gamma ⊢A\mathrm{type}\Gamma ⊢a:A$$

对应这两种 judgement, 我们来定义两个预层和它们间的自然变换: $$\mathsf{p}:\mathsf{tm}\to \mathsf{tp}$$

对于任意语境 $\Gamma$, $\mathsf{tp}(\Gamma )$ 是所有满足 $\Gamma ⊢A\mathrm{type}$ 的元素 $A$ 商去类型间 judgemental equality $A\equiv A^{\prime }$ 后的商集. 相应地, $\mathsf{tm}(\Gamma )$ 则是满足 $\Gamma ⊢a:A$ 的元素对 $(A,a)$ 商去 judgemental equality $A\equiv A^{\prime }$ 及 $a\equiv a^{\prime }$ 后的商集. 可以认为这里的 $A\in \mathsf{tp}(\Gamma )$. 最后我们定义: $$\mathsf{p}(A,a)=A$$

预层的函子性来自于这类 judgement 都与 substitution 交换, 也就是对于任意 substitution $\sigma :\Gamma \to \Delta$ 和 judgement $\mathcal{J}$, 我们有类型论中的规则: $$\frac{\Delta ⊢\mathcal{J}}{\Gamma ⊢\mathcal{J}\sigma }$$

对于任意范畴 $\mathcal{C}$, 和预层 $F\in \mathcal{P}(\mathcal{C})$, 我们有一个自然的范畴等价 ²: $$\mathcal{P}(\mathcal{C}{)}_{/F}\simeq \mathcal{P}({\mathcal{C}}_{/F})$$

2.	这里的 ${\mathcal{C}}_{/F}$ 指 comma category, 也被记作 $\mathcal{C}\downarrow F$. 当 $F$ 是预层时又被称为 category of elements, 常使用 $\int F$ 的记号.

而经由 $\mathsf{p}$, 预层 $\mathsf{tm}$ 成为 $\mathcal{P}(\mathsf{C}\mathsf{TX}(\mathbb{T}){)}_{/\mathsf{tp}}$ 中的对象, 因此我们也可以视其为 $\mathcal{P}(\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\mathsf{tp}})$ 中的对象, 它可以这样表述: 对于任意 $A:\mathsf{よ}(\Gamma )\to \mathsf{tp}$, 由 Yoneda 引理, 我们可以将其等同于元素 $A\in \mathsf{tp}(\Gamma )$. 此时一个 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\mathsf{tp}}$ 的对象可以看做一个元素对 $(\Gamma ,A)$, 其中 $\Gamma \in \mathsf{C}\mathsf{TX}(\mathbb{T})$, 而 $A\in \mathsf{tp}(\Gamma )$. 那么 $\mathsf{tm}$ 在其上的值就是: $$\mathsf{tm}(\Gamma ,A)=\{a|(A,a)\in \mathsf{tm}(\Gamma )\}$$也就是满足 $\Gamma ⊢a:A$ 的 $a$ 的集合. 为了方便起见, 接下来我们将不会区分 $\mathsf{tm}$ 的这两种形式.

注 1.6. 就像注 1.4 中所指出的, 一类 judgement 所对应的预层实际上无法还原最初的 judgement. 不过当我们试图对句法范畴中的概念作 judgement 的时候, 实际上只需要用到对应的预层. 因此从现在开始, 每当我们作出这样一个 judgement, 我们总是指对应预层中的元素.

例如, 当我们需要这样一个 judgement 时: $$\Gamma ⊢A\mathrm{type}$$我们其实是指一个元素: $$A\in \mathsf{tp}(\Gamma )$$在本文中无论多么复杂的 judgement 都可以这样翻译, 但很多时候这需要读者自己完成.

语境扩张

如果在某个 context $\Gamma$ 下有一个合法类型 $A$, 遵照类型论的基本规则, 我们可以扩充 $\Gamma$ 得到一个更大的 context $\Gamma .A=(\Gamma ,a:A)$. 为了标注自由变量的名字, 我们同时也使用 $\Gamma .(a:A)$ 的记法. 在这个新的 context 下, 自由变量 $a$ ³ 是 $A$ 的合法 term. 此时, 我们会在句法范畴 ⁴ 中得到一个交换方块:

$$\Gamma .A\mathsf{tm}\Gamma \mathsf{tp}\mathsf{q}\mathsf{p}\mathsf{p}A$$

在这个方块中, 下方的 $A$ 对应 judgement:

$$\Gamma ⊢A\mathrm{type}$$

上方的 $\mathsf{q}$ 称为 generic term, 对应 judgement:

$$\Gamma ,a:A⊢a:A$$

左侧的 $\mathsf{p}$⁵ 称为 projection. 它对于任何 substitution $(\sigma ,t):\Delta \to \Gamma .A$ 满足 $\mathsf{p}(\sigma ,t)=\sigma$. 由 Yoneda 引理, 这唯一确定了态射 $\mathsf{p}$. 其实 $\mathsf{q}$ 满足类似等式 $\mathsf{q}(\sigma ,t)=t$, 这也可作为 $\mathsf{q}$ 的另一种定义.

注 1.7. 态射 $\mathsf{q}:\Gamma .A\to \mathsf{tm}$ 总是对应一个自由变量. 因此如果语境清楚, 我们总是可以在没有命名的情况下, 使用 $\mathsf{q}$ 来指代这个类型为 $A$ 的自由变量. 这是一种局部无名 (locally nameless) 表示法. 更一般的, 如果我们有连续扩张: $${\mathsf{p}}^n:\Gamma .A_1.A_2...A_n\to \Gamma$$那么就有一列态射 (这里 $0\le k\le n$): $$\mathsf{q}{\mathsf{p}}^k:\Gamma .A_1.A_2...A_n\to \mathsf{tm}$$它们分别对应类型为 $A_{n-k}$ 的自由变量. 这实际上就是 de Brujin index.

3.	自由变量当然可以任意取名, 而不一定是 $a$. 我们也可以使用注 1.7 中的局部无名表示法.
4.	严格来说是在预层范畴 $\mathcal{P}(\mathsf{C}\mathsf{TX}(\mathbb{T}))$ 中. 不过方便起见, 我们就不区分这两种说法了.
5.	没错, 这和 $\mathsf{tm}$ 到 $\mathsf{tp}$ 的自然变换重名. 好在这一般不会造成混淆.

定理 1.8. 这是一个笛卡尔方块.

证明. 我们需要验证拉回的泛性质. 假设有一个交换方块: $$\Delta \mathsf{tm}\Gamma \mathsf{tp}t\sigma \mathsf{p}A$$

这个方块意味着什么? 答案是一个 judgement: $$\Delta ⊢t:A\sigma$$事实上这种方块和这类 judgement 是一一对应的. 现在我们可以构造一个交换图:

$$\Delta \Gamma .A\mathsf{tm}\Gamma \mathsf{tp}(\sigma ,t)t\sigma \mathsf{q}\mathsf{p}\mathsf{p}A$$

上方和左侧三角形的交换性就是等式 $\mathsf{p}(\sigma ,t)=\sigma$ 和 $\mathsf{q}(\sigma ,t)=t$. 我们由此得到泛性质的存在性部分, 而将这个论证倒过来则可以证明其唯一性.

$\square$

这给出了句法范畴上非常重要的附加结构, 称之为语境扩张 (context extension). 一个直接的推论是, 自然变换 $\mathsf{tm}\to \mathsf{tp}$ 其实是所谓的可表变换.

定义 1.9. 给定范畴 $\mathcal{C}$, 及其预层范畴 $\mathcal{P}(\mathcal{C})$ 中的自然变换 $\varphi :F\to G$. 如果对于任何对象 $X\in \mathcal{C}$ 和元素 $x\in F(X)$, 都存在拉回方块: $$\mathsf{よ}(Y)F\mathsf{よ}(X)G\mathsf{よ}(f)\varphi x$$

我们就称自然变换 $\varphi$ 是可表 (representable) 变换.

推论 1.10. 自然变换 $\mathsf{tm}\to \mathsf{tp}$ 是可表变换.

最后, 如果有两个语境 $\Gamma ,\Delta$, 并将 $\Delta$ 展开成 telescope: $$\Delta \equiv (a_1:A_1,a_2:A_2,...,a_n:A_n)$$那么我们用 $\Gamma .\Delta$ 来记如下一系列扩张后的语境: $$\Gamma .\Delta :=(\Gamma ,a_1:A_1,a_2:A_2,...,a_n:A_n)$$

可表态射

为了方便之后的论证, 我们来定义一个叫做可表态射的概念. 简而言之, 可表态射就是对应语境扩张的态射. 亦或者, 它们是一种性质良好的 fibration.

定义 1.11. 给定一个类型论 $\mathbb{T}$, 我们称句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中形如 $\mathsf{p}:\Gamma .A\to \Gamma$ 的态射为生成可表态射 (generating representable map). 如果一个态射是一系列生成可表态射的复合, 我们称其为可表态射 (representable map). 所有的生成可表态射记作 $\mathsf{G}\mathsf{EN}\mathsf{R}\mathsf{EP}(\mathbb{T})$, 而所有的可表态射记作 $\mathsf{R}\mathsf{EP}(\mathbb{T})$.

注 1.12. 换句话说, 可表态射其实就是这种态射: $${\mathsf{p}}^n:\Gamma .A_1.A_2...A_n\to \Gamma$$

注 1.13. 生成可表态射 $\mathsf{p}:\Gamma .A\to \Gamma$ 一般也被叫做 display map. 我们使用的术语来自 [1].

我们之后会看到, 如果类型论 $\mathbb{T}$ 包含外延相等类型, 所有的态射都同构于可表态射. 但一般来说, 这是不成立的.

注 1.14. 一个到空语境的态射 $A\to \bullet$ 是生成可表态射当且仅当 $A$ 是一个闭类型. 按定义, 所有到空语境的态射都是可表态射.

可表态射的一个重要性质是它们 stable under base change. 这可以从定理 1.8 直接推出.

定义 1.15. 给定范畴 $\mathcal{C}$, 和其中的一类态射 $\mathcal{S}\subseteq \mathrm{Mor}(\mathcal{C})$. 如果 $\mathcal{S}$ 中态射沿着任意态射的 base change 都存在, 并且 base change 后仍属于 $\mathcal{S}$, 那么我们称 $\mathcal{S}$ 是一个稳定类 (stable class).

定理 1.16. 生成可表态射类 $\mathsf{G}\mathsf{EN}\mathsf{R}\mathsf{EP}(\mathbb{T})$ 与可表态射类 $\mathsf{R}\mathsf{EP}(\mathbb{T})$ 都是稳定类.

笛卡尔积

这一节我们来解释为什么句法范畴总是容许有限乘积 (admits finite products). 首先, 正如我们一开始指出的 (定理 1.3), 空语境 $\bullet$ 是一个终对象.

引理 1.17. 对于任意语境 $\Gamma ,\Delta$, 语境 $\Gamma .\Delta$ 是它们在句法范畴中的乘积.

证明. 因为 $\Phi$ 到 $\Gamma .\Delta$ 的 substitution 一一对应于 $\Phi$ 分别到 $\Gamma$ 和 $\Delta$ 的一对 substitution.

$\square$

对任意范畴 $\mathcal{C}$, 其容许有限乘积当且仅当其包含终对象并且容许二元乘积. 我们立即可以由此推出:

定理 1.18. 句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 容许有限乘积.

2$\Pi$ 类型

现在假设我们的类型论 $\mathbb{T}$ 包含 $\Pi$ 类型 (简记作 $\mathbb{T}$ 包含 $\Pi$). 这意味着我们有如下的规则:

$$\mathrm{To}\mathrm{Be}Continued...$$

我们可以将这些规则利用预层翻译到句法范畴之上. 为此我们首先定义两个新的预层和它们间的自然变换: 对于任意语境 $\Gamma$:$${\mathsf{tp}}^{(2)}(\Gamma )=\{(A,B)|A\in \mathsf{tp}(\Gamma ),B\in \mathsf{tp}(\Gamma .A)\}$$$${\mathsf{tm}}_{\Pi }^{(2)}(\Gamma )=\{(A,B,b)|(A,B)\in {\mathsf{tp}}^{(2)}(\Gamma ),b\in \mathsf{tm}(\Gamma .A,B)\}$$$$\begin{array}{rl}{\mathsf{p}}_{\Pi }:{\mathsf{tm}}_{\Pi }^{(2)}& \to {\mathsf{tp}}^{(2)}\\ (A,B,b)& \mapsto (A,B)\end{array}$$

注 2.1. 这里及以后我们都会使用这种类似模式匹配 (pattern matching) 的写法来定义自然变换.

你可以认为 ${\mathsf{tp}}^{(2)}$ 实际上 classify 了一对 judgements⁶:$$\Gamma ⊢A\mathrm{type}\Gamma ,a:A⊢B\mathrm{type}$$而在此基础之上 ${\mathsf{tm}}_{\Pi }^{(2)}$ 则 classify 了:$$\Gamma ,a:A⊢b:B$$

注 2.2. 如果我们使用预层范畴的内语言 (internal language), 也就是将其作为一种类型论使用, 那么这里的两个预层可以等价地表述为:$${\mathsf{tp}}^{(2)}={\Sigma }_{(A:\mathsf{tp})}(\mathsf{tm}(A)\to \mathsf{tp})$$$${\mathsf{tm}}_{\Pi }^{(2)}={\Sigma }_{((A,B):{\mathsf{tp}}^{(2)})}{\Pi }_{(a:\mathsf{tm}(A))}Ba$$而 ${\mathsf{p}}_{\Pi }$ 则是到第一个变量的投影.

接下来, 我们把每个 $\Pi$ 类型的规则对应到预层之中. 首先 type formation 我们有自然变换:$$\begin{array}{rl}\Pi :{\mathsf{tp}}^{(2)}& \to \mathsf{tp}\\ (A,B)& \mapsto \Pi (A,B)\end{array}$$随后 term introduction 也就是 $\lambda$-abstraction 给出一个自然变换:$$\begin{array}{rl}\lambda :{\mathsf{tm}}_{\Pi }^{(2)}& \to \mathsf{tm}\\ (A,B,b)& \mapsto (\Pi (A,B),\lambda a.b)\end{array}$$

按定义我们有一个交换方块:$${\mathsf{tm}}_{\Pi }^{(2)}\mathsf{tm}{\mathsf{tp}}^{(2)}\mathsf{tp}\lambda {\mathsf{p}}_{\Pi }\mathsf{p}\Pi$$

接下来 term elimination 也就是 function application 会给出自然变换:$$\begin{array}{rl}\mathsf{app}:{\mathsf{tp}}^{(2)}{\times }_{\mathsf{tp}}\mathsf{tm}& \to {\mathsf{tm}}_{\Pi }^{(2)}\\ ((A,B),f)& \mapsto (A,B,f\mathsf{q})\end{array}$$

这里的拉回 ${\mathsf{tp}}^{(2)}{\times }_{\mathsf{tp}}\mathsf{tm}$ 取自上面方块的右下角. 而 $\mathsf{q}:\Gamma .A\to \mathsf{tm}$ 可以被看作类型为 $A$ 的自由变量.

6.	当然这里全部都要商去 judgemental equality.

定理 2.3. 刚刚的交换方块是一个笛卡尔方块.

证明. 我们只需要证明从泛性质得出的自然变换是一个同构:$$(\lambda ,{\mathsf{p}}_{\Pi }):{\mathsf{tm}}_{\Pi }^{(2)}\to {\mathsf{tp}}^{(2)}{\times }_{\mathsf{tp}}\mathsf{tm}$$它的逆其实就是 $\mathsf{app}$. 等式 $\mathsf{app}\circ (\lambda ,{\mathsf{p}}_{\Pi })=\mathsf{id}$ 和 $(\lambda ,{\mathsf{p}}_{\Pi })\circ \mathsf{app}=\mathsf{id}$ 分别对应 $\Pi$ 类型的 $\beta$ 和 $\eta$ 规则. 不信的话请验证一下吧.

$\square$

Exponential Object

这一小节将解释类型论中的 $\Pi$ 类型如何给出其句法范畴中可表态射间的 exponential object. 本小节所涉及的类型论 $\mathbb{T}$ 都包含 $\Pi$. 我们从最简单的情形: 一个生成可表态射 $\mathsf{p}:\Delta .A\to \Delta$ 开始.

引理 2.4. 存在关于 $\sigma :\Gamma \to \Delta$ 的自然同构: $${\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta }(\Gamma .A,\Delta .B)\simeq {\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta }(\Gamma ,\Delta .\Pi (A,B))$$这意味着 $\mathsf{p}:\Delta .\Pi (A,B)\to \Delta$ 是 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的一个 exponential object $\mathrm{F}(\Delta .A,\Delta .B)$.

证明. 选定 $\sigma :\Gamma \to \Delta$, 等式左侧的元素是二元组 $(\sigma ,b)$, 其中 $b$ 满足 judgement: $$\Gamma ,a:A⊢b:B$$而等式右侧的元素则是二元组 $(\sigma ,f)$, 其中 $f$ 满足 judgement: $$\Gamma ⊢f:\Pi (A,B)$$由此可知 $\lambda$ 和 $\mathsf{app}$ 能够给出 $b$ 和 $f$ 间的一一对应. 自然性嘛, 就留给读者作为练习.

$\square$

给定一个生成可表态射 $\mathsf{p}:\Delta .A\to \Delta$, 如果我们有另一个可表态射 ${\mathsf{p}}^m:\Delta .A.\overrightarrow{B}\to \Delta$, 其中: $$\Delta .A.\overrightarrow{B}\equiv (\Delta ,a:A,b_1:B_{1}a,b_2:B_2(a,b_1),...,b_m:B_m(a,b_1,b_2,...,b_{m-1}))$$

我们记 $\Delta .\Pi (A,\overrightarrow{B})$ 为如下语境: $$\Delta .(f_1:(a:A)\to B_{1}a).(f_2:(a:A)\to B_2(a,f_{1}a))...(f_m:(a:A)\to B_m(a,f_{1}a,f_{2}a,...,f_{m-1}a))$$

注意到 ${\mathsf{p}}^m:\Delta .\Pi (A,\overrightarrow{B})\to \Delta$ 是可表态射.

引理 2.5. 存在关于 $\sigma :\Gamma \to \Delta$ 的自然同构: $${\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta .A}(\Gamma .A,\Delta .A.\overrightarrow{B})\simeq {\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta }(\Gamma ,\Delta .\Pi (A,\overrightarrow{B}))$$

证明. 只需要对生成可表态射 $\mathsf{p}:\Delta .A\to \Delta$ 证明这个定理即可. 假设有可表态射 ${\mathsf{p}}^n:\Delta .A.\overrightarrow{B}\to \Delta .A$, 我们来证明有如下关于 $\sigma :\Gamma \to \Delta$ 的自然同构: $${\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta .A}(\Gamma .A,\Delta .A.\overrightarrow{B})\simeq {\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta }(\Gamma ,\Delta .\Pi (A,\overrightarrow{B}))$$证明的细节比较繁琐. 总之, 等式左侧的元素可看成一列元素: $$\overrightarrow{b}=(b_1,b_2,...,b_m)$$其满足: $$\begin{gathered} \Gamma ,a:A\sigma ⊢b_1:B_1(\sigma \mathsf{p},a) \\ \Gamma ,a:A\sigma ⊢b_2:B_2(\sigma \mathsf{p},a,b_1) \\ ... \\ \Gamma ,a:A\sigma ⊢b_m:B_m(\sigma \mathsf{p},a,b_1,b_2,...,b_{m-1}) \end{gathered}$$等式右侧的元素也可看做一列元素: $$\overrightarrow{f}=(f_1,f_2,...,f_m)$$其满足: $$\begin{gathered} \Gamma ⊢f_1:(a:A\sigma )\to B_1(\sigma \mathsf{p},a) \\ \Gamma ⊢f_2:(a:A\sigma )\to B_2(\sigma \mathsf{p},a,f_{1}a) \\ ... \\ \Gamma ⊢f_m:(a:A\sigma )\to B_m(\sigma \mathsf{p},a,f_{1}a,f_{2}a,...,f_{m-1}a) \end{gathered}$$现在我们借助 $\lambda$ 和 $\mathsf{app}$ 就能建立 $\overrightarrow{b}$ 和 $\overrightarrow{f}$ 间的一一对应.

$\square$

我们引入一个关于伴随函子的概念:

定义 2.6. 给定一个函子 $F:\mathcal{C}\to \mathcal{D}$, 如果对于某个 $X\in \mathcal{D}$ 存在对象 $\tilde{X}\in \mathcal{C}$ 和关于 $A$ 的自然同构: $${\mathrm{Hom}}_{\mathcal{D}}(F(A),X)\simeq {\mathrm{Hom}}_{\mathcal{C}}(A,\tilde{X})$$我们就称 $F$ 的右伴随在 $X\in \mathcal{C}$ 处有定义, 其值为 $\tilde{X}$.

将这个同构用两次就可以记得得到如下引理:

引理 2.7. 给定函子 $F:\mathcal{C}\to \mathcal{D}$ 和 $G:\mathcal{D}\to \mathcal{E}$, 如果对于 $X\in \mathcal{E}$ 我们有:

1.	函子 $G$ 的右伴随在 $X$ 处有定义, 其值为 $Y$;
2.	函子 $F$ 的右伴随在 $Y$ 处有定义, 其值为 $Z$.

那么函子 $G\circ F$ 的右伴随在 $X$ 处有定义, 其值为 $Z$.

本节的主要定理是:

定理 2.8. 如果类型论 $\mathbb{T}$ 包含 $\Pi$, 那么任意可表态射 $f:\Gamma \to \Delta$ 所诱导拉回函子 $f^{\ast }:\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }\to \mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Gamma }$ 的右伴随在可表态射处有定义, 并且其值仍是可表态射.

证明. 由引理 2.7, 我们只需要对生成可表态射 $\mathsf{p}:\Delta .A\to \Delta$ 作证明即可, 也就是引理 2.5.

$\square$

注 2.9. 我们一般用 $f_{\ast }$ 记这个右伴随.

对于任意范畴 $\mathcal{C}$ 和态射类 $\mathcal{S}\subseteq \mathrm{Mor}(\mathcal{C})$ 以及对象 $X\in \mathcal{C}$, 我们用 ${\mathcal{S}}_{/X}$ 记 ${\mathcal{C}}_{/X}$ 内由 $\mathcal{S}$ 中态射所组成的满子范畴.

推论 2.10. 如果类型论 $\mathbb{T}$ 包含 $\Pi$, 那么任意可表态射 $f:\Gamma \to \Delta$ 诱导的拉回函子 $f^{\ast }:\mathsf{R}\mathsf{EP}(\mathbb{T}{)}_{/\Delta }\to \mathsf{R}\mathsf{EP}(\mathbb{T}{)}_{/\Gamma }$ 有右伴随.

推论 2.11. 如果类型论 $\mathbb{T}$ 包含 $\Pi$, 那么对于任意语境 $\Gamma$, 范畴 $\mathsf{R}\mathsf{EP}(\mathbb{T}{)}_{/\Gamma }$ 是笛卡尔闭范畴 (cartesian closed category).

证明. 给定可表态射 $f:\Delta .\overrightarrow{A}\to \Delta$ 和 ${\mathsf{p}}^n:\Delta .\overrightarrow{B}\to \Delta$, 我们可以使用定理 2.8 得到关于 $\sigma :\Gamma \to \Delta$ 的自然同构: $${\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta }(\Gamma .\overrightarrow{A},\Delta .\overrightarrow{B})\simeq {\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta .\overrightarrow{A}}(\Gamma .\overrightarrow{A},f^{\ast }({\mathsf{p}}^n))\simeq {\mathrm{Hom}}_{\mathsf{C}\mathsf{TX}(\mathbb{T})/\Delta }(\Gamma ,f_{\ast }{f}^{\ast }({\mathsf{p}}^n))$$这说明 $f_{\ast }{f}^{\ast }({\mathsf{p}}^n)$ 就是我们需要的 exponential object.

$\square$

最后我们引入一个新术语来概括本节的主要内容 (见 [3] 定义 27):

定义 2.12. 给定有终对象的范畴 $\mathcal{C}$, 如果一个稳定类 $\mathcal{S}\subseteq \mathrm{Mor}(\mathcal{C})$, 满足如下条件:

1.	任意到终对象的态射都属于 $\mathcal{S}$;
2.	类 $\mathcal{S}$ 中的态射在复合下封闭;
3.	任意 $f:X\to Y\in \mathcal{S}$ 诱导的拉回函子 $f^{\ast }:{\mathcal{C}}_{/Y}\to {\mathcal{C}}_{/X}$ 在 $\mathcal{S}$ 处有右伴随.

我们就称 $\mathcal{S}$ 是一个闭类 (closed class).

推论 2.13. 如果类型论 $\mathbb{T}$ 包含 $\Pi$, 那么可表态射类 $\mathsf{R}\mathsf{EP}(\mathbb{T})$ 是闭类.

3外延相等

这一节我们来解释, 为何当你的类型论包含外延相等 (extensional identity) 类型时 (简记作 $\mathbb{T}$ 包含 ${\mathsf{Id}}_{\mathrm{ext}}$), 句法范畴将容许所有的有限极限 (admits finite limits). 首先外延相等的规则是:

$$\mathrm{To}\mathrm{Be}Continued...$$

我们首先来解释一下这些 jugdements 如何翻译成预层. Type formation 对应如下的自然变换:$$\begin{array}{rl}{\mathsf{Id}}_{\mathrm{ext}}:\mathsf{tm}{\times }_{\mathsf{tp}}\mathsf{tm}& \to \mathsf{tp}\\ ((a,A),(a^{\prime },A))& \mapsto a=a^{\prime }\end{array}$$Term introduction 对应一个交换方块. 这里 $\Delta$ 是对角映射 $\Delta (x)=(x,x)$, 而 $\mathsf{refl}(A,a)=(a=a,\mathsf{refl})$:$$\mathsf{tm}\mathsf{tm}\mathsf{tm}{\times }_{\mathsf{tp}}\mathsf{tm}\mathsf{tp}\mathsf{refl}\Delta \mathsf{p}{\mathsf{Id}}_{\mathrm{ext}}$$

我们可以由 equality reflection 推出这是一个笛卡尔方块.

对角映射

外延相等类型和对角映射 (diagonal map) 间有密切的联系.

定理 3.1. 如果类型论 $\mathbb{T}$ 包含 ${\mathsf{Id}}_{\mathrm{ext}}$, 那么句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中有同构 ⁷: $$\Gamma .A.A.(\mathsf{qp}=\mathsf{q})\simeq \Gamma .A$$

7.	我们在这里使用了局部无名法, 见注 1.7

证明. 这个同构由态射 $(\mathsf{id},\mathsf{q})$ 和 $(\mathsf{id},\mathsf{q},\mathsf{q},\mathsf{refl})$ 给出. 它们的互逆性需要用到 equality reflection.

$\square$

由此可知 $\mathsf{p}:\Gamma .A.A.(\mathsf{qp}=\mathsf{q})\to \Gamma .A.A$ 实际上就是对角映射.

可表态射与有限极限

本节的主要定理在此:

定理 3.2. 如果类型论 $\mathbb{T}$ 包含 ${\mathsf{Id}}_{\mathrm{ext}}$, 那么句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的所有态射都同构于某个可表态射.

证明. 选定一个态射 $\sigma :\Gamma \to \Delta$, 这里我们把语境展开成 telescope: $$\begin{gathered} \sigma =({\sigma }_1,{\sigma }_2,...,{\sigma }_n) \\ \Gamma =(x_1:X_1,x_2:X_2,...,x_m:X_m) \\ \Delta =(y_1:Y_1,y_2:Y_2,...,y_n:Y_n) \end{gathered}$$

先构造一个新的语境: $$\Sigma :=\Gamma .\Delta .({\sigma }_1=y_1).({\sigma }_2=y_2)...({\sigma }_n=y_n)$$

我们有如下 substitution, 它可以使得 $\Sigma$ 成为 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 中的对象: $$y:=(y_1,y_2,...,y_n):\Sigma \to \Delta$$

使用 equality reflection 可得 $y=({\sigma }_1,{\sigma }_2,...,{\sigma }_n)$, 由此我们可以定义两个 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 中的态射: $$\begin{gathered} x:=(x_1,x_2,...,x_n):\Sigma \to \Gamma \\ f:=(x_1,x_2,...,x_n,{\sigma }_1,{\sigma }_2,...,{\sigma }_n,\mathsf{refl},\mathsf{refl},...,\mathsf{refl}):\Gamma \to \Sigma \end{gathered}$$

可以验证 $x$ 和 $f$ 实际上互为逆映射, 因而 $\Sigma \simeq \Gamma \in \mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$. 再由对称性知在 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 中有同构: $$\Sigma \simeq \Delta .\Gamma .({\sigma }_1=y_1).({\sigma }_2=y_2)...({\sigma }_n=y_n)$$

而上式右侧是一个可表态射, 因此 $\sigma$ 同构于一个可表态射.

$\square$

本小节开头的断言就是一个直接的推论:

推论 3.3. 如果类型论 $\mathbb{T}$ 包含 ${\mathsf{Id}}_{\mathrm{ext}}$, 那么句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 容许所有有限极限.

证明. 只需证明句法范畴有终对象和关于所有态射的 base change. 前者可以取空语境 $\bullet$. 而对于后者, 我们知道关于可表态射的 base change 总是存在 (定理 1.16), 而定理 3.2 表明所有的态射都同构于可表态射, 因此关于一切态射的 base change 都存在.

$\square$

4局部笛卡尔闭范畴

经由之前的讨论, 我们可以立即得到这个众所周知的定理:

定理 4.1. 如果类型论 $\mathbb{T}$ 包含 $\Pi$ 和 ${\mathsf{Id}}_{\mathrm{ext}}$, 那么句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 是局部笛卡尔闭范畴.

证明. 在命题给出的条件下, 推论 3.3 说明句法范畴容许有限极限, 只需要再验证对于任意语境 $\Delta$, 范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 都是笛卡尔闭范畴. 换句话说, 就是对于任意 $\Gamma ,\Phi \in \mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$, 对应的 exponential object $\mathrm{F}(\Gamma ,\Phi )$ 总是存在. 由定理 3.2, 我们可以假设 $\Gamma ,\Phi$ 都是可表态射, 此时使用定理 2.11 即可.

$\square$

注 4.2. 这个定理最初来自于 [2]. 不过我们的版本条件更宽松, 只要求类型论 $\mathbb{T}$ 包含 $\Pi$ 和 ${\mathsf{Id}}_{\mathrm{ext}}$.

5$\text{𝟙}$ 类型

现在我们假设 $\mathbb{T}$ 包含单位类型, 或者叫 $\text{𝟙}$ 类型 (简记为 $\mathbb{T}$ 包含 $\text{𝟙}$):$$⊢\text{𝟙}\mathrm{type}$$$$⊢\ast :\text{𝟙}$$并且 $\text{𝟙}$ 类型满足 $\eta$ 规则:$$\frac{\Gamma ⊢t:\text{𝟙}}{\Gamma ⊢t\equiv \ast }$$

我们也可以加入 type eliminator rule, 不过这其实是 admissible 的.

这些 judgement 比较容易翻译,type formation 就是空语境下的一个元素:$$\text{𝟙}\in \mathsf{tp}(\bullet )$$

由于 $\bullet$ 是终对象, 这等价于预层 $\mathsf{tp}$ 的一个整体截面 (global section). Term introduction 也是一个元素:$$\ast \in \mathsf{tm}(\bullet ,\text{𝟙})$$

这也可看成是一个三角形:$$\mathsf{tm}\bullet \mathsf{tp}\mathsf{p}\text{𝟙}\ast$$

而 $\eta$ 规则则对应下面的方块总是笛卡尔方块:$$\Gamma \mathsf{tm}\Gamma \mathsf{tp}\ast \mathsf{id}\mathsf{p}\text{𝟙}$$或者说 $\text{𝟙}$ 关于 $\mathsf{p}$ 的 lifting 存在且唯一.

终对象

定理 5.1. 如果类型论 $\mathbb{T}$ 包含 $\text{𝟙}$, 那么 $\text{𝟙}$ 是句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 的一个终对象.

证明. 任何 $\sigma :\Gamma \to \text{𝟙}$ 满足: $$\Gamma ⊢\sigma :\text{𝟙}$$由 $\text{𝟙}$ 类型的 $\eta$ 规则, 我们只能有一个这样的 $\sigma$, 也就是 $\ast$.

$\square$

注 5.2. 由终对象的唯一性, 我们知道在句法范畴中空语境同构于 $\text{𝟙}$ 类型: $$\bullet \simeq \text{𝟙}$$

6$\Sigma$ 类型

现在我们假设 $\mathbb{T}$ 包含 $\Sigma$ 类型 (简记为 $\mathbb{T}$ 包含 $\Sigma$), 也就是说 $\mathbb{T}$ 有如下规则:$$\mathrm{To}\mathrm{Be}Continued...$$

如果我们将这些 judgements 翻译到预层上, 那么 type formation 类似于 $\Pi$ 类型的情形:$$\begin{array}{rl}\Sigma :{\mathsf{tp}}^{(2)}& \to \mathsf{tp}\\ (A,B)& \mapsto \Sigma (A,B)\end{array}$$

接下来, 我们先定义一个新预层 ${\mathsf{tm}}_{\Sigma }^{(2)}$ 和一个自然变换 ${\mathsf{p}}_{\Sigma }$. 对于任意语境 $\Gamma$:$${\mathsf{tm}}_{\Sigma }^{(2)}(\Gamma )=\{(A,B,a,b)|(A,B)\in {\mathsf{tp}}^{(2)}(\Gamma ),a\in \mathsf{tm}(\Gamma ,A),b\in \mathsf{tm}(Ba)\}$$$$\begin{array}{rl}{\mathsf{p}}_{\Sigma }:{\mathsf{tm}}_{\Sigma }^{(2)}& \to {\mathsf{tp}}^{(2)}\\ (A,B,a,b)& \mapsto (A,B)\end{array}$$

注 6.1. 如果我们使用预层范畴的内语言, 那么这里的预层可以等价地表述为:$${\mathsf{tm}}_{\Sigma }^{(2)}={\Sigma }_{((A,B):{\mathsf{tp}}^{(2)})}{\Sigma }_{(a:\mathsf{tm}(A))}Ba$$而 ${\mathsf{p}}_{\Sigma }$ 则是到第一个变量的投影.

此时 term introduction 对应自然变换:$$\begin{array}{rl}\mathsf{pair}:{\mathsf{tm}}_{\Sigma }^{(2)}& \to \mathsf{tm}\\ (A,B,a,b)& \mapsto (\Sigma (A,B),\mathsf{pair}(a,b))\end{array}$$

按定义我们有一个交换方块:$${\mathsf{tm}}_{\Sigma }^{(2)}\mathsf{tm}{\mathsf{tp}}^{(2)}\mathsf{tp}\mathsf{pair}{\mathsf{p}}_{\Sigma }\mathsf{p}\Sigma$$

而 $\Sigma$ 类型的 $\beta$ 与 $\eta$ 规则则对应这个方块是笛卡尔方块.

闭类型范畴

如果 $\mathbb{T}$ 包含 $\Sigma$, 那么它句法范畴的结构会大幅简化. 这是因为除了空语境, 所有的 telescope 都会等价于一个单独的闭类型. 方便起见, 我们假设 $\mathbb{T}$ 也包含 $\text{𝟙}$, 这样就可以包括所有的情形. 给定一个语境 $\Gamma$ 并将其展开成 telescope: $$(a_1:A_1,a_2:A_2,...,a_n:A_n)$$我们定义 $\Sigma (\Gamma )$ 为如下的一系列 $\Sigma$ 类型的组合: $${\Sigma }_{(a_1:A_1)}{\Sigma }_{(a_2:A_2)}...{\Sigma }_{(a_{n-1}:A_{n-1})}{A}_n$$当然特殊情形 $n=0,1$ 需要定义. 对于空语境, 也就是 $n=0$ 时, 我们定义: $$\Sigma (\bullet )=\text{𝟙}$$而 $n=1$ 时, 我们则将其定义为对应的闭类型: $$\Sigma (A)=A$$实际上 $\Sigma$ 可以看做是 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 到 $\mathsf{T}\mathsf{YPE}(\mathbb{T})$ 的函子. 我们用 $\iota$ 记 $\mathsf{T}\mathsf{YPE}(\mathbb{T})$ 到 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 的自然嵌入.

定理 6.2. 如果类型论 $\mathbb{T}$ 包含 $\text{𝟙}$ 和 $\Sigma$, 那么 $\iota$ 是一个范畴等价. 或者说闭类型范畴等价于整个句法范畴: $$\mathsf{T}\mathsf{YPE}(\mathbb{T})\simeq \mathsf{C}\mathsf{TX}(\mathbb{T})$$

证明. 请读者验证 $\Sigma \circ \iota \simeq \mathsf{Id}$ 和 $\iota \circ \Sigma \simeq \mathsf{Id}$, 很简单的.

$\square$

注 6.3. 从定理 6.2 可以看出, 即便类型论 $\mathbb{T}$ 不包含 $\Sigma$, 它的句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 也会表现得好像包含 $\Sigma$ 类型. 而语境扩张相当于构造 $\Sigma$ 类型. 实际上本文中的许多证明都借助了这一点. 如果 $\mathbb{T}$ 包含 $\Sigma$, 这些证明 (起码在记号上) 就可以简化. 读者不妨自己试一试.

同样的构造可以应用到任意语境 $\Gamma$ 下, 从而证明:

定理 6.4. 如果类型论 $\mathbb{T}$ 包含 $\text{𝟙}$ 和 $\Sigma$, 那么其句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的可表态射等价于生成可表态射: $$\mathsf{G}\mathsf{EN}\mathsf{R}\mathsf{EP}(\mathbb{T})\simeq \mathsf{R}\mathsf{EP}(\mathbb{T})$$

使用定理 3.2 和定理 6.4 我们可以推出:

推论 6.5. 如果类型论 $\mathbb{T}$ 包含 $\text{𝟙}$, $\Sigma$ 和 ${\mathsf{Id}}_{\mathrm{ext}}$, 那么其句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中所有态射都等价于生成可表态射.

最后合并定理 4.1 和定理 6.2 我们可以得到:

推论 6.6. 如果类型论 $\mathbb{T}$ 包含 $\text{𝟙}$, $\Sigma$, $\Pi$ 和 ${\mathsf{Id}}_{\mathrm{ext}}$, 那么其闭类型范畴 $\mathsf{T}\mathsf{YPE}(\mathbb{T})$ 是局部笛卡尔闭范畴.

7内涵相等

当类型论 $\mathbb{T}$ 不再是外延的 (譬如在同伦类型论的情形下), 而是包含内涵相等 (intensional equality) 类型时 (简记为 $\mathbb{T}$ 包含 $\mathsf{Id}$), 其句法范畴的结构会变得更加丰富. 同伦类型论 (homotopy type theory) 就是这样一种情形. 这一节我们就来解释这件事.

内涵相等的规则是:$$\mathrm{To}\mathrm{Be}Continued...$$

Judgement 到预层的翻译和外延相等的情形很相似. Type formation 对应如下的自然变换:$$\begin{array}{rl}\mathsf{Id}:\mathsf{tm}{\times }_{\mathsf{tp}}\mathsf{tm}& \to \mathsf{tp}\\ ((a,A),(a^{\prime },A))& \mapsto a=a^{\prime }\end{array}$$

Term introduction 对应一个交换方块. 这里 $\Delta$ 是对角映射 $\Delta (x)=(x,x)$, 而 $\mathsf{refl}(A,a)=(a=a,\mathsf{refl})$:$$\mathsf{tm}\mathsf{tm}\mathsf{tm}{\times }_{\mathsf{tp}}\mathsf{tm}\mathsf{tp}\mathsf{refl}\Delta \mathsf{p}\mathsf{Id}$$

但这个方块不再是笛卡尔方块. 事实上它的笛卡尔性等价于 equality reflection. 内涵相等的 $\mathsf{J}$ 规则对应一个 extension-lifting problem. 对于如下任意交换方块 ⁸, 都存在对角方向的映射使整个图交换:$$\Gamma .A\mathsf{tm}\Gamma .A.A.(\mathsf{qp}=\mathsf{q})\mathsf{tp}\delta (\mathsf{id},\mathsf{q},\mathsf{q},\mathsf{refl})\mathsf{p}P\mathsf{J}(P,\delta )$$事实上, 左上角三角形的交换性对应 $\beta$ 规则, 而右下角三角形的交换性对应 term elimination.

8.	我们在这里使用了局部无名法, 见注 1.7

注 7.1. 我们可以纯粹使用预层表述 $\mathsf{J}$ 规则, 而不用涉及语境扩张. 不过这件事稍微有些复杂, 详情请见 [3].

$\mathsf{J}$ 规则与提升性质

刚刚我们所使用的是双侧对称形式的 $\mathsf{J}$ 规则, 但我们在之后的内容中会用到单侧的 $\mathsf{J}$ 规则. 这两种形式是完全等价的, 一个证明可在 [4] 中找到. 用预层来表述, 单侧 $\mathsf{J}$ 规则就是对于任何 $a\in \mathsf{tm}(\Gamma ,A)$, 如下的提升问题总有解: $$\Gamma \mathsf{tm}\Gamma .A.(a=\mathsf{q})\mathsf{tp}\delta (\mathsf{id},a,\mathsf{refl})\mathsf{p}P\mathsf{J}(P,\delta )$$

方便起见, 我们将使用 $\mathsf{i}$ 来记左侧态射 $(\mathsf{id},\mathsf{q},\mathsf{q},\mathsf{refl})$. 如同可表态射 ${\mathsf{p}}^n$, 我们可以使用更一般的记号: $${\mathsf{i}}^n:\Gamma \to \Gamma .A_1.(a_1=\mathsf{q}).A_2.(a_2=\mathsf{q})...A_n.(a_n=\mathsf{q})$$这里 $a_i$ 满足: $$a_i\in \mathsf{tm}(\Gamma .A_1.(a_1=\mathsf{q}).A_2.(a_2=\mathsf{q})...A_{i-1}.(a_{i-1}=\mathsf{q}),A_n)$$方便起见我们会使用如下简写: $${\mathsf{i}}^n:\Gamma \to \Gamma .{\overrightarrow{A}}_{\mathsf{Id}}$$我们称这样形如 ${\mathsf{i}}^n$ 的态射为 elementary acyclic cofibration ⁹. 现在基于单侧 $\mathsf{J}$ 规则的提升性质, 我们可以解决句法范畴中的一整类提升问题:

引理 7.2. 假设类型论 $\mathbb{T}$ 包含 $\mathsf{Id}$. 给定句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的 elementary acyclic cofibration ${\mathsf{i}}^m$ 和可表态射 ${\mathsf{p}}^n$, 如下的提升问题总有解: $$\Gamma \Delta .\overrightarrow{B}\Gamma .{\overrightarrow{A}}_{\mathsf{Id}}\Delta {\mathsf{i}}^m{\mathsf{p}}^n$$

证明. 只需注意到在相对提升问题中, 右侧态射在 base change 下封闭, 且左侧和右侧态射都在复合下封闭即可.

$\square$

9.	这是作者为了方便临时起的名字, 并不是标准术语 (似乎本来就没有标准术语).

弱分解系统

在本小节我们来解释, 当 $\mathbb{T}$ 包含 $\mathsf{Id}$ 时, 句法范畴内会自然地形成一个弱分解系统 (见 [5]).

定义 7.3. 给定一个范畴 $\mathcal{C}$ 和其中的两个态射类 $\mathcal{L},\mathcal{R}\subseteq \mathrm{Mor}(\mathcal{C})$. 如果下面两个条件得到满足, 我们就称 $(\mathcal{L},\mathcal{R})$ 为 $\mathcal{C}$ 中的一组弱分解系统 (weak factorization system):

1.	(分解的存在性) 对于任何 $\mathcal{C}$ 中态射 $f$, 都存在 $l\in \mathcal{L}$ 和 $r\in \mathcal{R}$ 使得 $f=r\circ l$: $$ZXYrlf$$
2.	(提升性质) 对于任何满足 $l\in \mathcal{L}$ 和 $r\in \mathcal{R}$ 的交换方块, 都存在对角方向态射使得整个图交换: $$AXBYlr$$

在我们将要定义的弱分解系统中, $\mathcal{R}$ 就是所有的可表态射, 而 $\mathcal{L}$ 则简单粗暴地定义成所有相对于可表态射满足提升性质的态射.

定义 7.4. 给定范畴 $\mathcal{C}$ 和态射类 $\mathcal{S}\subseteq \mathrm{Mor}(\mathcal{C})$, 以及一个态射 $i\in \mathcal{C}$. 如果对于任意 $p\in \mathcal{S}$ 的 (如下) 方块, 都存在对角方向映射使得整个图交换: $$AXBYip$$我们就称 $i$ 满足关于 $\mathcal{S}$ 的左提升性质.

定义 7.5. 假设类型论 $\mathbb{T}$ 包含 $\mathsf{Id}$, 我们称关于可表态射满足左提升性质的态射为 acyclic cofibration. 全体 acyclic cofibration 构成的态射类记作 $\mathsf{AC}\mathsf{OF}(\mathbb{T})$.

此时定义 7.3 中的提升性质是平凡的, 我们只需要验证分解的存在性. 实际上我们的证明只涉及 elementary acyclic cofibration. 当然, 我们必须说明 elementary acyclic cofibration 的确是 acyclic cofibration. 这不过就是引理 7.2 换种说法. 我们在此重新叙述一遍:

引理 7.6. 所有的 elementary acyclic cofibration 都是 acyclic cofibration.

本节的主要定理是:

定理 7.7. 如果类型论 $\mathbb{T}$ 包含 $\mathsf{Id}$, 那么其句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的任何态射都可以分解为 elementary acyclic cofibration 和可表态射的复合 ¹⁰: $$\Phi \Gamma \Delta {\mathsf{p}}^n{\mathsf{i}}^m\sigma$$

10.	我们这里的说法并不完全正确, 严格来说只是同构于 elementary acyclic cofibration 和可表态射.

证明. 选定一个态射 $\sigma :\Gamma \to \Delta$, 这里我们把语境展开成 telescope: $$\begin{gathered} \sigma =({\sigma }_1,{\sigma }_2,...,{\sigma }_n) \\ \Gamma =(x_1:X_1,x_2:X_2,...,x_m:X_m) \\ \Delta =(y_1:Y_1,y_2:Y_2,...,y_n:Y_n) \end{gathered}$$

先构造一个新的语境: $$\Sigma :=\Gamma .\Delta .({\sigma }_1=y_1).({\sigma }_2=y_2)...({\sigma }_n=y_n)$$

我们有如下 substitution, 它可以使得 $\Sigma$ 成为 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 中的对象: $$y:=(y_1,y_2,...,y_n):\Sigma \to \Delta$$

我们可以定义一个 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 中的态射: $$f:=(x_1,x_2,...,x_n,{\sigma }_1,{\sigma }_2,...,{\sigma }_n,\mathsf{refl},\mathsf{refl},...,\mathsf{refl}):\Gamma \to \Sigma$$

再由对称性知在 $\mathsf{C}\mathsf{TX}(\mathbb{T}{)}_{/\Delta }$ 中有两个同构: $$\Sigma \simeq \Delta .\Gamma .({\sigma }_1=y_1).({\sigma }_2=y_2)...({\sigma }_n=y_n)$$$$\Sigma \simeq \Gamma .(y_1:Y_1).({\sigma }_1=y_1).(y_2:Y_2).({\sigma }_2=y_2)...(y_n:Y_n).({\sigma }_n=y_n)$$

第一式右侧是一个可表态射, 而我们可以通过第二式把 $f$ 看成一个 elementary acyclic cofibration, 这样就完成了证明.

$\square$

注 7.8. 这个证明和定理 3.2 的证明非常相似. 我们完全可以认为它们是同一个构造在两种不同相等类型上的应用.

结合引理 7.6 我们就立即可以得到以下推论:

推论 7.9. 如果类型论 $\mathbb{T}$ 包含 $\mathsf{Id}$, 那么其句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的 acyclic cofibration 和可表态射 $(\mathsf{AC}\mathsf{OF}(\mathbb{T}),\mathsf{R}\mathsf{EP}(\mathbb{T}))$ 构成弱分解系统.

最后我们引入一个新术语来概括本节的主要内容 (见 [3] 引理 29 前的定义):

定义 7.10. 给定范畴 $\mathcal{C}$ 和态射类 $\mathcal{S}\subseteq \mathrm{Mor}(\mathcal{C})$, 记 $\mathcal{A}$ 为全体关于 $\mathcal{S}$ 满足左提升性质的态射类. 如果 $(\mathcal{A},\mathcal{S})$ 构成一个弱分解系统, 我们就称 $\mathcal{S}$ 是一个分解类 (factorizing class).

推论 7.11. 如果类型论 $\mathbb{T}$ 包含 $\Pi$ 和 $\mathsf{Id}$, 那么可表态射类 $\mathsf{R}\mathsf{EP}(\mathbb{T})$ 是分解类.

8内涵类型论

这一节我们来研究内涵类型论 (intensional type theory) 的句法范畴. 首先我们对之前几节的内容做一个简单的概括:

定理 8.1. 如果类型论 $\mathbb{T}$ 包含 $\Pi$ 和 $\mathsf{Id}$, 那么可表态射类 $\mathsf{R}\mathsf{EP}(\mathbb{T})$ 是句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 中的稳定闭分解类 (stable, closed and factorizing class).

证明. 稳定性是定理 1.16, 闭性是定理 2.8 而分解性是推论 7.11.

$\square$

注 8.2. 外延类型论的句法范畴的是局部笛卡尔闭范畴 (见定理 4.1). 而定理 8.1 则可以看作是对应的内涵类型论版本.

9范畴语义

什么是范畴语义 (categorical semantics)? 如果用一句话概括, 范畴语义就是把一个类型论中的语句翻译到一个范畴当中去. 当然, 有很多基本问题需要阐明. 事实上, 如何翻译, 翻译到什么样的范畴里, 这些问题截至目前并没有标准答案, 现有的解决方案也不止一种. 在这一节里, 我们选择 category with families(简称为 CwF) 的理论来建立范畴语义.

定理 9.1. 给定一个类型论 $\mathbb{T}$, 它的句法范畴 $\mathsf{C}\mathsf{TX}(\mathbb{T})$ 是一个 CwF, 我们称其为项模型 (term model).

定理 9.2. 一个 ${\mathsf{CwF}}_{\mathbb{T}}$ 总是包含 $2$ 范畴意义下的始对象 (bi-initial object), 这个始对象被称为始模型 (initial model).

猜想 9.3. (Initiality Conjecture) 项模型是始模型.

严格来说, 这并不是一个猜想, 因为它依赖于我们究竟如何定义类型论 $\mathbb{T}$, 以及对应的 ${\mathsf{CwF}}_{\mathbb{T}}$. 事实上, 在很多的重要的情形下, 它已经被证明了.

参考文献

[1]	Uemura, T. (2019). A General Framework for the Semantics of Type Theory. https://arxiv.org/abs/1904.04097. arXiv.
[2]	Seely, R. A. G. (1984). Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95.1, pp. 33–48.
[3]	Awodey, S. (2018). Natural models of homotopy type theory. Mathematical Structures in Computer Science 28.2, pp. 241–286.
[4]	The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/. Institute for Advanced Study.
[5]	Gambino, N., Garner, R. (2008). The identity type weak factorisation system. Theoretical Computer Science 409(1), 94–109.