I am a non-binary (they/them) mathematician and software engineer from Brazil, with an interest in Homotopy Type Theory, and formalised mathematics in general. Some of my projects include implementations of type theories and an accessible formalisation of HoTT: https://cubical.1lab.dev