Tripos theory
From MaRDI portal
Publication:3897050
DOI10.1017/S0305004100057534zbMath0451.03027OpenAlexW4243933121MaRDI QIDQ3897050
J. M. E. Hyland, Andrew M. Pitts, Peter T. Johnstone
Publication date: 1980
Published in: Mathematical Proceedings of the Cambridge Philosophical Society (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0305004100057534
triposhyperdoctrinerealizability toposestopos of P-valued setstopos-representing indexed pre-ordered set
Categorical logic, topoi (03G30) Topoi (18B25) Fibered categories (18D30) Other algebras related to logic (03G25) Preorders, orders, domains and lattices (viewed as categories) (18B35) Computability and recursion theory (03D99)
Related Items (57)
Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness ⋮ AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS ⋮ The effects of effects on constructivism ⋮ Limiting partial combinatory algebras ⋮ Computational adequacy for recursive types in models of intuitionistic set theory ⋮ Extensional realizability ⋮ Dialectica logical principles ⋮ Kleene computable functionals and the higher order existence property ⋮ On a generalization of equilogical spaces ⋮ A small complete category ⋮ Colimit completions and the effective topos ⋮ A topos for continuous logic ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Triposes as a generalization of localic geometric morphisms ⋮ Partial hyperdoctrines: categorical models for partial function logic and Hoare logic ⋮ Relating first-order set theories, toposes and categories of classes ⋮ Dictoses ⋮ Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator ⋮ Functoriality of modified realizability ⋮ Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory ⋮ Fibrations and recursivity ⋮ Sheaves of structures, Heyting‐valued structures, and a generalization of Łoś's theorem ⋮ Dialectica principles via Gödel doctrines ⋮ An exper model for Quest ⋮ The category of implicative algebras and realizability ⋮ A characterization of generalized existential completions ⋮ On categorical structures arising from implicative algebras: from topology to assemblies ⋮ Nonstandard proof methods in toposes ⋮ What should a generic object be? ⋮ Categorical semantics for higher order polymorphic lambda calculus ⋮ Ordered combinatory algebras and realizability ⋮ Categories of partial equivalence relations as localizations ⋮ Characterizing partitioned assemblies and realizability toposes ⋮ Two remarks on the Lifschitz realizability topos ⋮ Realizability in ordered combinatory algebras with adjunction ⋮ Triposes, q-toposes and toposes ⋮ Frame-fuzzy points and membership ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Regular functors and relative realisability categories ⋮ The category of equilogical spaces and the effective topos as homotopical quotients ⋮ Classical realizability in the CPS target language ⋮ The modified realizability topos ⋮ On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes ⋮ A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ A co-free construction for elementary doctrines ⋮ Unifying exact completions ⋮ The existential completion ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Equilogical spaces ⋮ Differential equations in constructive analysis and in the recursive realizability topos ⋮ Relative and modified relative realizability ⋮ An application of open maps to categorical logic ⋮ Aspects of Categorical Recursion Theory ⋮ FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION ⋮ Models of intuitionistic set theory in subtoposes of nested realizability toposes ⋮ A characterization of the left exact categories whose exact completions are toposes
Cites Work
This page was built for publication: Tripos theory
