Blakers-Messay in Agda

[Favonia]

We (Peter L Lumsdaine, Guillaume, Dan and I) have formalized the
Blakers-Messay theorem in Agda. The proof is unfortunately based on
the old Agda library and requires further porting. We also believe
some major simplification is possible.

Anyway, it's fully computer-checked!

Favonia

PS: This mail is sent to two mailing lists because I'm not sure which
one it should go to.

[Bas Spitters]

Nice!

Could you elaborate on the plans with the agda library?
Maybe it is possible to standardize a bit between the Coq and agda library ??

Bas

> --
> You received this message because you are subscribed to the Google Groups "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Guillaume Brunerie]

We're working on a new Agda library which will hopefully become a common library for everyone doing homotopy type theory in Agda. A very early version is already available on Github, branch 2.0 of HoTT/HoTT-Agda (but I won't be able to work much on it for the next two weeks).

I could be nice to standardize things with the Coq library. One issue is that we can use much more symbols in identifiers in Agda, so sometimes we can have shorter and nicer identifiers.
Also we're doing an experiment of using the notion of path over a path directly (without implementing it with a transport), so various things are quite different in the library.

Are you thinking of specific things to standardize?

Guillaume

[Peter LeFanu Lumsdaine]

It feels to me like everything is so experimental at the moment that the benefits of having two different explorations are probably greater than the benefits of consistency.

–p.

[Bas Spitters]

Maybe "standardize" sounds to burocratic. It was a general remark:
Maybe it is possible to learn a few lessons from the organization of
the Coq library.
Conversely, it would be nice to know which killer features from agda
should be ported to Coq.

[Andrej Bauer]

One lesson to be learned from the Coq library (at least the last time I looked at the Agda library) is to write comments that help people figure out what is going on ;-)

[Guillaume Brunerie]

I'll try to write more comments.

Guillaume

On Apr 29, 2013 3:58 AM, "Andrej Bauer" <andrej...@andrej.com> wrote:

One lesson to be learned from the Coq library (at least the last time I looked at the Agda library) is to write comments that help people figure out what is going on ;-)

[Erik Palmgren]

This position at our department may be of interest to some readers of this list. 
(For instance the geometry research in Sergei Merkulov's group has a quite 
category- and homotopy-theoretic flavour.)

Professor in Mathematics with focus on Geometry

Deadline for application: August 15, 2013.

The Department of Mathematics at Stockholm University with its excellent research record and long lasting traditions has acquired a very special place in Scandinavian mathematics. Professors and lecturers working at the department possess competence in different areas of mathematics ranging from algebra, geometry and analysis to mathematical logic and combinatorics. Geometry with its central role in mathematics has shaped the department’s profile and unites different research groups. We are looking for a mathematician with outstanding research record working in geometry in a broad sense.


http://www.su.se/english/about/vacancies/lecturers-researchers/professor-in-mathematics-with-focus-on-geometry-1.123282

http://eims.ams.org/jobs#/detail/5254388/1,false