{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T17:38:52Z","timestamp":1732037932607},"reference-count":5,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T00:00:00Z","timestamp":1540252800000},"content-version":"unspecified","delay-in-days":52,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2018,9]]},"abstract":"Abstract<\/jats:title>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\u00f6f type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel\u2019s 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 \u201cHomotopy Type Theory\u201d by the Univalent Foundations Program.<\/jats:p>","DOI":"10.1017\/jsl.2017.84","type":"journal-article","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T11:16:27Z","timestamp":1540293387000},"page":"1132-1146","source":"Crossref","is-referenced-by-count":3,"title":["FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY"],"prefix":"10.1017","volume":"83","author":[{"given":"H\u00c5KON ROBBESTAD","family":"GYLTERUD","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,10,23]]},"reference":[{"key":"S0022481217000846_ref3","volume-title":"Multisets in Type Theory","author":"Gylterud","year":"2016"},{"key":"S0022481217000846_ref2","unstructured":"[2] Aczel P. and Gambino N. , The generalised type-theoretic interpretation of constructive set theory, this JOURNAL, vol. 71 (2006), no. 1, pp. 67\u2013103."},{"key":"S0022481217000846_ref5","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0022481217000846_ref4","volume-title":"Intuitionistic Type Theory","volume":"vol. 1","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0022481217000846_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71989-X"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481217000846","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T21:11:07Z","timestamp":1555189867000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481217000846\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":5,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["S0022481217000846"],"URL":"https:\/\/doi.org\/10.1017\/jsl.2017.84","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}