Homotopy type theory (HoTT) is an exciting new research area combining homotopy theory and type theory using tools from higher category theory. This is the homepage of the HoTT research group in the Department of Philosophy at Carnegie Mellon University.