The biequivalence of locally cartesian closed categories and Martin-Loef type theories

摘要

Seely’s paper Locally cartesian closed categories and type theory (Seely 1984) contains arnwell-known result in categorical type theory: that the category of locally cartesian closedrncategories is equivalent to the category of Martin-Loef type theories with Π,Σ andrnextensional identity types. However, Seely’s proof relies on the problematic assumption thatrnsubstitution in types can be interpreted by pullbacks. Here we prove a corrected version ofrnSeely’s theorem: that the Benabou–Hofmann interpretation of Martin-Loef type theory inrnlocally cartesian closed categories yields a biequivalence of 2-categories. To facilitate therntechnical development, we employ categories with families as a substitute for syntacticrnMartin-Loef type theories. As a second result, we prove that if we remove Π-types, thernresulting categories with families with only Σ and extensional identity types are biequivalentrnto left exact categories.