The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Jan 14, 2014, at 3:18 PM, Daniil Frumin wrote:

> Hi,
> 
> There are many examples of proof of the specific theorems/properties
> on the internet: everything from blogposts to Coq contributions that
> Harley has linked.
> 
> However, there are also bigger projects, like Math Classes [1], which
> aim is to develop interfaces (based on Coq's typeclasses) for many
> algebraic gadgets.
> 
> Recently, Vladimir Voevodsky has published his paper [2] on his work
> in the formalization of mathematics. I haven't read it yet, but I
> guess it deals with Univalence, HoTT and other things I am clueless
> about.
> 
> I myself tried to formalize basic category theory [3] and I've got to
> say it is going slower than I want and it is harder than I initially
> anticipated.
> 
> [1] http://math-classes.org
> [2] http://arxiv.org/abs/1401.0053
> [2] http://repos.covariant.me/browse?r=cat;a=tree


There is a conceptually correct formalization of the basics of basic category 
theory here:

https://github.com/benediktahrens/rezk_completion

with the accompanying paper here:

http://arxiv.org/abs/1303.0584


Vladimir.