We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY.
- Authors
GYLTERUD, HÅKON ROBBESTAD
- Abstract
We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-Löf type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel's 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of "Homotopy Type Theory" by the Univalent Foundations Program.
- Subjects
HOMOTOPY theory; MARTIN'S axiom; ITERATIVE methods (Mathematics); SET theory; TYPE theory
- Publication
Journal of Symbolic Logic, 2018, Vol 83, Issue 3, p1132
- ISSN
0022-4812
- Publication type
Article
- DOI
10.1017/jsl.2017.84