计算HoTT
Calculational HoTT
摘要：
我们在同伦类型理论（HoTT）中发现了一种表示直觉主义逻辑（ICL）的一阶版本的方法，对于直觉主义计算逻辑），其中，代替演绎树，相应的线性计算格式被用作形式证明工具;除此之外，等式和逻辑等价比蕴涵更优越。ICL的形式主义以前曾被一位作者从Dijkstra和Scholten提出的计算逻辑的经典版本改编为直觉主义逻辑。我们在HoTT中正式定义了\textit{deductive chains}作为ICL线性格式的表示。此外，我们使用这些演绎链证明了ICL的方程式公理和规则在HoTT中具有对应的。在这样做的过程中，我们意识到HoTT中基本类型的所有归纳算子实际上都是同伦等价的，这是我们在本文中证明的事实。此外，我们提出了一个非正式的方法来寻找类型之间的规范函数。我们认为，这些结果可能会导致一个完整的重述HoTT平等和同伦等价发挥了突出的作用。有了这种方法，并通过计算方法，有效和优雅的形式证明HoTT是可能的，通过提出的正式演绎链的方式适当的格式和符号。
英文摘要：
We found in Homotopy Type Theory (HoTT), a way of representing a first order version of intuitionistic logic (ICL), for intuitionistic calculational logic) where, instead of deduction trees, corresponding linear calculational formats are used as formal proof-tools; and besides this, equality and logical equivalence have preeminence over implication. ICL formalisms had been previously adapted by one of the authors to intuitionistic logic from the classical version of the calculational logic proposed by Dijkstra and Scholten. We formally defined \textit{deductive chains} in HoTT as a representation of the linear formats of ICL. Furthermore, we proved using these deductive chains, that the equational axioms and rules of ICL have counterparts in HoTT. In doing so, we realized that all the induction operators of the basic types in HoTT are actually, homotopic equivalences, fact that we proved in this paper. Additionally, we propose an informal method to find canonical functions between types. We think that these results could lead to a complete restatement of HoTT where equality and homotopic equivalence play a preeminent role. With this approach, and by way of calculational methods, effective and elegant formal proofs in HoTT are possible through the proposed formal deductive chains by way of appropriate formats and notations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
