Monthly Archives: January 2016

Colimits in HoTT

Posted on 8 January 2016 by Simon Boulier

In this post, I would want to present you two things: the small library about colimits that I formalized in Coq, a construction of the image of a function as a colimit, which is essentially a sliced version of the … Continue reading →

Posted in Code, Higher Inductive Types | 14 Comments