## Definition ## __Intensional Martin-Loef type theory__ is a [[homotopy type theory]] with all [[W-types]]. ## See also ## * [[homotopy type theory]]