You must enable JavaScript to use this site
  • 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.

  • News



    cicm2014 logo
    coimbra logo
Last modified: December 19 2016 18:02:45 CET