The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Wow, thanks all for your answers. This amount of code should keep me
busy for a while. I hope I can understand the Coq used in these
implementations.

---
Ömer Sinan Ağacan
http://osa1.net


2014/1/14 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.
>
>