Sina Hazratpour

I'm a category theorists and I use category theory to make bridges between logic, algebraic topology, homotopy theory, higher category theory, and topos theory. I also  formalize various kinds of math into interactive theorem provers such as Lean 4. I also design and implement DSLs in Lean to make synthetic reasoning accessible to the users of Lean. Read more about my research interests on my personal website.