  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.

Logic in Computer Science