Finn Lawler product-absolute pullback (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

In category with finite products, the following squares must be pullbacks, for any morphisms $f,g$:

as must the naturality square for the symmetry $\sigma \colon X \times Y \cong Y \times X$ , the product on one side or the other with an identity morphism of a pullback square, square and (which the pasting of two pullback squares side by side. These pullbacks must be preserved by any product-preserving functor, so we will call themtype D), and the pasting of two pullback squares side by side. These pullbacks must be preserved by any product-preserving functor, so we call them product-absolute.

This fact was already noted for squares of types (A) A and (C) C byLawvere; the others are given by Seely. See also Todd Trimble’s exposition, noting in particular that the squares expressing coassociativity of diagonal maps $d \colon X \to X \times X$ are product-absolute pullbacks, which we call type E.