Multisets and sets in homotopy type theory

Håkon Robbestad Gylterud

This project has had two main focusses so far:


Agda formalisation

Some of the theorems of the above articles have been formalised in Agda:

Expecting a comment section? Feel free to e-mail me your comments, or otherwise contact me to discuss the content of this site. See my contact info. You can also write your opinion on your own website, and link back here! ☺