Hi!
I'm Rahul Chhabra (any pronouns work), PhD student in the Logic and Semantics group at Aarhus University. I work under Daniel Gratzer and Lars Birkedal. My primary interests are homotopy type theory, categorical realizability and higher category theory.
I have formalised in Cubical Agda a significant part of categorical realizability in my realizability project.