[Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Altenkirch Thorsten]

On 06/01/2014 03:25, "Alexis Hazell" <alexis.hazell at gmail.com> wrote:

>
>richter at math.northwestern.edu writes:
>
>> My half-butted idea is that nobody has yet explained how my subject,
>> 1960s-era homotopy theory, gives a powerful explanation of why UF/Coq
>> is great.
>
>As someone who is very much an amateur in all this - I welcome any
>corrections! - my thoughts are:
>
>* As others have said, Coq is but one proof tool one can use for
>UF/HoTT; Agda is another:
>
>https://github.com/HoTT/HoTT-Agda
>
>I believe there are pros and cons to using either. In any case, however,
>it seems to me a distinction needs to be made between UF/HoTT, as areas
>of mathematics, versus Coq / Agda etc., as tools used to research and
>develop those areas.

While nobody asked for it - here is an attempt at a comparison of Coq and
Agda:

In general Coq is the more mature tool while Agda is more recent and
experimental.

Agda emphasizes dependently typed programming which gives you a very
direct and often very readable notion of (proof-)terms. On the other hand
Agda doesn't yet support tactic based proof development (hopefully this
can be emulated by improved support for proof by reflection).

Agda implements pattern matching which makes many type theoretic
constructions much more readable and intuitive but has the disadvantage
that out-of-the-box it justifies uniqueness of equality proofs which is
incompatible with HoTT. However, there is an (experimental) flag without-K
which should rule this out (pattern matching without K is currently an
active area of research - see the Agda mailing list).

Agda directly supports more flexible type definitions, e.g.
inductive-recursive and inductive-inductive definition which allow you to
introduce user defined universes. Also Agda allows mixed
inductive-coinductive definitions very directly, even though again this is
an area of active experimentation.

Agda enforces termination via a termination checker which is more flexible
but I think less principled than Coq's approach. Most of Coq could be
reduced to a core theory only using eliminators - it is less clear how to
do this for Agda. 

Agda implements universes very explicitely via (usually hidden) level
parameters. This is in principle more flexible than Coq's universe
inference but it adds lot of chatter to universe generic constructions
which frequently renders them unreadable.

Agda's syntax and approach to hidden arguments is more modern than the
corresponding baroque features in Coq.

Higher inductive types were first experimentally implemented in Agda (by
Dan Licata) using some existing features of Agda. However, I think Coq has
caught up on this now.

I cc this to the Agda and Coq lists. Hope I haven't started a flame war.
:-)

>
>* As far as I can tell, homotopy theory doesn't so much /explain/ UF,
>but is instead applied to / combined with MLTT, to create the notion of
>'types-as-spaces', and HoTT as a generalisation of that, /within/ the UF
>program. I found this blog post to be quite enlightening:
>
>"What's the big deal with HoTT?"
>https://existentialtype.wordpress.com/2013/06/22/whats-the-big-deal-with-h
>ott/
>
>Hope I've not confused things further!
>
>
>Alexis.
>
>-- 
>You received this message because you are subscribed to the Google Groups
>"Homotopy Type Theory" group.
>To unsubscribe from this group and stop receiving emails from it, send an
>email to HomotopyTypeTheory+unsubscribe at googlegroups.com.
>For more options, visit https://groups.google.com/groups/opt_out.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.