There is a funny typo (spell corrector maybe?): it's "Homotopy" not "Homeopaty" Type Theory