Independent researcher studying category theory and univalent type theories. Undergraduate student.