The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

The end result (without definition of group). (Dunno, maybe someone finds it useful).

 

Require Import Utf8 Relations Equivalence Morphisms Setoid.

Set Implicit Arguments.

Class Equiv: Type := {

  EquivT : Type;

  EquivR : relation EquivT;

  EquivE :> Equivalence EquivR

}.

Arguments EquivT _: clear implicits.

Coercion EquivT: Equiv >-> Sortclass.

Notation "x ≡ y" := (EquivR x y) (at level 70).

Class Fun (A B: Equiv): Type := {

  FunF : @EquivT A → @EquivT B;

  FunP :> Proper (@EquivR A ==> @EquivR B) FunF

}.

Arguments Build_Fun {A} {B} _ _.

Coercion FunF: Fun >-> Funclass.

Definition FunEquiv (A B: Equiv) := @Build_Equiv (Fun A B) eq _.

Notation "x ≡> y" := (FunEquiv x y) (at level 100, right associativity).

Structure Group := {

  GroupT: Equiv;

  GroupOp: GroupT ≡> GroupT ≡> GroupT;

  GroupAssoc: ∀ a b c, GroupOp (GroupOp a b) c ≡ GroupOp a (GroupOp b c);

  GroupId: GroupT;

  GroupIdR: ∀ a, GroupOp GroupId a ≡ a;

  GroupIdL: ∀ a, GroupOp a GroupId ≡ a; 

  GroupInv: Fun GroupT GroupT;

  GroupInvR: ∀ a, GroupOp a (GroupInv a) ≡ GroupId;

  GroupInvL: ∀ a, GroupOp (GroupInv a) a ≡ GroupId;

}.

Notation "a ∘ b" := (GroupOp _ a b) (at level 60, right associativity).

Notation "a '⁻¹'" := (GroupInv _ a) (at level 55).

Notation "'e'" := (GroupId _).

Theorem T0 (G: Group) (a b: GroupT G):

  a ∘ b ≡ e → b ≡ a⁻¹.

Proof.

  intros. rewrite <- (GroupIdL _ (a⁻¹)).

  rewrite <- H. rewrite <- GroupAssoc.

  rewrite <- (GroupIdR _ b) at 1.

  rewrite (GroupInvL _ a). reflexivity.

Qed.

  

 

If one wants to make Equivalence primary in such or similar way - for example, by making a Coq extension...

I believe it's possible, but are there some reasons against it?