[Alta-Logic] Peripatetic Seminar Monday 13:30 in MS 427

[Matthew Burke]

This week the peripatetic seminar will be at its normal time and
location.

Speaker: Matthew Burke

Title: Using Postulated Colimits in Coq

Abstract: In this talk we define and construct finite colimits in the
Coq proof assistant in a context that is similar to the category of
sets. First we review without proof the key mathematical ideas involved
in the theory of postulated colimits as described in a note of Anders
Kock. This theory gives us a way to prove results about colimits in an
arbitrary sheaf topos. Then we give an inductive definition in Coq of
the fundamental notion of zigzag in this theory. We finish by proving
the result analogous to the (mathematically easy) result that in the
category of sets pushouts of monomorphisms are monomorphisms.