Locally cartesian closed categories and type theory
From MaRDI portal
Publication:3325725
DOI10.1017/S0305004100061284zbMath0539.03048OpenAlexW2022837260WikidataQ56172124 ScholiaQ56172124MaRDI QIDQ3325725
Publication date: 1984
Published in: Mathematical Proceedings of the Cambridge Philosophical Society (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0305004100061284
Categorical logic, topoi (03G30) Fibered categories (18D30) Proof theory and constructive mathematics (03F99)
Related Items (72)
Linear Dependent Type Theory for Quantum Programming Languages ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ Logic in Category Theory ⋮ Axiomatic reals and certified efficient exact real computation ⋮ Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions ⋮ A higher-order calculus and theory abstraction ⋮ Algebra of constructions. I. The word problem for partial algebras ⋮ A small complete category ⋮ An interpretation of dependent type theory in a model category of locally cartesian closed categories ⋮ On the semantics of the universal quantifier ⋮ Dependence and independence results for (impredicative) calculi of dependent types ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ The genesis of the groupoid model ⋮ A category-theoretic account of program modules ⋮ Martin-Löf complexes ⋮ Independence results for calculi of dependent types ⋮ Dictoses ⋮ A dialectica-like model of linear logic ⋮ The linear-non-linear substitution 2-monad ⋮ A formal logic for formal category theory ⋮ The Local Universes Model ⋮ A general framework for the semantics of type theory ⋮ Game semantics of Martin-Löf type theory ⋮ Totality in arena games ⋮ Categorical semantics for higher order polymorphic lambda calculus ⋮ Induction-recursion and initial algebras. ⋮ Unnamed Item ⋮ The essence of ornaments ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ A note on Russell's paradox in locally Cartesian closed categories ⋮ Composition of deductions within the propositions-as-types paradigm ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Polynomial functors and polynomial monads ⋮ A logical framework combining model and proof theory ⋮ Homotopy-Theoretic Models of Type Theory ⋮ The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories ⋮ Internal type theory ⋮ Unnamed Item ⋮ The identity type weak factorisation system ⋮ The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective ⋮ Revisiting the categorical interpretation of dependent type theory ⋮ Comprehension categories and the semantics of type dependency ⋮ A linear category of polynomial diagrams ⋮ The biequivalence of locally cartesian closed categories and Martin-Löf type theories ⋮ The proof monad ⋮ Unnamed Item ⋮ Homotopy theoretic models of identity types ⋮ Unnamed Item ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Three extensional models of type theory ⋮ A note on inconsistencies caused by fixpoints in a cartesian closed category ⋮ Categorical and algebraic aspects of Martin-Löf type theory ⋮ A category-theoretic account of program modules ⋮ Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types ⋮ Kripke Semantics for Martin-Löf’s Extensional Type Theory ⋮ Two-dimensional models of type theory ⋮ Unnamed Item ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Classifying categories for partial equational logic ⋮ Wellfounded trees in categories ⋮ Containers: Constructing strictly positive types ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories ⋮ Type Theory and Homotopy ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed ⋮ European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991 ⋮ A natural semantics of first-order type dependency ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
Cites Work
This page was built for publication: Locally cartesian closed categories and type theory
