Calculational HoTT

TL;DR

This paper introduces a calculational approach to Homotopy Type Theory (HoTT), emphasizing linear proof formats, equality, and homotopic equivalences to facilitate formal proofs and potentially reshape HoTT's foundational framework.

Contribution

It formalizes deductive chains in HoTT as a linear calculational format for ICL, demonstrating their equivalence and proposing methods to find canonical functions between types.

Findings

Equational axioms of ICL have counterparts in HoTT.

Induction operators in HoTT are homotopic equivalences.

Calculational methods enable effective formal proofs in HoTT.

Abstract

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.