Multisets and sets in homotopy type theory

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.

Articles

• 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

Agda formalisation

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

• Read the description of the formalisation
• Download the formalisation