diff --git a/hott/algebra/binary.lean b/hott/algebra/binary.hlean
similarity index 100%
rename from hott/algebra/binary.lean
rename to hott/algebra/binary.hlean
diff --git a/hott/algebra/category/basic.lean b/hott/algebra/category/basic.hlean
similarity index 100%
rename from hott/algebra/category/basic.lean
rename to hott/algebra/category/basic.hlean
diff --git a/hott/algebra/group.lean b/hott/algebra/group.hlean
similarity index 100%
rename from hott/algebra/group.lean
rename to hott/algebra/group.hlean
diff --git a/hott/algebra/groupoid.lean b/hott/algebra/groupoid.hlean
similarity index 100%
rename from hott/algebra/groupoid.lean
rename to hott/algebra/groupoid.hlean
diff --git a/hott/algebra/precategory/basic.lean b/hott/algebra/precategory/basic.hlean
similarity index 100%
rename from hott/algebra/precategory/basic.lean
rename to hott/algebra/precategory/basic.hlean
diff --git a/hott/algebra/precategory/constructions.lean b/hott/algebra/precategory/constructions.hlean
similarity index 100%
rename from hott/algebra/precategory/constructions.lean
rename to hott/algebra/precategory/constructions.hlean
diff --git a/hott/algebra/precategory/functor.lean b/hott/algebra/precategory/functor.hlean
similarity index 100%
rename from hott/algebra/precategory/functor.lean
rename to hott/algebra/precategory/functor.hlean
diff --git a/hott/algebra/precategory/iso.lean b/hott/algebra/precategory/iso.hlean
similarity index 100%
rename from hott/algebra/precategory/iso.lean
rename to hott/algebra/precategory/iso.hlean
diff --git a/hott/algebra/precategory/morphism.lean b/hott/algebra/precategory/morphism.hlean
similarity index 100%
rename from hott/algebra/precategory/morphism.lean
rename to hott/algebra/precategory/morphism.hlean
diff --git a/hott/algebra/precategory/natural_transformation.lean b/hott/algebra/precategory/natural_transformation.hlean
similarity index 100%
rename from hott/algebra/precategory/natural_transformation.lean
rename to hott/algebra/precategory/natural_transformation.hlean
diff --git a/hott/algebra/relation.lean b/hott/algebra/relation.hlean
similarity index 100%
rename from hott/algebra/relation.lean
rename to hott/algebra/relation.hlean
diff --git a/hott/axioms/funext.lean b/hott/axioms/funext.hlean
similarity index 100%
rename from hott/axioms/funext.lean
rename to hott/axioms/funext.hlean
diff --git a/hott/default.lean b/hott/default.hlean
similarity index 100%
rename from hott/default.lean
rename to hott/default.hlean
diff --git a/hott/equiv_precomp.lean b/hott/equiv_precomp.hlean
similarity index 100%
rename from hott/equiv_precomp.lean
rename to hott/equiv_precomp.hlean
diff --git a/hott/init/equiv.lean b/hott/init/equiv.hlean
similarity index 100%
rename from hott/init/equiv.lean
rename to hott/init/equiv.hlean
diff --git a/hott/init/funext_from_ua.lean b/hott/init/funext_from_ua.hlean
similarity index 100%
rename from hott/init/funext_from_ua.lean
rename to hott/init/funext_from_ua.hlean
diff --git a/hott/init/funext_varieties.lean b/hott/init/funext_varieties.hlean
similarity index 100%
rename from hott/init/funext_varieties.lean
rename to hott/init/funext_varieties.hlean
diff --git a/hott/path.lean b/hott/init/path.hlean
similarity index 100%
rename from hott/path.lean
rename to hott/init/path.hlean
diff --git a/hott/axioms/ua.lean b/hott/init/ua.hlean
similarity index 100%
rename from hott/axioms/ua.lean
rename to hott/init/ua.hlean
diff --git a/hott/logic.lean b/hott/logic.hlean
similarity index 100%
rename from hott/logic.lean
rename to hott/logic.hlean
diff --git a/hott/pointed.lean b/hott/pointed.hlean
similarity index 100%
rename from hott/pointed.lean
rename to hott/pointed.hlean
diff --git a/hott/trunc.lean b/hott/trunc.hlean
similarity index 100%
rename from hott/trunc.lean
rename to hott/trunc.hlean
diff --git a/hott/types/W.lean b/hott/types/W.hlean
similarity index 100%
rename from hott/types/W.lean
rename to hott/types/W.hlean
diff --git a/hott/types/pi.lean b/hott/types/pi.hlean
similarity index 100%
rename from hott/types/pi.lean
rename to hott/types/pi.hlean
diff --git a/hott/types/prod.lean b/hott/types/prod.hlean
similarity index 100%
rename from hott/types/prod.lean
rename to hott/types/prod.hlean
diff --git a/hott/types/sigma.lean b/hott/types/sigma.hlean
similarity index 100%
rename from hott/types/sigma.lean
rename to hott/types/sigma.hlean