An Overview of Homotopy Type Theory and Formal Methods

Abstract

In this project, I have studied the basics of type theory, as a foundation for mathematics and a basis for theorem provers, using which we can formalize mathematical objects and proofs, and check their validity as well. I have taken up an example of representing graphs in type theoretic language to understand the formalization better. I have also studied homotopy type theory as an extension of Intuitionistic type theory, with the addition of univalence axiom and higher inductive types.