Yves Bertot

Inria

A naive view of Homotopy Type Theory and its relation to the calculus of constructions

Homotopy Type Theory is a recent evolution of Type Theory, where homotopy equivalence is used to give a new understanding to the notion of equality. This approach also makes it possible change the point of view we can have about inductive types and provides better tools to master the notion of quotients, which play a pervasive role in modern mathematics.