Misc

Author: Trebor-Huang

category.typ

@@ -235,8 +235,6 @@ $))
 
 (countermodel of Markov's principle)
 
-(optional: sheafification universe)
-
 === 自然模型的类型结构 <sec:natural-type-structure>
 
 Use internal language of presheaves to describe type structures
@@ -257,14 +255,22 @@ Use internal language of presheaves to describe type structures
 
 (also mention universes in sheaf topos)
 
-== 语法模型的泛性质
+== 语法与自由模型
 
 What are morphisms between models?
 
 mention sconing and gluing (dependent elimination)
 
 will use to prove canonicity etc later down the line
 
+/*
+类型论模型定义的重要特性是其中只要求等式。并非所有数学结构都可以这样定义。例如域是拥有四则运算的集合，其中除法的除数必须非零。因此在域的定义中就必须用到_不等式_。相对地，环则只拥有加法、减法与乘法，其中的结合律、分配律等等都是纯等式。这种数学结构称作#define[代数结构][algebraic structure]。群、环、向量空间都是代数结构，而域、全序、拓扑空间不是.#footnote[代数结构可以包含多个集合，而不一定只在一个集合上配备运算。这称作#define[多类][multi-sorted] 代数结构。类型论模型的另一个特别之处在于涉及的集合以元素为指标，例如 $"Tp"(Gamma)$ 对每个元素 $Gamma in "Ctx"$ 都有一个集合。这样的代数理论称作#define[广义代数理论][generalized algebraic theory]，或者 Cartmell 理论。]
+
+代数结构的一大特征是可以自由生成。换言之，给定一些元素，可以构造出_仅仅_满足代数结构本身要求的等式的结构。例如，一个元素 $x$ 在环的加法、减法、乘法下可以生成表达式 $x^2 + x - 2x$。这些表达式构成的环称作多项式环 $ZZ[x]$。具体来说，我们将给定的元素利用代数结构中的运算自由组合，将构造出的所有表达式商去需要满足的等式关系，得到的就是自由代数结构。
+
+当然，假如这个代数结构中有指定元素 (也就是零元运算，例如环公理要求乘法单位元 $1$)，那么不用给定元素，也能生成非平凡的代数结构。 (expand on this, syntax of groups vs free groups)
+*/
+
 == 模型的函子观点
 
 (a category of algebras, model is a map from an algebra to a specified subcategory)

examples.typ

@@ -360,7 +360,7 @@ $)
 
 1996 年，Hofmann 与 Streicher @groupoid-interpretation 提出了群胚模型，作为 K 原理的反模型。这不仅回答了这个问题，还为其独立性提供了清晰的解释。Martin-Löf 类型论中的类型不仅可以理解为集合，还可以视作_空间_。相等类型的元素则可以视作空间中两个点之间的全体道路构成的空间。这样，人们首次建立了类型论与同伦论之间的联系。为此，在与同伦相关的语境下，我们也将相等类型称作*道路类型*。
 
-在类型论的语法中，类型的定义表面上只会描述其元素的构成，而其中的道路则是 “自动生成” 的。例如给出一条 $A times B$ 中的道路就等价于同时给出 $A$ 中的道路与 $B$ 中的道路。再如函数 $(a, b : X) -> (a = b) -> (f(a) = f(b))$ 是靠 J 消去子定义的，无法在定义函数 $f$ 时控制此函数的表现。如果以空间作为模型，就可以精确控制道路的去处，进而给出各种命题的反模型。
+在类型论的语法中，类型的定义表面上只会描述其元素的构成，而其中的道路则是 “自动生成” 的。例如 $A times B$ 中的道路被 $A$ 与 $B$ 中的道路完全决定。再如定义函数 $f : X -> Y$ 时，自动附带了映射 $(a, b : X) -> (a = b) -> (f(a) = f(b))$。这是靠 J 消去子定义的，无法在定义函数 $f$ 时控制此映射的表现。如果以空间作为模型，就可以精确控制道路的去处，进而给出各种命题的反模型。
 
 === 群胚与道路
 

introduction.typ

@@ -111,16 +111,6 @@
   })
 ] <fig:set-family-substitution>
 
