{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T10:22:16Z","timestamp":1753438936056},"reference-count":7,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,6]]},"abstract":"<jats:p>This paper presents a dependently-typed construction of semi-simplicial sets in a type theory where sets are taken to be types. This addresses an open question raised on the wiki of the special year on Univalent Foundations at the Institute of Advanced Study (2012\u20132013).<\/jats:p>","DOI":"10.1017\/s0960129514000528","type":"journal-article","created":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T14:44:22Z","timestamp":1416494662000},"page":"1116-1131","source":"Crossref","is-referenced-by-count":4,"title":["A dependently-typed construction of semi-simplicial types"],"prefix":"10.1017","volume":"25","author":[{"given":"HUGO","family":"HERBELIN","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,20]]},"reference":[{"key":"S0960129514000528_ref6","unstructured":"Voevodsky V. (2012a) Semi-simplicial types. Available at http:\/\/uf-ias-2012.wikispaces.com\/Semi-simplicial+types."},{"key":"S0960129514000528_ref2","doi-asserted-by":"publisher","DOI":"10.1216\/RMJ-2012-42-2-353"},{"key":"S0960129514000528_ref3","unstructured":"LeFanu Lumsdaine P. (2012) Semi-simplicial types. Available at: http:\/\/uf-ias-2012.wikispaces.com\/Semi-simplicial+types."},{"key":"S0960129514000528_ref1","unstructured":"Coq Development Team, T. (2012) The Coq Reference Manual, version 8.4. Available at http:\/\/coq.inria.fr\/doc."},{"key":"S0960129514000528_ref4","unstructured":"The Univalent Foundations Program, Institute of Advanced Study. (2013) Homotopy Type theory: Univalent Foundations of Mathematics. Available at http:\/\/homotopytypetheory.org\/book."},{"key":"S0960129514000528_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20920-8_4"},{"key":"S0960129514000528_ref7","unstructured":"Voevodsky V. (2012b) Univalent foundations repository. Ongoing Coq development. Available at https:\/\/github.com\/vladimirias\/Foundations."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000528","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T23:52:55Z","timestamp":1555804375000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000528\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,20]]},"references-count":7,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000528"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000528","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,20]]}}}