Hi there 👋

I'm Amélia (acceptable nicknames: Amy, Lia, Ame; acceptable pronouns: they/them), a Brazilian mathematician working independently on homotopy type theory and formalised category theory. I'm also a software engineer @obsidiansystems, where I work on making the web better with Haskell.

• 🔭 I work on the 1Lab (source), a formalised, cross-linked, explorable reference resource for cubical methods in homotopy type theory, featuring almost twenty thousand lines each of prose and of code. In addition to the mathematics, the project serves as an experiment for bringing Agda publishing on the web to 21st-century standards.

• ⏪ I worked on the type checker for the Amulet programming language, where I independently re-implemented many of GHC's trickier type system features, including (but not limited to) GADTs, type families, type classes with functional dependencies, and "quick look" impredicative polymorphism.

• 💬 Ask me about synthetic homotopy-coherent mathematics, synthetic homotopy theory, category theory, Haskell programming, and formalisation with Agda.

• 📫 How to reach me: Start by sending me a Twitter direct message at plt_amy, whence we can discuss an appropriate method of communication :)