Calculational HoTT

Ernesto Acosta, Bernarda Aldana, Jaime Bohorquez

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 deduct…