-/*
-(... move to categorical semantics)
-
-类型论模型定义的重要特性是其中只要求等式。并非所有数学结构都可以这样定义。例如域是拥有四则运算的集合，其中除法的除数必须非零。因此在域的定义中就必须用到_不等式_。相对地，环则只拥有加法、减法与乘法，其中的结合律、分配律等等都是纯等式。这种数学结构称作#define[代数结构][algebraic structure]。群、环、向量空间都是代数结构，而域、全序、拓扑空间不是.#footnote[代数结构可以包含多个集合，而不一定只在一个集合上配备运算。这称作#define[多类][multi-sorted] 代数结构。类型论模型的另一个特别之处在于涉及的集合以元素为指标，例如 $"Tp"(Gamma)$ 对每个元素 $Gamma in "Ctx"$ 都有一个集合。这样的代数理论称作#define[广义代数理论][generalized algebraic theory]，或者 Cartmell 理论。]
-
-代数结构的一大特征是可以自由生成。换言之，给定一些元素，可以构造出_仅仅_满足代数结构本身要求的等式的结构。例如，一个元素 $x$ 在环的加法、减法、乘法下可以生成表达式 $x^2 + x - 2x$。这些表达式构成的环称作多项式环 $ZZ[x]$。具体来说，我们将给定的元素利用代数结构中的运算自由组合，将构造出的所有表达式商去需要满足的等式关系，得到的就是自由代数结构。当然，假如这个代数结构中有指定元素 (也就是零元运算，例如环公理要求乘法单位元 $1$)，那么不用给定元素，也能生成非平凡的代数结构。
-
-这样的描述看上去与 #[@sec:prelim-type-theory]对语法的描述不谋而合。事实上，语法正是自由生成的模型，记作 $cal(T)$。换句话说，语法是依靠模型中的运算自由组合生成的结构，并且除了模型要求的等式之外不满足任何额外的等式。这就是为何我们对语法和语义使用同样的记号：语法是特殊的语义。如果有多个模型 $cal(M), cal(N)$，我们用 $"Tp"_cal(M)$ 等记号区分语义对象来自哪个模型。这样，如果要强调某个对象是语法对象，也可以直接写 $"Tp"_cal(T)$。
-*/
-
 === 类型结构
 
 不同的类型论会在以上的基础上添加各自的类型，因此在模型中也会相应的按照这些类型的规则定义类型结构。我们以几个常见的类型为例，展示这些类型结构的一般定义办法。这些定义只消对类型论规则作机械地改写即可得到，读者观察出规律即可跳过。读者也可以试着用定理证明助手形式化集合模型的构造，有助于消化其中微妙之处。

prerequisite.typ

@@ -56,7 +56,6 @@ $)
 这两种解释办法定义得到语法本质上是等价的，并且都自然地对应一种模型的定义。前者为每一种长度的语境都各自赋予一类对象，而后者将所有的语境放在一起。但是，数学实际中遇到的对象往往不会具有这样明确的长度结构。例如在集合中，$A times varnothing = varnothing$，因此没有办法区分一个空集究竟是几个集合的乘积。我们故而采用第二种观点，而将第一种观点下的相关定义称作#define[语境性][contextual] 的。不过，这两者实际上大同小异，只是细节处理上后者会更加优雅。
 
 为供读者参考，在@fig:substitution 中列出了第二种观点下需要添加的相关规则。其中并无难解之处，无非分为四组：代换之间的运算、代换作用于类型的性质、代换作用于元素的性质，最后还有语境扩展与代换的相互作用。读者也可参考 Angiuli 与 Gratzer 的教材~@type-theory-book。
-
 其中，$frak(p)$ 是从语境扩展 $(Gamma, A)$ 到 $Gamma$ 的代换，抛弃最后一个分量。同时应当有变量表达式 #eq($ Gamma, x : A tack x : A. $)但是 $A$ 是在语境 $Gamma$ 中的类型，所以严格来说需要经过 $frak(p)$ 代换之后才能在 $(Gamma, x : A)$ 语境下使用。在不使用变量名时，将元素表达式 $Gamma, x : A tack x : A$ 写作 $frak(q) in "Tm"((Gamma, A), A frak(p))$。这样，语境中从右向左的第 $n$ 个变量就应该写作 $frak(q) frak(p)^(n-1)$，与 de Bruijn 指标的写法类似。
 
 #numbered-figure(
@@ -423,7 +422,7 @@ ZFC 集合论中 C 指代的是*选择公理*，即给定一族集合 $X_(alpha
 
 给定两个基数 $kappa$ 与 $lambda$，取集合的不交并得到的新集合的基数写作 $kappa + lambda$，而取乘积得到的基数是 $kappa times lambda$。对于有限基数而言，这就是自然数的加法与乘法。假如集合 $A$ 与 $B$ 有限，那么从 $A$ 到 $B$ 的函数一共有 $abs(B)^(abs(A))$ 个，因为每个元素 $a in A$ 处的函数值都有 $abs(B)$ 种选择，而一共要选择 $abs(A)$ 次。因此，我们推广到无限基数时，也用函数集定义基数的幂 $lambda^kappa$。
 
-全体实数的基数，与任意非空区间 $(a, b)$、$[a, b]$、$[a, b)$ 等等的基数都相同，写作 $frak(c)$。由于区间 $[0,1]$ 的元素可以写作二进制小数，但是不同的小数可能表示同一个实数，因此有 $frak(c) <= 2^(aleph_0)$。反过来，考虑只含有 $1$ 与 $2$ 的十进制小数，共有 $2^(aleph_0)$ 个，并且两辆不同，因此 $frak(c) >= 2^(aleph_0)$。这样就能说明 $frak(c) = 2^(aleph_0)$。
+全体实数的基数，与任意非空区间 $(a, b)$、$[a, b]$、$[a, b)$ 等等的基数都相同，写作 $frak(c)$。由于区间 $[0,1]$ 的元素可以写作二进制小数，但是不同的小数可能表示同一个实数，因此有 $frak(c) <= 2^(aleph_0)$。反过来，考虑只含有 $1$ 与 $2$ 的十进制小数，共有 $2^(aleph_0)$ 个，并且两两不同，因此 $frak(c) >= 2^(aleph_0)$。这样就能说明 $frak(c) = 2^(aleph_0)$。
 
 === 序数