The Coq mailing list

[ben <Benedikt.Ahrens AT unice.fr>]

Hi David,

no, it's not about universes. Even when using records i have never had
to duplicate definitions to avoid universe clashes (as in ConCaT). That
is thanks to the carrier of setoids being a parameter in the modern
implementation of setoids of Coq, whereas in ConCaT it is a field of a
record.

The reason why there are bundled (records) and unbundled (classes)
versions of all definitions is that i did (and do) not really know what
the better way is.

On the one hand you cannot avoid bundling when you want your structures
to be objects or morphisms of a category.

On the other hand, type classes seem more flexible, even though i have
not encountered many situations where i'd profit from this flexibility.
(One of them was already mentioned : you can have a type class instance
CAT, but not such a record.)

So i started with classes, but found myself using the bundled version
afterwards all the time, for the mentioned reason. Another reason was
that at that time i did not know the solutions to the problems that come
with the use of classes, such as lack of notations for the parameters of
the classes (*).

greetings,
b

(*) These problems (and solutions) are exhibited e.g. in a paper by
Spitters and v.d. Weegen in Coq2 and ITP 2010, see
http://www.xs4all.nl/~weegen/eelis/research/math-classes/

David Leduc wrote:
> Hi Ben,
> 
>> (You can find all of this in my lib of cats on
>> http://math.unice.fr/~ahrens ;).
> 
> I had a look at it. It looks good.
> 
> Why do you split the definition of a category into first a class and
> then a record?
> Does it help with duplication of definitions?