{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:17:23Z","timestamp":1770283043923,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Presheaf models of dependent type theory have been successfully applied to\nmodel HoTT, parametricity, and directed, guarded and nominal type theory. There\nhas been considerable interest in internalizing aspects of these presheaf\nmodels, either to make the resulting language more expressive, or in order to\ncarry out further reasoning internally, allowing greater abstraction and\nsometimes automated verification. While the constructions of presheaf models\nlargely follow a common pattern, approaches towards internalization do not.\nThroughout the literature, various internal presheaf operators ($\\surd$,\n$\\Phi\/\\mathsf{extent}$, $\\Psi\/\\mathsf{Gel}$, $\\mathsf{Glue}$, $\\mathsf{Weld}$,\n$\\mathsf{mill}$, the strictness axiom and locally fresh names) can be found and\nlittle is known about their relative expressivenes. Moreover, some of these\nrequire that variables whose type is a shape (representable presheaf, e.g. an\ninterval) be used affinely. We propose a novel type former, the transpension\ntype, which is right adjoint to universal quantification over a shape. Its\nstructure resembles a dependent version of the suspension type in HoTT. We give\ngeneral typing rules and a presheaf semantics in terms of base category\nfunctors dubbed multipliers. Structural rules for shape variables and certain\naspects of the transpension type depend on characteristics of the multiplier.\nWe demonstrate how the transpension type and the strictness axiom can be\ncombined to implement all and improve some of the aforementioned\ninternalization operators (without formal claim in the case of locally fresh\nnames).<\/jats:p>","DOI":"10.46298\/lmcs-20(2:16)2024","type":"journal-article","created":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T11:30:06Z","timestamp":1718796606000},"source":"Crossref","is-referenced-by-count":1,"title":["Transpension: The Right Adjoint to the Pi-type"],"prefix":"10.46298","volume":"Volume 20, Issue 2","author":[{"given":"Andreas","family":"Nuyts","sequence":"first","affiliation":[]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,6,19]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13798\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13798\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T11:30:06Z","timestamp":1718796606000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6725"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,19]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(2:16)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2008.08533v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2008.08533v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2008.08533v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2008.08533","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2008.08533","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,19]]},"article-number":"6725"}}