We define a category walking_cospan (resp. walking_span), which is the index category for the given data for a pullback (resp. pushout) diagram. Convenience methods cospan f g and span f g construct functors from the walking (co)span, hitting the given morphisms.
We define pullback f g and pushout f g as limits and colimits of such functors.
Typeclasses has_pullbacks and has_pushouts assert the existence of (co)limits shaped as walking (co)spans.
The type of objects for the diagram indexing a pullback.
The type of objects for the diagram indexing a pushout.
The arrows in a pullback diagram.
The walking_cospan is the index diagram for a pullback.
The arrows in a pushout diagram.
The walking_span is the index diagram for a pushout.
cospan f g is the functor from the walking cospan hitting f and g.
span f g is the functor from the walking span hitting f and g.
pullback f g computes the pullback of a pair of morphisms with the same target.
pushout f g computes the pushout of a pair of morphisms with the same source.