The Discrete Objects in the Effective Topos
From MaRDI portal
Publication:3481914
DOI10.1112/plms/s3-60.1.1zbMath0703.18002OpenAlexW2094410575MaRDI QIDQ3481914
Edmund P. Robinson, J. M. E. Hyland, Giuseppe Rosolini
Publication date: 1990
Published in: Proceedings of the London Mathematical Society (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1112/plms/s3-60.1.1
equivalencecompletenesspolymorphisminternal categoriesfibered category of families of discrete objects in the recursion theoretic effective toposfibered category of modest setssmall complete category
Categorical logic, topoi (03G30) Topoi (18B25) Fibered categories (18D30) Computability and recursion theory (03D99)
Related Items
Non-deterministic effects in a realizability model, Axiomatizing higher-order Kleene realizability, Profunctors in Mal'tsev categories and fractions of functors, Parametricity as isomorphism, On completeness and cocompleteness in and around small categories, Some free constructions in realizability and proof theory, A small complete category, Constructive natural deduction and its ‘ω-set’ interpretation, An application of descent to a classification theorem for toposes, The Girard-Reynolds isomorphism (second edition), Dictoses, Internal enriched categories, A note on ``Extensional PERs, An exper model for Quest, On the failure of fixed-point theorems for chain-complete lattices in the effective topos, What should a generic object be?, A modest model of records, inheritance, and bounded quantification, Denotational semantics for guarded dependent type theory, The category of equilogical spaces and the effective topos as homotopical quotients, Univalent polymorphism, Sobriety for equilogical spaces, Aspects of predicative algebraic set theory. II: Realizability, A proposed categorical semantics for Pure ML, On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos, Unnamed Item, Extensional models for polymorphism, Functorial polymorphism, The Dedekind reals in abstract Stone duality, From term models to domains, Unnamed Item, Equilogical spaces, Axioms and (counter)examples in synthetic domain theory, A Convenient Category of Domains, Relational Parametricity for Control Considered as a Computational Effect, Formal parametric polymorphism, Fixpoint operators for domain equations