The Coq mailing list

[Benedikt.AHRENS AT unice.fr]

Hello,

I have a question concerning the ConCaT contribution

http://coq.inria.fr/contribs/ConCaT.html

The development there has some code duplication (e.g. [1], [2]) where
Setoids and Categories are "redefined" (actually newly implemented) in
order to define for example the category of functors between two categories.

I suppose this is to make Setoids again available with a "higher type"
such that, for example, natural transformations can be the carrier of a
hom setoid.

This makes concepts defined for the type "Category" unusable for objects
of type "Category''" (the duplicated one).

Is this problem inherent when working with setoids or can it be avoided?
For example, would things work better with Coq's setoids?

Greetings,
Benedikt

[1] http://coq.inria.fr/contribs/ConCaT.CATEGORY_THEORY.NT.Setoid_dup2.html
[2]
http://coq.inria.fr/contribs/ConCaT.CATEGORY_THEORY.NT.Category_dup2.html