The Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theories

摘要

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-L6f type theories with 77, ∑, 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 Benabou-Hofmann interpretation of Martin-Loef 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-Loef type theories. As a second result we prove that if we remove 77-types the resulting categories with families are biequivalent to left exact categories.