Brief Introduction and questions about Coq vs. Agda codebase

[Clarissa Littler]

Hello,

I've been following this mailing list on and off for awhile now with great interest but little temerity. I'm a phd student and I read through most of the HoTT book, and was at OPLSS last year, but at this point I'd like to get my hands a bit dirtier.

To that end, it's my understanding that there's both a Coq and an Agda codebase and since I'm fluent in both theorem provers I was wondering if there was a general preference in terms of which is used and what they're used for, or if it was just a matter of what proof assistant one was more comfortable with?

Cheers,

Clarissa

[Michael Shulman]

It's mostly a matter of what one is comfortable with. Generally
speaking, the people who prefer Coq have coded in Coq and the people
who prefer Agda have coded in Agda. You're undoubtedly familiar with
the relative advantages and disadvantages of the two in general (e.g.
tactic proofs versus proof-terms with holes, typical ambiguity versus
explicit universe polymorphism), which apply just as well when doing
HoTT. Historically, there have been a few issues with one or the
other specific to HoTT, but most or all of them are no longer
relevant.

1. It used to be the case that higher inductive types could be faked
better in Agda; Dan Licata invented a trick using private types that
could be used to get HITs with judgmental computation rules for
point-constructors (as are used in the book). This didn't used to be
possible in Coq, but more recently it's been hacked to support a
similar mechanism. So as long as you use the version of Coq
suggested/required by the HoTT Coq library, there is no difference
here any more.

2. Coq's rules for universes and its treatment of the special universe
"Prop" (in particular, singleton elimination) didn't used to be
(obviously) compatible with univalence. This has also been mostly
fixed by patches implementing a new flag -indices-matter.

3. Coq's typical ambiguity didn't used to be flexible enough to
support some of the stuff we want to do with universes in HoTT, but
Mathieu has recently implemented better universe polymorphism.

4. By default, Agda allows a sort of pattern-matching that is not
compatible with univalence (it allows you to prove axiom K). There is
now a flag --without-K which modifies Agda's pattern-matching so that
it no longer allows you to prove axiom K in the obvious way. However,
no one has proven that Agda using --without-K *is* compatible with
univalence, and I think people still occasionally find issues with it
that need to be fixed. (So --without-K should really be called
--without-all-the-incompatibilities-with-univalence-that-we've-thought-of-so-far.)
However, in practice this is not really a problem: it's pretty easy
to restrict your coding style to only use pattern-matching as
syntactic sugar for the induction principle, the way the book does.

Mike

> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Edward Z. Yang]

The Coq HoTT library has been around longer, and so has accumulated more
"stuff" (e.g. there is HoTTBook.v, but no HoTTBook.agda), but Agda is a
lot more pleasant for constructing the proof terms that are endemic in
HoTT, and has better "support" for HITs, so you might try it first now
that it is developed.

Edward

Excerpts from Clarissa Littler's message of 2014-03-17 10:38:14 -0700:

[Vladimir Voevodsky]

On Mar 17, 2014, at 2:21 PM, Michael Shulman <shu...@sandiego.edu> wrote:

