Abstract
We show how the categorical logic of untyped, simply typed and
dependently typed lambda calculus can be structured around the notion of
category with family (cwf). To this end we introduce subcategories of simply
typed cwfs (scwfs), where types do not depend on variables, and unityped
cwfs (ucwfs), where there is only one type. We prove several equivalence and
biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with
finite products and limits, cartesian closed categories, and locally cartesian
closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault
and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others
are biequivalences between notions where properties are only preserved up to
isomorphism. In addition to this we discuss various constructions of initial
ucwfs, scwfs, and cwfs with extra structure.