Some free constructions in realizability and proof theory
From MaRDI portal
Publication:1903677
DOI10.1016/0022-4049(94)00103-PzbMath0839.18002MaRDI QIDQ1903677
Publication date: 19 June 1996
Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)
polymorphismregular categoryexact completioneffective toposfull reflective subcategorystack completionfree colimit constructionlex categorystable factorization systems
Related Items
Relative completions, Extensional realizability, The symmetric topos, Decidable (= separable) objects and morphisms in lextensive categories, Regular and exact completions, Quotient completion for the foundation of constructive mathematics, Cocomplete toposes whose exact completions are toposes, Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator, A characterization of generalized existential completions, On categorical structures arising from implicative algebras: from topology to assemblies, Pre-rigid monoidal categories, Lex colimits, On stability of exactness properties under the pro-completion, Elementary doctrines as coalgebras, Unnamed Item, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, Regular functors and relative realisability categories, The category of equilogical spaces and the effective topos as homotopical quotients, Exact completion of path categories and algebraic set theory. I: Exact completion of path categories, A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS, Aspects of predicative algebraic set theory. I: Exact completion, Splitting idempotents in a fibered setting, Sobriety for equilogical spaces, Category theoretic structure of setoids, Unifying exact completions, Aspects of predicative algebraic set theory. II: Realizability, Läuchli's completeness theorem from a topos-theoretic perspective, Setoids and universes, W-types in homotopy type theory, When do completion processes give rise to extensive categories?, Inductive types and exact completion, On algebraically exact categories and essential localizations of varieties, The existential completion, The Herbrand topos, The Herbrand topos, A characterisation of the category of compact Hausdorff spaces, Three extensional models of type theory, On generalized equilogical spaces, Lawvere–Tierney sheaves in Algebraic Set Theory, A minimalist two-level foundation for constructive mathematics, Locally cartesian closed exact completions, Weak subobjects and the epi-monic completion of a category., A factorization of regularity, An extension of the regular completion, Completions, comonoids, and topological spaces, Aspects of Categorical Recursion Theory, The effective model structure and -groupoid objects, A characterization of the left exact categories whose exact completions are toposes, More exact completions that are toposes
Cites Work
