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 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 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.