A small complete category

DOI10.1016/0168-0072(88)90018-8zbMath0659.18007OpenAlexW2086061699MaRDI QIDQ1112159

Publication date: 1988

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(88)90018-8

zbMATH Keywords

polymorphic lambda calculus completeness category of modest sets models for strong type theories small full subcategory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Other constructive mathematics (03F65) Combinatory logic and lambda calculus (03B40)

Related Items

Typed equivalence, type assignment, and type containment, Non-deterministic effects in a realizability model, Axiomatizing higher-order Kleene realizability, The S-replete construction, The convex powerdomain in a category of posets realized by cpos, A proposed categorical semantics for ML modules, Parametricity as isomorphism, On completeness and cocompleteness in and around small categories, Least fixpoints of endofunctors of cartesian closed categories, Building domains from graph models, Logical systems. I: Internal calculi., A higher-order calculus and theory abstraction, Categorifying Computations into Components via Arrows as Profunctors, Categorical data types in parametric polymorphism, Semantics of the second order lambda calculus, Constructive sets in computable sets, European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988, Internal enriched categories, A note on ``Extensional PERs, What should a generic object be?, A category-theoretic characterization of functional completeness, Two remarks on the Lifschitz realizability topos, A modest model of records, inheritance, and bounded quantification, Recursion over realizability structures, Bunched polymorphism, Mathesis Universalis and Homotopy Type Theory, Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic, The category of equilogical spaces and the effective topos as homotopical quotients, Univalent polymorphism, Categorical models of polymorphism, The extended calculus of constructions (ECC) with inductive types, Aspects of predicative algebraic set theory. II: Realizability, Realizability models and implicit complexity, Comprehension categories and the semantics of type dependency, Semantics of constructions. I: The traditional approach, A game semantics for generic polymorphism, Unnamed Item, Extensional models for polymorphism, Functorial polymorphism, Categorical semantics for arrows, From parametric polymorphism to models of polymorphic FPC, From constructivism to computer science, From term models to domains, Unnamed Item, Realizability models for BLL-like languages, A homotopy-theoretic model of function extensionality in the effective topos, The sequentially realizable functionals, A Convenient Category of Domains, Relational Parametricity for Control Considered as a Computational Effect, The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus

Cites Work