Erik Palmgren: Categories with Families and FOLDS: functorial semantics vs standard semantics

Every dependent first-order signature \(\Sigma\) generates a free category with families \(\mathcal{F}_ \Sigma\). A model \(\mathcal{C} \) of the \(\Sigma\)-signature is a cwf morphism M from \(\mathcal{F}_\Sigma\)  to C. Such a morphism is uniquely determined by its values on the signature. We show that such morphisms can constructed by incrementally by induction on the signature. This shows that this functorial notion of model extends the usual non-dependent version of model of first-order signature.