Homotopy Type Theory Intersection of: dependent type theory higher category theory homotopy theory type DependentTypeTheory { }