The Biequivalence of Locally Cartesian Closed Categories and Martin-L\"of Type Theories

TL;DR

This paper establishes a corrected categorical equivalence between locally cartesian closed categories and Martin-L"of type theories with Pi, Sigma, and extensional identity types, using categories with families for technical clarity.

Contribution

It provides a corrected proof of the biequivalence between locally cartesian closed categories and Martin-L"of type theories, addressing previous assumptions and extending to categories without Pi-types.

Findings

Biequivalence between locally cartesian closed categories and Martin-L"of type theories.

Categories with families are effective for technical development.

Equivalence extends to left exact categories without Pi-types.

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.