mathlib documentation

category_theory.limits.preserves.shapes.pullbacks

Preserving pullbacks #

Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete pullback cones.

In particular, we show that pullback_comparison G f g is an isomorphism iff G preserves the pullback of f and g.

TODO #