In mathematical logic and computer science, homotopy type theory (HoTT) includes various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.