The Coq mailing list

["Daniele Pucci" <pucci.daniele AT gmail.com>]

Hi,

 

I am experimenting with type classes and categories, and there is a basic point that is not still clear for me:

 

I defined a category class:

 

Class Category

  (Ob: Type)

  (Hom: Ob->Ob->Type)

  (Eqv: forall {a b}, (Hom a b) -> (Hom a b) -> Prop)

  (Id: forall ob, Hom ob ob)

  (Comp: forall {a b c}, Hom a b -> Hom b c -> Hom a c) :=

{

  eqv_equivalence : forall a b,  Equivalence (@Eqv a b);

  comp_proper : forall a b c, Proper (@Eqv a b ==> @Eqv b c ==> @Eqv a c) Comp;

  comp_associativity : forall `(f: Hom a b)`(g: Hom b c)`(h: Hom c d), Eqv (Comp (Comp f g) h) (Comp f (Comp g h));

  id_left_identity : forall `(f: Hom a b), Eqv (Comp (Id a) f) f;

  id_right_identity : forall `(f: Hom a b), Eqv (Comp f (Id b)) f

}.

 

And then I was trying to define a monoid as a category with a single object:

 

Class Monoid (Carrier: Type)(Eqv: Carrier -> Carrier -> Prop)(One: Carrier)(Comp: Carrier -> Carrier -> Carrier)  :=

  underlying_category :> Category unit (fun _ _ => Carrier) (fun _ _ => Eqv) (fun _ => One) (fun _ _ _ => Comp).

 

This class is „equivalent” to a monoid:

 

Instance Nat : Monoid nat eq O plus.

repeat split; repeat auto with *.

Qed.

 

But in reality, looking at the definition  ( Print Monoid ), you can see that this is in reality a category built using the  unit set of objects.

 

The question is:  IS THERE ANY SIMPLE WAY TO SAY  TO COQ THAT THE TYPE  unit->A  IS ISOMORPHIC TO  A, AND THEN THE CLASS OBTAINED BY SUBSTITUTING unit->unit->A WITH A WILL HAVE THE SAME INSTANCES?

 

IS IT POSSIBLE TO FIND THE „NORMAL FORM” OF THE CLASS ( THE ONE CONTAINING THE TYPE A ) AUTOMATICALLY ?

 

 

Best regards,

Daniele