{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T03:21:23Z","timestamp":1768706483674,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T00:00:00Z","timestamp":1683158400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We investigate predicative aspects of constructive univalent foundations. By\npredicative and constructive, we respectively mean that we do not assume\nVoevodsky's propositional resizing axioms or excluded middle. Our work\ncomplements existing work on predicative mathematics by exploring what cannot\nbe done predicatively in univalent foundations. Our first main result is that\nnontrivial (directed or bounded) complete posets are necessarily large. That\nis, if such a nontrivial poset is small, then weak propositional resizing\nholds. It is possible to derive full propositional resizing if we strengthen\nnontriviality to positivity. The distinction between nontriviality and\npositivity is analogous to the distinction between nonemptiness and\ninhabitedness. Moreover, we prove that locally small, nontrivial (directed or\nbounded) complete posets necessarily lack decidable equality. We prove our\nresults for a general class of posets, which includes e.g. directed complete\nposets, bounded complete posets, sup-lattices and frames. Secondly, the fact\nthat these nontrivial posets are necessarily large has the important\nconsequence that Tarski's theorem (and similar results) cannot be applied in\nnontrivial instances. Furthermore, we explain that generalizations of Tarski's\ntheorem that allow for large structures are provably false by showing that the\nordinal of ordinals in a univalent universe has small suprema in the presence\nof set quotients. The latter also leads us to investigate the\ninter-definability and interaction of type universes of propositional\ntruncations and set quotients, as well as a set replacement principle. Thirdly,\nwe clarify, in our predicative setting, the relation between the traditional\ndefinition of sup-lattice that requires suprema for all subsets and our\ndefinition that asks for suprema of all small families.<\/jats:p>","DOI":"10.46298\/lmcs-19(2:8)2023","type":"journal-article","created":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T11:20:24Z","timestamp":1683199224000},"source":"Crossref","is-referenced-by-count":2,"title":["On Small Types in Univalent Foundations"],"prefix":"10.46298","volume":"Volume 19, Issue 2","author":[{"given":"Tom","family":"de Jong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mart\u00edn H\u00f6tzel","family":"Escard\u00f3","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2023,5,4]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/lmcs.episciences.org\/11270\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/lmcs.episciences.org\/11270\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:30Z","timestamp":1687292430000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/lmcs.episciences.org\/8643"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,4]]},"references-count":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.46298\/lmcs-19(2:8)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2111.00482v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2111.00482v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2111.00482v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2111.00482","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2111.00482","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,4]]},"article-number":"8643"}}