The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi, Daniele --

Do you have a notion of isomorphisms for categories? If so, you should be able to prove something like:

Iso (unit -> A) A

Where these things refer to the categories and then prove that this Iso is refexive and transitive. Then you will probably want to prove your lemmas up to isomorphism of categories. I've done things like this for other structures and it works out reasonably well but it is a little bit verbose.

On Wed, Sep 19, 2012 at 10:00 AM, Daniele Pucci <pucci.daniele AT gmail.com> wrote:

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

 

 

 

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/