{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:20Z","timestamp":1761611240976},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4842,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,12]]},"abstract":"<jats:p>Lambek used categories with indeterminates to capture explicit variables in simply typed \u03bb-calculus. He observed that such categories with indeterminates can be described as Kleisli categories for suitable comonads. They account for \u2018functional completeness\u2019 for Cartesian (closed) categories.<\/jats:p><jats:p>Here we refine this analysis, by distinguishing \u2018contextual\u2019 and \u2018functional\u2019 completeness, and extend it to polymorphic \u03bb-calculi. Since the latter are described as certain fibrations, we are lead to consider indeterminates, not only for ordinary categories, but also for fibred categories. Following a 2-categorical generalisation of Lambek's approach, such fibrations with indeterminates are presented as 'simple slices' in suitable 2-categories of fibrations; more precisely, as Kleisli objects. It allows us to establish contextual and functional completeness results for some polymorphic calculi.<\/jats:p>","DOI":"10.1017\/s0960129500001213","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:09Z","timestamp":1236157209000},"page":"501-531","source":"Crossref","is-referenced-by-count":11,"title":["Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi"],"prefix":"10.1017","volume":"5","author":[{"given":"Claudio","family":"Hermida","sequence":"first","affiliation":[]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500001213_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129500001213_ref014","volume-title":"Introduction to higher-order categorical logic","author":"Lambek","year":"1986"},{"key":"S0960129500001213_ref011","unstructured":"Jacobs B. and Streicher T. (1993) A categorical view of equality in type theory, Technical Report 820, Department of Mathematics, University of Utrecht."},{"key":"S0960129500001213_ref009","doi-asserted-by":"crossref","unstructured":"Jacobs B. (1993a) Comprehension categories and the semantics of type dependency. Theoretical Computer Science.","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"S0960129500001213_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0063101"},{"key":"S0960129500001213_ref008","unstructured":"Jacobs B. (1991) Categorical Type Theory, PhD. Thesis, University of Nijmgen."},{"key":"S0960129500001213_ref006","doi-asserted-by":"crossref","unstructured":"Hermida C. (1993) Fibrations, logical predicates and indeterminates, PhD. Thesis, University of Edinburgh. (Technical Report ECS-LFCS-93\u2013277; also available as Aarhus University DAIMI Technical Report PB-462.)","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"S0960129500001213_ref005","volume-title":"Decomposing typed lambda calculus into a couple of categorical programming languages","author":"Hasegawa","year":"1994"},{"key":"S0960129500001213_ref012","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700002781"},{"key":"S0960129500001213_ref004","unstructured":"Fourman M. and Phoa W. (1992) A proposed categorical semantics for Pure ML. In: Proceedings ICALP 92."},{"key":"S0960129500001213_ref002","unstructured":"Burstall R. and McKinna J. (1992) Deliverables: a categorical approach to program development in type theory, Technical Report ECS-LFCS-92\u2013242, Department of Computer Science, Edinburgh University."},{"key":"S0960129500001213_ref003","volume-title":"A 2-categorical approach to change of base and geometric morphisms","author":"Carboni","year":"1990"},{"key":"S0960129500001213_ref016","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093634727"},{"key":"S0960129500001213_ref007","unstructured":"Hermida C. and Jacobs B. (1994) An algebraic view of structural induction. In: CSL'94. (Extended version in preparation)"},{"key":"S0960129500001213_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"},{"key":"S0960129500001213_ref010","unstructured":"Jacobs B. (1993b) Parameters and parametrization in specification, Technical Report 786, Department of Mathematics, University of Utrecht."},{"key":"S0960129500001213_ref001","volume-title":"The Lambda Calculus: its syntax and semantics","author":"Barendregt","year":"1984"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500001213","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T20:12:51Z","timestamp":1557778371000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500001213\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["S0960129500001213"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500001213","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}