The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The basic category theory does not depend much on HoTT nor univalence; the two main dependencies are that you add an extra requirement saying "forall x y (f g : Hom x y) (pf1 pf2 : f = g), pf1 = pf2", and that there is a new notion of a saturated or univalent category (alternatively, you can call classical categories unsaturated or precategories, and call precategory + univalence a category), but you don't need to use that.  There's a decent amount of basic category theory developed at https://github.com/HoTT/HoTT/tree/master/theories/categories (on top of the other HoTT library), and there's an earlier version of it at https://bitbucket.org/JasonGross/catdb/src which doesn't depend on HoTT nor on a patched version of Coq.  (The library Vladimir mentioned requires manually patching Coq, the HoTT/HoTT library requires a dev version of Coq, available at https://github.com/HoTT/coq, but should compile with Coq 8.5 when it comes out, and the earlier version that I just mentioned should compile with vanilla 8.4.)

-Jason
 

On Tue, Jan 14, 2014 at 3:39 PM, Daniil Frumin <difrumin AT gmail.com> wrote:

I saw that work, unfortunately it's beyond my understating at the
moment, as I am unfamiliar with HoTT/Univalence.
I'll make sure to read that paper once I learn type theory/HoTT properly.

On Wed, Jan 15, 2014 at 12:26 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:
>
> 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.
>
>

--
Sincerely yours,
-- Daniil