The Coq mailing list

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

This sounds awesome. I'll start reading that as first thing. Thanks.

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


2014/1/14 Daniel Schepler 
<dschepler AT gmail.com>:
> A while ago I posted the beginnings of a tutorial of Coq for mathematics, at
> http://people.debian.org/~schepler/coqtut.pdf or
> http://people.debian.org/~schepler/coqtut.v.html .  I didn't get very far on
> the project, but it should hopefully be a gentle introduction to the general
> flow of how you do proofs in Coq.  Then from there you could start looking
> at use of typeclasses for encoding algebraic varieties which is what I'd
> recommend.  (For the latter, "Typeclasses for Mathematics" I think is the
> title of a good introduction for how that would work.)
> --
> Daniel Schepler
>
>
> On Tue, Jan 14, 2014 at 12:29 PM, Ömer Sinan Ağacan 
> <omeragacan AT gmail.com>
> wrote:
>>
>> 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.
>> >
>> >
>
>