The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories

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öf 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énabou-Hofmann interpretation of Martin-Löf 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öf 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.

arXiv commentTLCA 2011 - 10th Typed Lambda Calculi and Applications, Novi Sad : Serbia (2011)

Cited by in corpus (9)

• A General Framework for the Semantics of Type Theory
• Modal Dependent Type Theory and Dependent Right Adjoints
• Towards a constructive simplicial model of Univalent Foundations
• Large and Infinitary Quotient Inductive-Inductive Types
• A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
• Bicategories in Univalent Foundations
• Categories with families and first-order logic with dependent sorts
• Comparing semantic frameworks for dependently-sorted algebraic theories
• Controlling unfolding in type theory