The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> 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.

Yes.

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

Yes.

In the "Constructive Category" contribution, setoids (and categories)
are tuples of which the carrier is one of the component. To avoid
paradoxical constructions such as the ordinal of all ordinals, the
Calculus of Inductive Constructions forbids application of this kind
of structures to themselves.

  Require Import ConCaT.RELATIONS.Relations.
  Structure Setoid : Type :=
   {Carrier :> Type; Equal : Relation Carrier; Prf_equiv :> Equivalence 
Equal}.

Lemma eq_equivalence : Equivalence (@eq Setoid).
split; eauto using refl_equal, sym_equal, trans_equal.
Qed.

Check {|Carrier := Setoid; Equal := @eq Setoid; Prf_equiv := eq_equivalence|}.
(* Universe inconsistency *)

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

Things are different with the definition of Setoids present in the Coq
standard library (actually defined as a class but this is not
important for the current purpose):

Require Import Relations RelationClasses.
Structure Setoid (A : Type) : Type :=
  { equiv : relation A;  setoid_equiv : Equivalence equiv }.

Now, the carrier is a parameter and it can be shown that the
collection of all setoids {A : Type & Setoid A} (equivalent to the
first definition of Setoid above) has a structure of setoid itself:

Check {| equiv := @eq {A : Type & Setoid A}; setoid_equiv := eq_equivalence |}
    : Setoid {A : Type & Setoid A}.
(* OK *)

(actually, one even does not need sort-polymorphism of inductive types
as I may have thought first)

Hugo Herbelin