mathlib documentation


Preserving terminal object #

Constructions to relate the notions of preserving terminal objects and reflecting terminal objects to concrete objects.

In particular, we show that terminal_comparison G is an isomorphism iff G preserves terminal objects.

If C has a terminal object and G preserves terminal objects, then D has a terminal object also. Note this property is somewhat unique to (co)limits of the empty diagram: for general J, if C has limits of shape J and G preserves them, then D does not necessarily have limits of shape J.