Small remark on cubical canonicity

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}.

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},