• Development of homotopy type theory in Agda

    Agda 181 43 Updated May 22, 2017
  • Homotopy type theory

    Coq 437 81 Updated May 20, 2017
  • A textbook on informal homotopy type theory

    TeX 1,156 250 Updated May 14, 2017
  • A formalization of M-types in Agda

    Agda 8 1 Updated Oct 17, 2016
  • coq

    Forked from coq/coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

    OCaml 20 153 Updated Aug 1, 2013
  • Archived materials related to Homotopy Type Theory.

    8 2 Updated Apr 24, 2012
  • Development of the univalent foundations of mathematics in Coq

    Coq 5 16 Updated Apr 24, 2012