立方非正式类型论：高阶广群结构
Cubical informal type theory: the higher groupoid structure
摘要：
在同伦类型论一书中进行了一个为非正式类型论开发约定和符号的项目，该项目是为了建立一个框架，该框架是通过Voevodsky的univalance公理和更高的归纳类型来管理高维结构的公理来增强建设性类型论的，本文提出了一种以立方类型论为基础的非正式类型论的方法。为此，我们采用了一个立方体类型论最近提出的Angiuli，侯（Favonia）和哈珀，一个框架与累积层次的单价Kan宇宙，充分的univalence和实例的高归纳类型。本文只研究关于型的高广群结构的几个基本定理。
英文摘要：
Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of constructive type theory with axioms governing higher-dimensional constructions via Voevodsky's univalance axiom and higher-inductive types, this paper proposes a way of doing informal type theory with a cubical type theory as the underlying foundation instead. To that end, we adopt a cubical type theory recently proposed by Angiuli, Hou (Favonia) and Harper, a framework with a cumulative hierarchy of univalent Kan universes, full univalence and instances of higher-inductive types. In the present paper we confine ourselves to some elementary theorems concerning the higher groupoid structure of types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
