Merge pull request #7 from ice1k/main

一点微小的贡献

.github/workflows/main.yml

@@ -55,6 +55,7 @@ jobs:
           # glob_root_file: true
           root_file: "history.tex"
           latexmk_use_xelatex: true
+          latexmk_shell_escape: true
       - name: Upload PDF file
         uses: actions/upload-artifact@v3
         with:

.gitignore

@@ -12,4 +12,5 @@
 *.toc
 *.xdv
 .DS_Store
+/_minted-history
 title.tex

README.md

@@ -8,7 +8,7 @@
 
 An overview of the history of type theory, mainly for mathematically oriented people. I seek to achive these goals:
 - Provide a coherent and up-to-date source of information in Chinese.
-- Link to important books and papers I recommend to read.
+- Link to important books and papers I recommend reading.
 - Clear up some important misunderstandings.
 
 This is my coursework. I have already finished the submitted version (`d0aaf51`), but this is still being actively expanded. Suggestions and PR's are welcome!

chapters/hott.tex

@@ -344,6 +344,8 @@ \section{立方类型论}
 生成的立方体作为基础, 得到了ABCFHL模型
 与\textbf{积立方类型论}.
 
+立方类型论有自己的闭典范性定义, 在 2018 年由
+Huber~\cite{huber:2018:canonicity} 提出并证明.
 2021年, Sterling等人发展了范畴论工具, 证明了立方类型论的
 典范性. 在他的学位论文~\cite{sterling:2021:thesis}中,
 Sterling进一步描述了这些范畴论工具, 并且指出语法与语义研究
@@ -359,7 +361,7 @@ \subsection{立方类型论简介}
 它有两个端点 \(0,1\). 一个变量 \(i : \mathbb I\) 则表示
 区间上的一个点. 如果有多个变量, 则它们表示立方体中的某个坐标.
 在同伦类型论中, 相等类型的直觉是两点之间道路的空间. 在立方类型论
-中, 如果有一条套路 \(p : x =_A y\), 那么就允许我们取出这条
+中, 如果有一条道路 \(p : x =_A y\), 那么就允许我们取出这条
 道路上的某一点 \(p(i) : A\). 因此, \(\lambda i. p(i)\) 就是
 一个函数 \(\mathbb I \to A\), 而道路空间就可以看成是端点固定的
 函数空间.
@@ -394,5 +396,10 @@ \subsection{立方类型论简介}
 
 可以看到, 将相等类型使用道路空间的方式定义, 使得证明更加简洁直观.
 同时函数外延性在用泛等公理证明时十分复杂, 而使用立方类型论则是最基础的结论.
+
+立方类型论版本的闭典范性, 又叫立方闭典范性, 是指将传统意义上的闭典范性中的
+空语境换成完全由类型 \(\mathbb I\) 拼成的语境
+\(x_1:\mathbb I, x_2:\mathbb I, \cdots, x_n : \mathbb I\).
+
 希望继续了解立方类型论的读者可以
 参考\href{https://1lab.dev/1Lab.intro.html}{这篇文章}~\cite{amelia:2023:1lab}.

chapters/martin-lof.tex

@@ -287,13 +287,13 @@ \subsection{Coq}
 并且写完之后难以阅读. 读者可以尝试一下, 用于检测自己对类型论
 的知识是否熟悉. 在 Coq 中提供了\textbf{证明策略}(tactic)的语言,
 此时这个命题的证明可以写成
-\begin{verbatim}
+\begin{minted}{coq}
 Proof.
   intros m. induction m as [| m' H ].
   - apply add_zero.
   - rewrite add_succ. rewrite H. reflexivity.
 Qed.
-\end{verbatim}
+\end{minted}
 这与自然语言几乎完全一致. 第一句话用策略 \texttt{intros}
 引入了变量 \(m\), 第二句话对其进行归纳.
 这里 \(m'\) 就是在第二种情况下
@@ -357,28 +357,29 @@ \subsection{Agda}
 用户可以让Agda执行一些操作修改洞附近的代码, 在这个与
 软件合作的过程中逐步完成整个证明. 譬如证明定理
 \(\forall n. n + 0 = n\).
-\begin{verbatim}
+\begin{minted}{agda}
 theorem : (n : Nat) -> n + 0 == n
 theorem = ?
-\end{verbatim}
+\end{minted}
 这里的问号就是待填入的内容. 此时可以使用快捷键
 命令Agda引入变量, 它便会自动将代码修改为
-\begin{verbatim}
+\begin{minted}{agda}
 theorem : (n : Nat) -> n + 0 == n
 theorem n = ?
-\end{verbatim}
+\end{minted}
 接下来, 我们命令Agda对\(n\)归纳, 代码就会变为
-\begin{verbatim}
+\begin{minted}{agda}
 theorem : (n : Nat) -> n + 0 == n
 theorem zero = ?
 theorem (succ x) = ?
-\end{verbatim}
+\end{minted}
 以此类推. 由于这里类型系统强大的表达能力, 我们可以
 直接使用类型指导应该填入哪些东西.
 
 Agda实现了非常多前沿的类型论, 如可以开启立方类型论
-模式, 就能在立方类型论中进行定理证明. 因此, Agda 对类型论
-研究者非常友好, 便于进行实验.
+模式, 就能在立方类型论中进行定理证明. Agda 还支持
+自定义公理及其重写规则来模拟全新的类型论. 因此,
+Agda 对类型论研究者非常友好, 便于进行实验.
 
 \subsection{其他}
 
@@ -390,4 +391,5 @@ \subsection{其他}
 Nuprl 与 Andromeda 是基于外延类型论的计算机辅助证明软件.
 尽管上文中我们说过外延集合论中一个证明是否正确难以机械判定,
 但是这些软件中允许用户手动插入额外的说明, 用于帮助软件进行判断.
-
+Sterling、Favonia 等人在 Nuprl 的思想基础上开发了一种
+积立方类型论的原型实现 \textsf{{\color{red} Red}PRL}.

history.bib

@@ -458,6 +458,13 @@ @misc{henry:2019:constructive
   publisher = {arXiv},
   year      = {2019}
 }
+@article{huber:2018:canonicity,
+  doi       = {10.1007/s10817-018-9469-1},
+  journal   = {J Autom Reasoning},
+  author    = {Simon Huber},
+  title     = {Canonicity for Cubical Type Theory},
+  year      = {2018},
+}
 @article{cartmell:1986:contextualcat,
   title   = {Generalised algebraic theories and contextual categories},
   journal = {Annals of Pure and Applied Logic},

history.tex

@@ -9,6 +9,7 @@
 \usepackage{biblatex}
 \usepackage{hyperref}
 \usepackage{fontspec}
+\usepackage{minted}
 
 % Load computer modern font for e.g. cyrillic.
 % Referring by file name is needed