Intuitionist type theory and the free topos

DOI10.1016/0022-4049(80)90102-4zbMath0452.03049OpenAlexW2036138623MaRDI QIDQ1148318

Philip J. Scott, Joachim Lambek

Publication date: 1980

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

Full work available at URL: https://doi.org/10.1016/0022-4049(80)90102-4

zbMATH Keywords

free toposintuitionist type theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Intuitionistic mathematics (03F55) Foundations, relations to logic and deductive systems (18A15)

Related Items

Equational classes of toposes, Constructive natural deduction and its ‘ω-set’ interpretation, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, On fixpoint objects and gluing constructions, Meeting of the Association for Symbolic Ldgic, Washington, DC, 1985, Choice and independence of premise rules in intuitionistic set theory, Intuitionist type theory and foundations, Unnamed Item, Quotients of decidable objects in a topos, Internal coproduct of abelian groups in an elementary topos, Abelian groups in a topos: injectives and injective effacements, Aspects of Categorical Recursion Theory

Cites Work

• Contribution to the study of the natural number object in elementary topoi
• From types to sets
• Intuitionist type theory and foundations
• Model theory and topoi. A collection of lectures by various authors
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Functional completeness of cartesian categories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item