A Dependent type theory with Identity type. Or rather it's an umbrella term for several closely related such theories.
Wikipedia: Intuitionistic type theory
Identity type