CatGloss

A diagram is said to be finite if its indexing category contains only finitely many morphisms. Lemmas \ref{lem:prod-as-pullback} and \ref{lem:equalizer-as-pullback} prove: