From daef53e29d19cbfcb3d13720ee3c10fedb5fab35 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 4 Mar 2023 09:24:20 -0500
Subject: [PATCH 1/5] Apply highlighting to Coq code

---
 .github/workflows/main.yml | 1 +
 .gitignore                 | 1 +
 README.md                  | 2 +-
 chapters/martin-lof.tex    | 4 ++--
 history.tex                | 1 +
 5 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 6f49adc..bff9771 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -59,6 +59,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:
diff --git a/.gitignore b/.gitignore
index b6ae4f5..ead2d0c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,4 +12,5 @@
 *.toc
 *.xdv
 .DS_Store
+/_minted-history
 title.tex
\ No newline at end of file
diff --git a/README.md b/README.md
index 9fd0051..b7659a3 100644
--- a/README.md
+++ b/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!
diff --git a/chapters/martin-lof.tex b/chapters/martin-lof.tex
index 47fb47f..61c2e72 100644
--- a/chapters/martin-lof.tex
+++ b/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'\) 就是在第二种情况下
diff --git a/history.tex b/history.tex
index 1f24225..0fed52c 100644
--- a/history.tex
+++ b/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

From 4ed600e048b2a394e108a28d8c36bff43fbfd5d8 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 4 Mar 2023 09:34:19 -0500
Subject: [PATCH 2/5] Small remark on Agda & RedPRL

---
 chapters/martin-lof.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/chapters/martin-lof.tex b/chapters/martin-lof.tex
index 61c2e72..fa4c07f 100644
--- a/chapters/martin-lof.tex
+++ b/chapters/martin-lof.tex
@@ -377,8 +377,9 @@ \subsection{Agda}
 直接使用类型指导应该填入哪些东西.
 
 Agda实现了非常多前沿的类型论, 如可以开启立方类型论
-模式, 就能在立方类型论中进行定理证明. 因此, Agda 对类型论
-研究者非常友好, 便于进行实验.
+模式, 就能在立方类型论中进行定理证明. Agda 还支持
+自定义公理及其重写规则来模拟全新的类型论. 因此,
+Agda 对类型论研究者非常友好, 便于进行实验.
 
 \subsection{其他}
 
@@ -390,4 +391,5 @@ \subsection{其他}
 Nuprl 与 Andromeda 是基于外延类型论的计算机辅助证明软件.
 尽管上文中我们说过外延集合论中一个证明是否正确难以机械判定,
 但是这些软件中允许用户手动插入额外的说明, 用于帮助软件进行判断.
-
+Sterling、Favonia 等人在 Nuprl 的思想基础上开发了一种
+积立方类型论的原型实现 \textsf{{\color{red} Red}PRL}.

From 8a5f125a5884edbdd2c445d1bc19d3b7b429a773 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 4 Mar 2023 09:39:17 -0500
Subject: [PATCH 3/5] =?UTF-8?q?=E5=B0=91=E4=B8=80=E7=82=B9=E5=A5=97?=
 =?UTF-8?q?=E8=B7=AF?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 chapters/hott.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/chapters/hott.tex b/chapters/hott.tex
index 3eceb94..ee2e111 100644
--- a/chapters/hott.tex
+++ b/chapters/hott.tex
@@ -359,7 +359,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\), 而道路空间就可以看成是端点固定的
 函数空间.

From f5dac11f04d8442d8fe4c29bebd9a8d83d8bfa92 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 4 Mar 2023 10:01:29 -0500
Subject: [PATCH 4/5] Small remark on cubical canonicity

---
 chapters/hott.tex | 7 +++++++
 history.bib       | 7 +++++++
 2 files changed, 14 insertions(+)

diff --git a/chapters/hott.tex b/chapters/hott.tex
index ee2e111..56abfe6 100644
--- a/chapters/hott.tex
+++ b/chapters/hott.tex
@@ -344,6 +344,8 @@ \section{立方类型论}
 生成的立方体作为基础, 得到了ABCFHL模型
 与\textbf{积立方类型论}.
 
+立方类型论有自己的闭典范性定义, 在 2018 年由
+Huber~\cite{huber:2018:canonicity} 提出并证明.
 2021年, Sterling等人发展了范畴论工具, 证明了立方类型论的
 典范性. 在他的学位论文~\cite{sterling:2021:thesis}中,
 Sterling进一步描述了这些范畴论工具, 并且指出语法与语义研究
@@ -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}.
diff --git a/history.bib b/history.bib
index ff28459..c6623e2 100644
--- a/history.bib
+++ b/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},

From 46c07b0b7083ebbaf8aae065d7310fc890c6a7b0 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Sat, 4 Mar 2023 10:19:46 -0500
Subject: [PATCH 5/5] Add Agda pygments highlighter

---
 chapters/martin-lof.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/chapters/martin-lof.tex b/chapters/martin-lof.tex
index fa4c07f..c89337a 100644
--- a/chapters/martin-lof.tex
+++ b/chapters/martin-lof.tex
@@ -357,22 +357,22 @@ \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}
 以此类推. 由于这里类型系统强大的表达能力, 我们可以
 直接使用类型指导应该填入哪些东西.