The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
From MaRDI portal
Publication:5740406
Abstract: Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B'enabou-Hofmann interpretation of Martin-L"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.
Recommendations
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- Locally cartesian closed categories and type theory
- Categories with families: unityped, simply typed, and dependently typed
- Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
- The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
Cites work
- Fibered categories and the foundations of naive category theory
- Generalized algebraic theories and contextual categories
- scientific article; zbMATH DE number 1289305 (Why is no real title available?)
- scientific article; zbMATH DE number 3335935 (Why is no real title available?)
- Locally cartesian closed categories and type theory
Cited in
(25)- Categories with families and first-order logic with dependent sorts
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- Locally Cartesian closed quasi-categories from type theory
- scientific article; zbMATH DE number 436447 (Why is no real title available?)
- scientific article; zbMATH DE number 25966 (Why is no real title available?)
- scientific article; zbMATH DE number 6816943 (Why is no real title available?)
- Categories with families: unityped, simply typed, and dependently typed
- Bicategories in univalent foundations
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- On generalized algebraic theories and categories with families
- Bicategories in univalent foundations
- Pointers in Recursion: Exploring the Tropics
- A cubical language for Bishop sets
- Multimodal dependent type theory
- Modal dependent type theory and dependent right adjoints
- A general framework for the semantics of type theory
- Towards a constructive simplicial model of Univalent Foundations
- Game semantics of Martin-Löf type theory
- A 2-categorical analysis of context comprehension
- Monoidal closure of Grothendieck constructions via -tractable monoidal structures and Dialectica formulas
- -type theories
- Controlling unfolding in type theory
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
This page was built for publication: The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740406)
