A small observation about Voevodsky's axiom of proposition resizing
I am @kang on Mathstodon
I've been and still am contributing to the Cubical Agda library. You can find my PRs here.
UN JOUR JE SERAI DE RETOUR PRÉS DE TOI