Van Kampen Colimits as Bicolimits in Span

The exactness properties of coproducts in extensive categories and pushouts along monos in adhesive categories have found various applications in theoretical computer science, e.g. in program semantics, data type theory and rewriting. We show that these properties can be understood as a single universal property in the associated bicategory of spans. To this end, we first provide a general notion of Van Kampen cocone that specialises to the above colimits. The main result states that Van Kampen cocones can be characterised as exactly those diagrams in C that induce bicolimit diagrams in the bicategory of spans SpanC, provided that C has pullbacks and enough colimits.

• Type: Conference
• Year: 2009
• Where: CALCO
• Authors: Tobias Heindel, Pawel Sobocinski
• Keywords: CALCO 2009, Data Type Theory, Mathematics, Single Universal Property, Van Kampen Cocones