Hey now... If you have a formulation in type theory (lean is not set theory), then you can translate to homotopy type theory fairly easily