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.