Misc

Author: Trebor-Huang

category.typ

@@ -73,7 +73,7 @@
   U edge(->) edge("d", ->) & "Tm" edgeL("d", ->, typeof)\
   1 edgeR(->, Unit) & "Tp"
 $))
-我们要求 $U$ 是单元素预层，即 $U -> 1$ 是预层同构.（不过注意 $Empty$ 不能要求拉回是空预层，因为某些语境下空类型是有元素的，例如 $x : Empty tack x : Empty$.）在 (...) 中还会进一步介绍如何用范畴语言处理其他类型结构。
+我们要求 $U$ 是单元素预层，即 $U -> 1$ 是预层同构.（不过注意 $Empty$ 不能要求拉回是空预层，因为某些语境下空类型是有元素的，例如 $x : Empty tack x : Empty$.）在 #[@sec:natural-type-structure]中还会进一步介绍如何用范畴语言处理其他类型结构。
 
 /*
 在预层范畴中的一切范畴构造都会附带代换操作。这样，范畴论的语言可以自动处理例如 $(A times B) sigma = A sigma times B sigma$ 的等式。我们完整叙述自然模型中乘积类型的定义为例。
@@ -108,7 +108,7 @@ $))
 - Justify mathematical motivation: dependent structures are hard to define
 - Alternative framework for models of type theory: comprehension categories
   - mention that this also ties into the already existing program of fibered category theory by Bénabou
-  - It's possible to have multiple $A$'s produce the same display map, so better have a projection $cal(E) -> cal(C)^->$
+  - It's possible to have multiple $A$'s produce the same display map (empty set example), so better have a projection $cal(E) -> cal(C)^->$
   - Elaborate on the morphism structure of $cal(E)$ (morphisms between types)
   - Substitution action: have a type $A : cal(E)$ over $Gamma$, should have a "pullback square"
   - Define Grothendieck fibrations
@@ -138,7 +138,11 @@ $))
     - presheaf categories
     - sheaves? maybe just over cantor space
 
-=== 自然模型的类型结构
+#definition[
+  假如有集合 $X$，配有两个集合 $X_0$、$X_1$ 与双射 $X tilde.equiv X_0 times X_1$，再配有集合 $X_00$、$X_01$、$X_10$、$X_11$ 与双射 $X_0 tilde.equiv X_00 times X_01$ 和 $X_1 tilde.equiv X_10 times X_11$，以此类推，就称此结构为 *Cantor 层*。Cantor 层之间的态射由一族映射 $f_b : X_b -> Y_b$ 组成，使得与配备的双射都交换。
+]
+
+=== 自然模型的类型结构 <sec:natural-type-structure>
 
 Use internal language of presheaves to describe type structures
 

examples.typ

@@ -282,7 +282,7 @@ $)
 $)
 证明见@sec:K-equivalences。我们在 #[@sec:set-model]的集合模型中已经说明了这与 Martin-Löf 类型论是相容的，因此不可能证伪该原理。它究竟可证还是独立，很长一段时间里都是未解之谜。
 
-1996 年，Hofmann 与 Streicher [?] 提出了群胚模型，作为 K 原理的反模型。这不仅回答了这个问题，还为其独立性提供了清晰的解释。Martin-Löf 类型论中的类型不仅可以理解为集合，还可以视作_空间_。相等类型的元素则可以视作空间中两个点之间的全体道路构成的空间。这样，人们首次建立了类型论与同伦论之间的联系。为此，在与同伦相关的语境下，我们也将相等类型称作*道路类型*。
+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$ 时控制此函数的表现。如果以空间作为模型，就可以精确控制道路的去处，进而给出各种命题的反模型。
 
@@ -319,7 +319,7 @@ $)
 
 群胚可以刻画空间的零维与一维同伦信息。一个自然的想法是能否同理给出刻画更高维信息的纯代数结构，乃至完全包含所有同伦信息。花些功夫可以定义出 2-群胚与 3-群胚等，但是定义的组合复杂度增长迅速，很难推广到无穷群胚的情况。对此的研究是高阶代数的来由。
 
-1991 年，Воеводский (Voevodsky) 与 Михаил Капранов (Mikhail Kapranov) 给出了一种无穷群胚的定义，并证明了这种无穷群胚能在同伦意义下表示所有的空间 [?]。但是 1998 年，由 Carlos Simpson~[?] 给出了反例，因此证明有误。事实上球面 $SS^2$ 就不在其表达能力范围内。然而，很长一段时间内，人们都没有明白错误在哪里，因此不清楚究竟是证明有误还是反例不成立。这件事是 Воеводский 转而追求形式化证明、发展同伦类型论的动机之一。
+1991 年，Воеводский (Voevodsky) 与 Михаил Капранов (Mikhail Kapranov) 给出了一种无穷群胚的定义，并证明了这种无穷群胚能在同伦意义下表示所有的空间 @inf-groupoid-homotopy-type。但是 1998 年，由 Carlos Simpson~@homotopy-type-3-groupoid 给出了反例，因此证明有误。事实上球面 $SS^2$ 就不在其表达能力范围内。然而，很长一段时间内，人们都没有明白错误在哪里，因此不清楚究竟是证明有误还是反例不成立。这件事是 Воеводский 转而追求形式化证明、发展同伦类型论的动机之一。
 
 === 模型定义
 
@@ -454,7 +454,7 @@ $)
 
 假设有汇编 $Gamma$ 与其上的汇编族 $A_x$，还有 $integral A$ 上的汇编族 $B_((x, a))$。定义 $Sigma$ 类型对应的汇编族 $(Sigma A B)_x$ 为不交并 $product.co_(a in A_x) B_((x, a))$，使得 $r realizes_((Sigma A B)_x) (a, b)$ 当且仅当 $r$ 是有序对程序 $P r_1 r_2$，满足 $r_1 realizes_A_x a$，并且 $r_2 realizes_B_((x, a)) b$。
 
-$Pi$ 类型的底集合则不是全体函数 $product_(a in A_x) B_((x, a))$，只包含可计算的依值函数。某个依值函数 $f$ 可计算，无非就是存在程序 $r$ 能实现它。这里，$r realizes_((Pi A B)_x) f$ 当且仅当 $s realizes_A_x a$ 时 $r s defined$，并且 $r s realizes_B_((x,a)) f(a)$。这样得到的汇编就仍然满足每个元素都至少有一个程序实现的要求。
+$Pi$ 类型的底集合则不是全体函数 $product_(a in A_x) B_((x, a))$，而只包含可计算的依值函数。某个依值函数 $f$ 可计算，无非就是存在程序 $r$ 能实现它。这里，$r realizes_((Pi A B)_x) f$ 当且仅当 $s realizes_A_x a$ 时 $r s defined$，并且 $r s realizes_B_((x,a)) f(a)$。这样得到的汇编就仍然满足每个元素都至少有一个程序实现的要求。
 
 对于自然数 $NN$ 或者 $Empty$ 与 $Unit$ 等类型，对应的汇编族直接不依赖 $x in Gamma$ 即可。这样，不难算出空语境中 $NN -> NN$ 的元素的确就与可计算函数一一对应。
 
@@ -508,21 +508,9 @@ You can improve to $Sigma$ type by searching the minimal one
 // - Define operational semantics on raw terms first, then fit a type system on it
 // - Relation to $Lambda$-realizability
 
-== 语义参数性
-
 == 语法翻译
 
 - syntactic version of the exception model/labelled function model
 - validate injectivity of type constructors via labels
   - trivial countermodel in set model, since $A times Empty = Empty$ strictly holds
-- parametricity??
-
-== 语法性质的证明
-
-- Promote to own chapter after category theory, only give brief review here
-
-  - Canonicity
-  - Normalization
-    - Injectivity of type constructors
-  - Parametricity? We can compare semantic and syntactic versions
 

impredicative.typ

@@ -1,7 +1,7 @@
 #import "common.typ": *
 = 非直谓宇宙 <appendix:impredicative>
 
-非直谓性在逻辑学和哲学中概念比较模糊，没有统一的定义。在类型论的语境中，非直谓性则具体指代函数类型 (或者 $Pi$ 类型) 所处的宇宙满足的规则。就一般直觉而言，假如类型 $A$ 在宇宙层级 $kappa$ 中，而 $B$ 在层级 $lambda$ 中，那么函数类型 $A -> B$ 应该取二者大者，即 $max{kappa, lambda}$。但是，如果某个宇宙层级是*非直谓*的，那么只要陪域 $B$ 在此层级中，任何函数类型 $A -> B$ 就也处在此层级中。
+非直谓性在逻辑学和哲学中概念比较模糊，没有统一的定义。在类型论的语境中，非直谓性则具体指代函数类型 (或者 $Pi$ 类型) 所处的宇宙满足的规则。就一般直觉而言，假如类型 $A$ 在宇宙层级 $kappa$ 中，而 $B$ 在层级 $lambda$ 中，那么函数类型 $A -> B$ 应该取其大者，即 $max{kappa, lambda}$。但是，如果某个宇宙层级是*非直谓*的，那么只要陪域 $B$ 在此层级中，任何函数类型 $A -> B$ 就也处在此层级中。
 
 具体来说，用 Tarski 宇宙描述的规则是
 #eq($
@@ -197,11 +197,6 @@ squash types and their impredicative encodings (compare with HoTT squashes)
 
 == 寓言一则
 
-- The universe structure of CoC, CIC and pCIC (in story)
-- talk about inductive types, large elimination, and squash types
-
----
-
 - Start with CoC
 - Add $"CC"_omega$
 - Add inductives to CIC
@@ -315,4 +310,4 @@ $)
 以上我们构造了 $pi : UU -> Bool^UU$ 与 $iota : Bool^UU -> UU$，满足 $pi compose iota = id_(Bool^UU)$。这其实足够导出 Russell 悖论，不过由于我们使用的是 $Bool$ 而不是 $"Prop"$，其最终结论是 $Bool$ 中的 $"true"$ 与 $"false"$ 相等，而非 $top <-> bot$。后者会使得一切命题都有证明，而前者仅仅使一切命题的证明都相等。
 ]
 
-(mention Diaconescu's theorem)
+// (mention Diaconescu's theorem)

main.typ

@@ -130,6 +130,8 @@ Trebor\ #v(1em)
 
 #include "category.typ"
 
+#include "syntax.typ"
+
 #include "model.typ"
 
 // Appendix numbering

model.typ

@@ -22,7 +22,7 @@ Sattler's model structure criteria?
 
 == 单纯集模型
 
-Воеводский (Voevodsky), paper by Chris Kapulkin and Peter LeFanu Lumsdaine
+Воеводский (Voevodsky), paper by Chris Kapulkin and Peter LeFanu Lumsdaine @simplicial-model
 
 Introduce fibrant types
 
@@ -36,6 +36,11 @@ Internal language and cartesian models
 
 Internal universes
 
+(homotopy canonicity??)
+
+problems with cubical models: they don't represent space
+$==>$ equivariant cubical model etc
+
 == 同伦类型论的内模型
 
 idea of using HoTT/2LTT to synthetically define infinity-models

prerequisite.typ

@@ -397,17 +397,27 @@ $)
 
 == 集合论撷英 <sec:set-theory>
 
-假设读者了解基数的基本定义。基数是度量集合元素个数的数学对象。例如每个自然数都是有限基数，而 $aleph_0$ 描述了全体自然数的数量，$frak(c)$ 表示全体实数的数量，等等。以下谈到的基数都指无限基数。
+// 假设读者了解基数的基本定义。基数是度量集合元素个数的数学对象。例如每个自然数都是有限基数，而 $aleph_0$ 描述了全体自然数的数量，$frak(c)$ 表示全体实数的数量，等等。以下谈到的基数都指无限基数。
 
 === 基数
 
+bijections and cardinals
+
+cardinal arithmetic
+
 === 序数
 
+well-founded orders
+
+well orders
+
+(the aleph series = well-founded cardinals)
+
 === 大基数理论
 
 依值类型论的模型不可避免涉及集合论与大基数的理论。例如直观上类型可以解释为集合，函数类型对应函数的集合，宇宙类型则是一定大小以内全体集合的集合。然而这是行不通的。例如在 ZFC 集合论中，就算限定集合只能包含一个元素，全体一元集也无法构成集合 #eq($ V_1 = {y mid(|) exists x bind y = {x}}. $) 假设不然，那么并集 $union.big V_1$ 按照公理也应该构成集合，但这恰好是全体集合的集合，在 ZFC 中是不能存在的。因此，我们需要发展一套理论，描述 “包含了足够多集合” 的集合。
 
-倘若我们的元理论也是类型论，并且本身包含宇宙的概念，那么可以利用元理论中的宇宙解释宇宙。但是这样做往往不很方便，并且需要元理论的规则高度匹配。有轶事一则： Martin-Löf~@mltt-1971 曾提出一套类型论，其中有 $cal(U) : cal(U)$，是不自洽的。但是论文中给出了自洽性的证明，其中元理论中也有 $cal(U) : cal(U)$ 的宇宙规则!
+倘若我们的元理论也是类型论，并且本身包含宇宙的概念，那么可以利用元理论中的宇宙解释宇宙。但是这样做往往不很方便，并且需要元理论的规则高度匹配。有轶事一则： Martin-Löf~@mltt-1971 曾提出一套类型论，其中有 $cal(U) : cal(U)$，是不自洽的，但是论文中却给出了自洽性的证明。其罪魁祸首在于元理论中也有 $cal(U) : cal(U)$ 的宇宙规则，本身就是不自洽的!
 
 在 ZFC 集合论中，给定基数 $kappa$，前面提到我们无法将全体元素个数少于 $kappa$ 的集合构成集合，这是因为尽管这些集合本身的大小有限制，但是它们的元素可以是任何别的集合，因此在数量上没有限制。假如我们要求不仅这些集合的元素个数少于 $kappa$，并且它们元素的元素个数也少于 $kappa$，元素的元素的元素等等都做如此要求，得到的东西称作#define(key: "hereditarily kappa-small set")[继承 $kappa$ 小集][hereditarily $kappa$-small set] $H_kappa$。例如，${varnothing, {varnothing}}$ 是继承有限集。可以证明 $H_kappa$ 构成集合。
 

references.yaml

@@ -151,3 +151,51 @@ independence-results-coc:
     title: Category Theory and Computer Science
     volume: 389
     publisher: Springer, Berlin, Heidelberg
+
+groupoid-interpretation:
+  type: article
+  title: The groupoid interpretation of type theory
+  author:
+    - Hofmann, Martin
+    - Streicher, Thomas
+  date: 1996
+  parent:
+    type: book
+    title: Twenty-five years of constructive type theory
+    volume: 36
+  page-range: 83-111
+  url: https://ncatlab.org/nlab/files/HofmannStreicherGroupoidInterpretation.pdf
+
+inf-groupoid-homotopy-type:
+  type: article
+  title: $infinity$-groupoids and homotopy types
+  author:
+    - Kapranov, M. M.
+    - Voevodsky, V. A.
+  date: 1991
+  page-range: 29-46
+  parent:
+    title: Cahiers de Topologie et Géométrie Différentielle Catégoriques
+    volume: 32
+    issue: 1
+  url: https://eudml.org/doc/91469
+
+homotopy-type-3-groupoid:
+  type: misc
+  note: ArXiv preprint
+  title: Homotopy types of strict 3-groupoids
+  author: Simpson, Carlos
+  date: 1998
+  serial-number:
+    doi: 10.48550/arXiv.math/9810059
+
+simplicial-model:
+  type: misc
+  note: ArXiv preprint
+  title: The Simplicial Model of Univalent Foundations (after Voevodsky)
+  author:
+    - Kapulkin, Chris
+    - Lumsdaine, Peter LeFanu
+  date: 2012
+  serial-number:
+    doi: 10.48550/arXiv.1211.2851

syntax.typ

@@ -0,0 +1,7 @@
+#import "common.typ": *
+= 语法性质的证明 <ch:syntax>
+
+- canonicity
+- normalization
+  - judgmental injectivity of type constructors
+- parametricity (syntactic and set-semantic)