{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T02:39:34Z","timestamp":1768703974660,"version":"3.49.0"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,4,27]],"date-time":"2017-04-27T00:00:00Z","timestamp":1493251200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study idempotents in intensional Martin-L\\\"of type theory, and in\nparticular the question of when and whether they split. We show that in the\npresence of propositional truncation and Voevodsky's univalence axiom, there\nexist idempotents that do not split; thus in plain MLTT not all idempotents can\nbe proven to split. On the other hand, assuming only function extensionality,\nan idempotent can be split if and only if its witness of idempotency satisfies\none extra coherence condition. Both proofs are inspired by parallel results of\nLurie in higher category theory, showing that ideas from higher category theory\nand homotopy theory can have applications even in ordinary MLTT.\n  Finally, we show that although the witness of idempotency can be recovered\nfrom a splitting, the one extra coherence condition cannot in general; and we\nconstruct \"the type of fully coherent idempotents\", by splitting an idempotent\non the type of partially coherent ones. Our results have been formally verified\nin the proof assistant Coq.<\/jats:p>","DOI":"10.2168\/lmcs-12(3:9)2016","type":"journal-article","created":{"date-parts":[[2017,8,10]],"date-time":"2017-08-10T10:03:42Z","timestamp":1502359422000},"source":"Crossref","is-referenced-by-count":2,"title":["Idempotents in intensional type theory"],"prefix":"10.46298","volume":"Volume 12, Issue 3","author":[{"given":"Michael","family":"Shulman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2017,4,27]]},"reference":[{"key":"1183:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2027\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2027\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:09:05Z","timestamp":1681243745000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,27]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-12(3:9)2016","relation":{"is-same-as":[{"id-type":"arxiv","id":"1507.03634","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1507.03634","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,27]]},"article-number":"2027"}}