CatDat

Implication Details

Assumptions: binary productsequalizers

Conclusions: pullbacks

Reason: The pullback of f:XSf : X \to S and g:YSg : Y \to S is the equalizer of p1f,p2g:X×YSp_1 \circ f, \, p_2 \circ g : X \times Y \rightrightarrows S.