4. By default, Agda allows a sort of pattern-matching that is not
compatible with univalence (it allows you to prove axiom K).  There is
now a flag --without-K which modifies Agda's pattern-matching so that
it no longer allows you to prove axiom K in the obvious way.  However,
no one has proven that Agda using --without-K *is* compatible with
univalence, and I think people still occasionally find issues with it
that need to be fixed.  (So --without-K should really be called
--without-all-the-incompatibilities-with-univalence-that-we've-thought-of-so-far.)
However, in practice this is not really a problem: it's pretty easy
to restrict your coding style to only use pattern-matching as
syntactic sugar for the induction principle, the way the book does.

For many of us this is a very important point. 

I have spent a lot of time and effort checking that the mechanism of inductive definitions in the original CIC i.e. assuming that everything is expressed through recursors is compatible with the univalence.

The actual inductive mechanism in Coq deviates from CIC but not too much and we have reasonable confidence that except for Singleton Elimination and a closely related issue in the assignment of universe levels to inductive types which is fixed by Dan Grayson’s patch “inductive-indices-matter”  it is compatible with univalence. 

The inductive machinery of Agda is much more flexible (e.g. induction-recursion) and it has never been in any way verified to be compatible with univalence.

Vladimir.

[Clarissa Littler]

Perhaps a foolish question, but if without-k is correct and doesn't force UIP then how *could* agda break univalence? What kinds of things can go wrong?

[Maxime Dénès]

Well, as an example, a few weeks ago I ported a recent paradox from Coq
to Agda, which shows that the termination checking was inconsistent with
Univalence. The problem seems to be still there:
https://code.google.com/p/agda/issues/detail?id=1023

My code was refined by Conor McBride, to show that it didn't
fundamentally need K.

Maxime.

On 03/17/2014 03:00 PM, Clarissa Littler wrote:
>
>
> On Mar 17, 2014 11:53 AM, "Vladimir Voevodsky" <vlad...@ias.edu

> <mailto:vlad...@ias.edu>> wrote:
> >
> >
> > On Mar 17, 2014, at 2:21 PM, Michael Shulman <shu...@sandiego.edu

> --
> 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 HomotopyTypeThe...@googlegroups.com

> <mailto:HomotopyTypeThe...@googlegroups.com>.

[Dan Licata]

Hi Clarissa,

Just in case people missed it in the other thread, there is a
proven-correct implementation of without-K now:
http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf

In terms of knowing whether the "theory" of Agda (which admitedly is not
very well-defined), I think the main issue is that Agda is very liberal
about mutual definitions, which gives you things like
induction-induction (simultaneously defining two inductive types, one
indexed by the other) and induction-recursion (simultaneously defining
an inductive type and another type family definied by recursion on it)
and combinations and generalizations of the two (e.g. you can
simultaneously define an inductive type and recursively define a binary
relation on it). I don't think we know that these are compatible with
univalence (though I would be surprised if they weren't).

But there are other small issues like the bugs in the termination
checker that both Agda and Coq currently have.

-Dan

[Michael Shulman]

Peter's and my construction of higher inductive types in model
categories (including univalent models such as simplicial sets):
http://ncatlab.org/homotopytypetheory/files/hit-semantics.pdf
can be extended to higher inductive-inductive definitions. This
includes, in particular, ordinary inductive-inductive definitions,
which are therefore compatible with univalence. I haven't written out
the details (and, in particular, I haven't tried to describe exactly a
general class of definitions that it works for), but I was convinced
of it last year (otherwise I would have been iffier about using higher
inductive-inductive types in the book). Writing it out carefully is
on the to-do list. The basic idea is to look at the categorical
semantics of inductive-inductive definitions in terms of dialgebras
(http://www.cs.nott.ac.uk/~txa/publ/catind2.pdf) and reformulate it in
terms of iterated algebras for endofunctors using the fact that
certain functors have left adjoints, then use the same technology of
free monads and colimits of monads.

Inductive-recursive definitions are a bit trickier, but I think we may
be making some progress. Further bulletins as events warrant.

Of course, it'd be tricky to prove that everything allowed by Agda is
compatible with univalence without a formal specification of exactly
what Agda allows. (-:

On Mon, Mar 17, 2014 at 12:50 PM, Dan Licata <d...@cs.cmu.edu> wrote:
> Hi Clarissa,
>
> Just in case people missed it in the other thread, there is a
> proven-correct implementation of without-K now:
> http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf
>
> In terms of knowing whether the "theory" of Agda (which admitedly is not
> very well-defined), I think the main issue is that Agda is very liberal
> about mutual definitions, which gives you things like
> induction-induction (simultaneously defining two inductive types, one
> indexed by the other) and induction-recursion (simultaneously defining
> an inductive type and another type family definied by recursion on it)
> and combinations and generalizations of the two (e.g. you can
> simultaneously define an inductive type and recursively define a binary
> relation on it). I don't think we know that these are compatible with
> univalence (though I would be surprised if they weren't).
>
> But there are other small issues like the bugs in the termination
> checker that both Agda and Coq currently have.
>
> -Dan
>
> On Mar17, Clarissa Littler wrote:

[Clarissa Littler]

Well, I appreciate all the responses and the conversation that's been happening. I have a bit of a follow-up question, though: so are there any current problems that would be sensible for someone not-new-to-formalizing but new-to-formalizing-for-HoTT to work out? I saw the open problems list but they're a bit bigger scale than a "I'd like to contribute something non-trivial while learning my way around the libraries and techniques" problem.

Cheers,

Clarissa

[Bas Spitters]

Not very specific, but this is a good place to start:

https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBook.v

[Andrej Bauer]

As Bas says, we'd be delighted to accept contributions to HoTTBook.v
in the HoTT library. This is perhaps a bit mundane, as it requires you
to sift through the library to figure out where in the library a given
book theorem can be found. A bit less mundane would be contributions
to

https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBookExercises.v

which contain solutions to book exercises. In any case, both are a
good way of familiarizing yourself with the library.

On Mon, Mar 17, 2014 at 10:03 PM, Clarissa Littler
<clarissa...@gmail.com> wrote:

[Altenkirch Thorsten]

It was already mentioned but I'd like to make clear that this is a serious
issue which affects both checkers:

5. Both Coq's and Agda's termination checker allow proofs which contradict
univalence. This is different to point 4 below and is not addressed by
Jasper's recent announcement that he has a verified "without-K" mode for
Agda (I haven't checked the details of this.

Thorsten

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.

[Michael Shulman]

Can you explain briefly what the problem is? The Agda code I saw at
the link posted used coinductive types; does the problem only have to
do with those?

[Maxime Dénès]

Hi,

The original problem was found for fixpoints on inductive types. I
translated it later on to co-fixpoints.

I'll try to summarize it here.

The termination checking of Coq and Agda (essential for consistency of
course) is done in a syntactic way. Which means that each object of an
inductive type is associated with a "size" (in terms of the numbers of
constructors used to build it). The termination criterion ensures that
every fixpoint is defined in such a way that its recursive calls occur
only on strictly smaller terms. The order defined by the size being
well-founded, termination follows. Now, how do you get a syntactically
"strictly smaller" object from an existing one? By pattern matching.

So far, so good. The problem is that you may have some type isomorphisms
that do not preserve size. Hence, your theory can potentially
distinguish between two isomorphic types. If you identify isomorphic
types and you allow size information of objects to flow through type
equalities, you'll get a contradiction.

In Coq, the same thing shows up when using propositional extensionality
which identifies equivalent propositions. Here is a refined example,
posted by Cristobal Camarero on Coq-club:

Axiom prop_ext: forall P Q, (P<->Q)->P=Q.

Inductive True2:Prop:= I2: (False->True2)->True2.

Theorem Heq: (False->True2)=True2.
Proof.
apply prop_ext. split.
- intros. constructor. exact H.
- intros. exact H.
Qed.

Fail Fixpoint con (x:True2) :False :=
match x with
I2 f => con (match Heq in _=T return T with eq_refl => f end)
end.

Note that this does not rely on impredicativity, so you can get the same
contradiction from a type in Set and univalence. If you look at the type
isomorphism built in the proof of Heq, you will see that it adds a
constructor.

Following ideas from Bruno Barras, I have implemented a fix for Coq:
https://github.com/maximedenes/coq/tree/guard-fix
Essentially, we restrict the flow of size information through type
equalities.

I am writing a more detailed description of the guard condition
obtained. Fixing Agda maybe more difficult, because the fix uses the
elimination predicate that Coq's pattern matching carries over (also
used to avoid K). The flow of size information through type equalities
is allowed or not depending on this predicate.

Maxime.

[Steve Awodey]

Thanks for this summary Maxime!

I have some questions about one point below, but I’m sure it’s just my lack of familiarity with the details:

On Mar 18, 2014, at 11:20 AM, Maxime Dénès <ma...@maximedenes.fr> wrote:

> Hi,
>
> The original problem was found for fixpoints on inductive types. I translated it later on to co-fixpoints.
>
> I'll try to summarize it here.
>
> The termination checking of Coq and Agda (essential for consistency of course) is done in a syntactic way.

the termination checking procedure is essential for the *usual proof* of consistency, right?
if it breaks, that doesn’t mean the system is inconsistent — just that we can’t run the usual proof.
right?

> Which means that each object of an inductive type is associated with a "size" (in terms of the numbers of constructors used to build it). The termination criterion ensures that every fixpoint is defined in such a way that its recursive calls occur only on strictly smaller terms. The order defined by the size being well-founded, termination follows. Now, how do you get a syntactically "strictly smaller" object from an existing one? By pattern matching.
>
> So far, so good. The problem is that you may have some type isomorphisms that do not preserve size. Hence, your theory can potentially distinguish between two isomorphic types.

“potentially” because we don’t kow that the syntactic property of “size” can actually be formalized inside the system — right?
in fact, I would not expect a syntactic property having to do with the numbers of constructors involved to be formalizable.

> If you identify isomorphic types and you allow size information of objects to flow through type equalities, you'll get a contradiction.

but again: only potentially, i.e. if the syntactic property of size can be formalized.
right?

>
> In Coq, the same thing shows up when using propositional extensionality which identifies equivalent propositions. Here is a refined example, posted by Cristobal Camarero on Coq-club:
>
> Axiom prop_ext: forall P Q, (P<->Q)->P=Q.
>
> Inductive True2:Prop:= I2: (False->True2)->True2.
>
> Theorem Heq: (False->True2)=True2.
> Proof.
> apply prop_ext. split.
> - intros. constructor. exact H.
> - intros. exact H.
> Qed.
>
> Fail Fixpoint con (x:True2) :False :=
> match x with
> I2 f => con (match Heq in _=T return T with eq_refl => f end)
> end.
>
> Note that this does not rely on impredicativity, so you can get the same contradiction from a type in Set and univalence. If you look at the type isomorphism built in the proof of Heq, you will see that it adds a constructor.

Are you saying that there is an actual contradiction with propositional extensionality here ?

Sorry for the naive questions!

Thanks,

Steve

[Michael Shulman]

On Tue, Mar 18, 2014 at 8:20 AM, Maxime Dénès <ma...@maximedenes.fr> wrote:
> Fail Fixpoint con (x:True2) :False :=
> match x with
> I2 f => con (match Heq in _=T return T with eq_refl => f end)
> end.

Why is it only univalence that creates this problem? I thought the
"structurally smaller calls" rule would mandate that inside the match,
the function "con" could only be called recursively on the values (f
x) for any x:False. Why are we allowed to apply some other random
function to it (such as coercing it along an equality of types)?

Mike

[Maxime Dénès]

Hello Steve,

Indeed, the first three points are only potential inconsistencies. But
the example is a concrete one :) The fixpoint "con" has type True2 ->
False, and True2 is inhabited (just build a proof H of False -> True2
and take I2 H).

My choice of the word "essential" was a bit unfortunate. I indeed meant
that it is an essential argument for the usual proof of consistency
(every closed term has a normal form, normal forms in inductive types
are in constructor form, there is no constructor in False, so there is
no closed proof of False).

As far as I understand, the trouble with syntactic criteria is that the
flexibility required in practice is in tension with an easy
interpretation in more semantical consistency proofs, like the one
justifying the propositional extensionality axiom, based on the
set-theoretical (proof-irrelevant) model.

Maxime.

On 03/18/2014 12:00 PM, Steve Awodey wrote:
> Thanks for this summary Maxime!
>
> I have some questions about one point below, but I'm sure it's just my lack of familiarity with the details:
>
> On Mar 18, 2014, at 11:20 AM, Maxime Dénès <ma...@maximedenes.fr> wrote:
>
>> Hi,
>>
>> The original problem was found for fixpoints on inductive types. I translated it later on to co-fixpoints.
>>
>> I'll try to summarize it here.
>>
>> The termination checking of Coq and Agda (essential for consistency of course) is done in a syntactic way.
> the termination checking procedure is essential for the *usual proof* of consistency, right?

> if it breaks, that doesn't mean the system is inconsistent -- just that we can't run the usual proof.

> right?
>
>
>> Which means that each object of an inductive type is associated with a "size" (in terms of the numbers of constructors used to build it). The termination criterion ensures that every fixpoint is defined in such a way that its recursive calls occur only on strictly smaller terms. The order defined by the size being well-founded, termination follows. Now, how do you get a syntactically "strictly smaller" object from an existing one? By pattern matching.
>>
>> So far, so good. The problem is that you may have some type isomorphisms that do not preserve size. Hence, your theory can potentially distinguish between two isomorphic types.

> "potentially" because we don't kow that the syntactic property of "size" can actually be formalized inside the system -- right?

[Altenkirch Thorsten]

Basically the termination checker assumes that using transport doesn't
change size. This is a reasonable assumption if the only proof of equality
is refl and hence the only computation transport can perform is identity.
However, this ceases to be true in the presence of univalence when
transport may have to execute any equivalence which may not be size
preserving (as the examples show).

The real bug (independent of univalence) is that the termination checker
accepts programs which cannot be implemented using the eliminator. This
should be part of the spec of the termination checker. I always thought
this was shown by Conor McBride and I am still confused wether this is a
bug in his PhD or it just means that the implementations are not faithful
to his spec.

Thorsten

[Maxime Dénès]

Thorsten said why it was believed to be correct. As for the motivation,
it comes as often from practical examples. One such example by Christine
Paulin is:

Definition pred n : n<>0 -> nat :=
match n returns (n<>0 -> nat) with
| 0 => fun k : 0<>0 => match k (refl 0) with end
| S p => fun k => p
end.

Now, if you define a fixpoint over natural numbers, you may want, in a
context where you have a proof H of n <> 0, to make a recursive call on
pred n H (n being the decreasing argument of the fixpoint).

Although you can often avoid this kind of constructions when you write
programs or proofs terms, a stricter guard condition will give you
unexpected failures when proving using tactics. And even for programs,
it may be very useful (to define the gcd on natural numbers for instance).

Maxime.

[Michael Shulman]

Your example doesn't seem to me to be explained by Thorsten's
explanation. Thorsten said that the termination checker assumes that
transport doesn't change size, which sounds as though the termination
checker has a special case built in to allow transport. But your
example doesn't use transport. Is there an underlying more general
class of functions that the termination checker "assumes don't change
size" which includes transport and also pred?

I'm also confused as to why anyone would expect to be able to make a
recursive call directly on pred n H. It seems to me as though that
clearly requires using "strong induction" rather than ordinary
induction, i.e. inducting over the well-founded relation le rather
than using the ordinary induction principle of the naturals. Are you
saying that the termination checker is trying to allow strong
induction without requiring the user to specify its use explicitly?

[Altenkirch Thorsten]

No I didn't mean that you have to use transport explicitely. What I meant
is that what the termination checker is doing is equivalent to assuming
that transport doesn't change size.

T.

[Michael Shulman]

Can you say anything comprehensible to a layman like me about what the
termination checker *is* doing?

[Altenkirch Thorsten]

You construct all possible circular call paths and check wether there is a
lexical ordering of arguments which always reduces constructor size.

I'd say this is the obvious thing but Andreas and I wrote a paper about it
in 2002:
"A predicative analysis of structural recursion", JFP 2002
http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf


The termination checker we were proposing doesn't take types into account.
I think this is also true for the termination checkers implemented in Coq
and Agda.

Thorsten

[Maxime Dénès]

On 03/18/2014 02:46 PM, Michael Shulman wrote:
> Your example doesn't seem to me to be explained by Thorsten's
> explanation. Thorsten said that the termination checker assumes that
> transport doesn't change size, which sounds as though the termination
> checker has a special case built in to allow transport. But your
> example doesn't use transport. Is there an underlying more general
> class of functions that the termination checker "assumes don't change
> size" which includes transport and also pred?

It is a bit more complex: the termination checker doesn't know anything
about transport or any function specifically. However, there is a rule
saying when a pattern matching expression (in Coq's sense) can be used
as a recursive argument. This is what allows a recursive call to be made
on pred n H. That rule used to be: if each of the branches returns a
term that is "strictly smaller" than the original argument, then the
whole match expression can be used as argument of a recursive call.

If you think of match expressions as simple case analyses, everything is
fine. But in a dependently typed setting, you can use it to express
transport (by matching on an equality proof).

>
> I'm also confused as to why anyone would expect to be able to make a
> recursive call directly on pred n H. It seems to me as though that
> clearly requires using "strong induction" rather than ordinary
> induction, i.e. inducting over the well-founded relation le rather
> than using the ordinary induction principle of the naturals. Are you
> saying that the termination checker is trying to allow strong
> induction without requiring the user to specify its use explicitly?

I am not sure to understand fully, but a recursive call on pred n H
seems legitimate even considering ordinary induction and a case
analysis: if you have a proof that the argument n is not 0, by case
analysis it should be a S p, so you want to make the recursive call on p.

Maxime.

[Maxime Dénès]

On 03/18/2014 03:24 PM, Altenkirch Thorsten wrote:
> You construct all possible circular call paths and check wether there is a
> lexical ordering of arguments which always reduces constructor size.
>
> I'd say this is the obvious thing but Andreas and I wrote a paper about it
> in 2002:
> "A predicative analysis of structural recursion", JFP 2002
> http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf
>
>
> The termination checker we were proposing doesn't take types into account.
> I think this is also true for the termination checkers implemented in Coq
> and Agda.

Due to impredicativity and the example by Thierry Coquand that you
mention in your paper, Coq's checker needs a bit of type information,
but not much (simply what is the tree of legal recursive subterms for a
given inductive type).

Maxime.

[Michael Shulman]

Thanks for the explanations, Maxime and Thorsten; I think I now have
as much of a layman's understanding as possible. (-:

On Tue, Mar 18, 2014 at 12:25 PM, Maxime Dénès <ma...@maximedenes.fr> wrote:
> I am not sure to understand fully, but a recursive call on pred n H seems
> legitimate even considering ordinary induction and a case analysis: if you
> have a proof that the argument n is not 0, by case analysis it should be a S
> p, so you want to make the recursive call on p.

Ordinary induction says that when defining f(n+1), you can recursively
call f(n). But it sounds to me like you're saying that you can also
call f(pred(n)), which is not justified by ordinary induction.

[Michael Shulman]

On Tue, Mar 18, 2014 at 12:32 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> Ordinary induction says that when defining f(n+1), you can recursively
> call f(n). But it sounds to me like you're saying that you can also
> call f(pred(n)), which is not justified by ordinary induction.

Ah, I see; but it is allowed by the sort of deep pattern-matching that
both Coq and Agda support.

match n with
| 0 => ...
| S 0 => ...
| S (S n) => ...
end

So this isn't (supposed to) add anything beyond what deep
pattern-matching can do (although that itself is justified by reducing
to strong induction, or a weaker version of it adapted to the
particular match).

[Maxime Dénès]

Actually, we were just off-by-1. In the example I had in mind, you would
build f(n) and get by some argument that H : n<>0, then you want to call
f(pred n H).

But as you said, Coq and Agda also support recursion on deep subterms.
However, Gimenez showed [1] that you can encode this with usual
recursors (using auxiliary inductive types).

The relationship between recursors and the current guard condition,
which has been extended over the years, is unclear to me.

Maxime.

[1] Eduardo Giménez: Codifying Guarded Definitions with Recursive
Schemes. TYPES 1994: 39-59

[Favonia]

I'd like to point out that while the Coq library indeed has more
stuff, it's certainly not a superset. For example, the Blakers-Massey
was first formalized in Agda, and it's probably still the only
formalized version. Guillaume and many other people also rebuilt the
whole library from scratch with some new ideas, like an abstract type
for paths over paths. I think they are still unique to the current
Agda library.

-Favonia


On Mon, Mar 17, 2014 at 2:34 PM, Edward Z. Yang <ezy...@mit.edu> wrote:
> The Coq HoTT library has been around longer, and so has accumulated more
> "stuff" (e.g. there is HoTTBook.v, but no HoTTBook.agda), but Agda is a
> lot more pleasant for constructing the proof terms that are endemic in
> HoTT, and has better "support" for HITs, so you might try it first now
> that it is developed.
>
> Edward
>
> Excerpts from Clarissa Littler's message of 2014-03-17 10:38:14 -0700:

>> Hello,
>> I've been following this mailing list on and off for awhile now with great
>> interest but little temerity. I'm a phd student and I read through most of
>> the HoTT book, and was at OPLSS last year, but at this point I'd like to
>> get my hands a bit dirtier.
>>
>> To that end, it's my understanding that there's both a Coq and an Agda
>> codebase and since I'm fluent in both theorem provers I was wondering if
>> there was a general preference in terms of which is used and what they're
>> used for, or if it was just a matter of what proof assistant one was more
>> comfortable with?
>>
>> Cheers,
>> Clarissa
>>
>