Multisets and sets in homotopy type theory
This project has had two main focusses so far:
- 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.
Some of the theorems of the above articles have been formalised in Agda:
- Read the description of the formalisation
- Download the formalisation