So far the project has focussed on:

- Give an axiomatisation of the theory of multisets using type theory as a language to express the axioms.
- Construct a model of iterative multisets in homotopy type theory.
- Restrict the multiset model to set-like multisets, giving a HIT-free construction of the iterative hierchy of sets in HoTT.
- Construct two hiearchies of ∈-structures, each with one model in each homotopy level.
- Construct a model of non-wellfounded sets in HoTT.

- Multisets in type theory (Mathematical proceedings of the Cambridge Philosophical Society version)
- From multisets to sets in homotopy type theory (JSL 2018 version)
- Non-wellfounded sets in homotopy type theory

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! ☺