Although univalent foundations concern preservation of mathematical structure in general, strongly inspired by category theory, applications within homotopy theory are particularly actively investigated. Intensional type theory extended with the univalence axiom and so called higher inductive types is therefore also called “homotopy type theory”. We refer to the entry on  type theory for further details.