module Authors where

About the Authors🔗

This is a page where everyone who adds to the 1lab can write a little bit about themselves. I mean it: everyone can write a bit about themselves! Try to follow the format of existing profiles in the source file, and keep the description short. Don’t forget to mention your pronouns.

Amélia's profile picture Amélia they/them @plt_amy

Hi! I’m Amélia, a non-binary programmer/mathematician. I’m 19, but I’ve been programming since age 7, and doing dependently-typed programming since 14. Last year, I implemented my own cubical type theory, to figure out what it was all about.

Since then, I’ve realised that my energy would be better spent making existing type theories more accessible, and this project was the result. The 1lab grew out of a personal project formalising category theory to better my understanding of category theory, and it’s currently undergoing a rewrite from base Agda-with-K to Cubical Agda.

My other notable projects include my personal blog, where I write about type theory and the implementation of programming languages, and Amulet, a ML-family language with an advanced type system.

Astra's profile picture Astra she/her @astradiol

Hey! I’m Astra, a Canadian trans graduate student in mathematics. Lately, my time has been equally spent divided between “real math” (e.g. thinking about category theory), “not-actual-math” (i.e. operating Agda in autopilot mode), and hanging out with my friends.

A cool project that I recently completed was formalising a categorical glueing argument for STLC.

Reed he/him @totbwf totbwf

Hey! I’m Reed! I develop proof assistants for a living, and write a lot of Agda. I’m interested in how we can make our tools more human friendly. In that vein, I like writing various forms of automation, especially those with a more semantic flavor.