Monthly Archives: January 2016
Colimits in HoTT
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
Homotopy Type Theory 