Kaluza-Klein Klub: Wiki
Home
About
Wiki
HoTT and \(\infty\)-categories
Dependant type theory is a formal way of writing a mathematical proof.
The equivalence in a type is analogous to homotopical equivalence in a topological space.
The natural language to study homotopy is \(\infty\)-category.
Homepage