>>12207223>>12205803OK listen up
homotopy type theory is not a logical basis for math. The type theory formulation of math used in that book is called "Martin-Lof type theory."
"Homotopy type theory" is applying ML type theory to the study of topological homotopy (or vice versa.) HoTT is an _application_ of ML type theory.
If you don't know what homotopy is, then I'd suggest reading Topology by James Munkres before you get into HoTT
>>12206106You're not even wrong, ML type theory is cool but it can only make math more difficult.
>>12207330Ah yes, I remember being in 10th grade
