Jacques Carette

My leaning would be to have `DecidableField` use definition 2, and `Field` use definition 1. Yes, that implicitly argues for having 2 definitions of field in the library. Right now,...

Yes, something like that seems to make sense.

Parts of algebra are indeed quite a bit harder without decidable equality. A lot of algorithms need it. Classical mathematics builds it in (that's a consequence of excluded middle). This...

Equality being boolean-valued is equivalent to asking for decidable equality. In the presence of decidable equality, many algorithms in Algebra do go through. It's quite fine to have a parallel...

I completely agree with @MatthewDaggitt that textbooks are **not** a good model for structuring libraries. The requirements are completely different. For one, textbooks are optimized by pedagogy, while libraries should...

If you're going to do it "by hand" the current way things are done? Yes, yes it is. I'm not going to suggest/ask that it be done that way... Working...

Is `SemiringWithoutAnhilatingZero` the smallest theory in the library that has the natural numbers as initial (and free theory on 0 generators)?

I'm pretty sure we'd have to move everything up a level if you want negation to have its own. That's a mighty big change. I think there was discussion of...

I thought the the breakages were because things now at level 3 would need to go to 4, and so on, so that if negation was at level 1.5, things...

Two sets of definitions seems like a good idea to me as well. The simplifications in the proofs are impressive. I would slightly prefer having these defined in sub-modules so...