Cubical Type Theory
Complex Projective 4-Space 2018-04-09
Summary:
Previously, we discussed Homotopy Type Theory, which is an alternative foundation of mathematics with several advantages over ZFC, mainly for computer-assisted proofs. It is based on Martin-Löf’s intuitionistic type theory, but with the idea that types are spaces, terms are … Continue reading →