3 ms·

Funny seeing you here--I'm in 590 with Max and Eric. I saw Agda and guessed it was someone from the group :)