  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.
