The Discrete Objects in the Effective Topos

DOI10.1112/PLMS/S3-60.1.1MaRDI QIDQ3481914zbMATH OpenOpenAlexFDO

Authors Martin Hyland, Edmund P. Robinson, 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

zbMATH Keywords

completenessequivalencefibered category of families of discrete objects in the recursion theoretic effective toposfibered category of modest setsinternal categoriespolymorphismsmall complete category

Mathematics Subject Classification ID

Computability and recursion theory (03D99) Categorical logic, topoi (03G30) Topoi (18B25) Fibered categories (18D30)

Recommendations

• ABOUT MODEST SETS
• Colimit completions and the effective topos
• Some free constructions in realizability and proof theory
• Partial morphisms in categories of effective objects
• A small complete category

Cited in

(46)

• A small complete category
• Formal parametric polymorphism
• Axiomatizing higher-order Kleene realizability
• Parametricity as isomorphism
• Axioms and (counter)examples in synthetic domain theory
• Fixpoint operators for domain equations
• Equilogical spaces
• On completeness and cocompleteness in and around small categories
• Some free constructions in realizability and proof theory
• Univalent polymorphism
• Non-deterministic effects in a realizability model
• Sobriety for equilogical spaces
• Profunctors in Mal'tsev categories and fractions of functors
• Internal enriched categories
• The definitions of middle object and weak topos
• On the failure of fixed-point theorems for chain-complete lattices in the effective topos
• A convenient category of domains
• ABOUT MODEST SETS
• The Dedekind reals in abstract Stone duality
• An application of descent to a classification theorem for toposes
• scientific article; zbMATH DE number 4154448 (Why is no real title available?)
• Fixpoint objects need not be -discrete
• scientific article; zbMATH DE number 4047722 (Why is no real title available?)
• Basic subtoposes of the effective topos
• Constructive natural deduction and its ‘ω-set’ interpretation
• On the failure of fixed-point theorems for chain-complete lattices in the effective topos
• The category of equilogical spaces and the effective topos as homotopical quotients
• From term models to domains
• Dictoses
• The Sierpinski object in the Scott realizability topos
• Denotational semantics for guarded dependent type theory
• A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
• A proposed categorical semantics for pure ML
• Relational parametricity for control considered as a computational effect
• Aspects of predicative algebraic set theory. II: Realizability
• An exper model for Quest
• A note on ``Extensional PERs
• What should a generic object be?
• Towards univalent reference types: the impact of univalence on denotational semantics
• Toward the effective 2-topos
• Strict universes for Grothendieck topoi
• Extensional models for polymorphism
• Functorial polymorphism
• Filtered colimits in the effective topos
• The Girard-Reynolds isomorphism (second edition)
• A modest model of records, inheritance, and bounded quantification

This page was built for publication: The Discrete Objects in the Effective Topos

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3481914)