Change type of Pi to AbGroup for n.+2

[Alizter]

I've changed the definition of HomotopyGroup so that it is a pType at 0, Group at 1 and AbGroup at n.+2. I've adapted the rest of the library accordingly.

In order to satisfy the uniform inheritance condition for coercions, I had to split the definition of HomotopyGroup_type into two parts.

closes #1160

[Alizter]

@jdchristensen This should simplify some things in the Hurewicz branch.

[jdchristensen]

It's unfortunate that so many proofs need a separate case now. I'd be interested to see whether this simplifies things in the Hurewicz branch, or means that additional cases need to be handled. I wonder if there's a clever trick that can somehow make things a bit smoother? If nobody has any suggestions over the next day or two, then I vote to merge this, but I think it's worth waiting to see if something else is suggested. E.g., since being abelian is a property, and doesn't affect the group homomorphisms, it could be a typeclass instance applied to some objects of type Group. That's just a random idea and probably has lots of issues.

[Alizter]

I always felt like I was missing something when designing the algebra library. I feel as though there are ways to get coq to accept various casts between algebraic structures without causing too much headache. For a while, I kept reading that canonical structures was supposed to help with this, but I never managed to git it to work.

Here is a small example that demonstrates what canonical structures actually does:

Require Import Basics Types Algebra.Groups Algebra.AbGroups.

Local Open Scope mc_add_scope.
Local Open Scope mc_mult_scope.

(** G is a group that happens to be commutative. *)
Axiom G : Group.
Axiom commutative_G : Commutative ((.*.) : G -> G -> G).
Global Existing Instance commutative_G.

(** Obviously, coq has no way of knowing that this is an abgroup *)
Fail Check (G : AbGroup).

(** Say we have a lemma about abelian groups *)
Definition ab_is_great (A : AbGroup) (x y : A) : Type
  := x + y = y + x.

(** Coq can't apply this lemma to G because it's not an abelian group. *)
Fail Lemma G_is_great (x y : G) : ab_is_great _ x y.

(** But if we mark the constructor Builld_AbGroup' as a "Canonical Structure" then we can give hints as on how to use G like an abelian group to coq. The commutativity part will be found by typeclasses. *)
Canonical Structure Build_AbGroup'.

(** Now the lemma works! *)
Lemma G_is_great (x y : G) : ab_is_great _ x y.

(** But coq still cannot cast G to an abelian group. *)
Fail Check (G : AbGroup).

I feel as though this might help @jdchristensen use homotopy groups like abelian groups when needed, without having to change the type of Pi to AbGroup.

[jdchristensen]

@Alizter If something like that works, it would be very nice. But the one thing I need doesn't seem to work. I have

Definition AbHom' (A : Group) (B : AbGroup) `{Funext} : AbGroup.

and even with the canonical structures and definitions you made, AbHom' H G fails (where of course H is assumed to be a group). Maybe someone knows how to make groups cast to abelian groups when we have an instance showing that they are abelian?

[Alizter]

@jdchristensen I have spoken with the mathcomp devs also, and it has been on peoples wishlist for coq for a while now. Cyril Cohen has dubbed these "reverse coercions" and there are some discussions going on: https://coq.discourse.group/t/generalizing-coercions-to-infer-typeclass-arguments/1241/4

[Alizter]

This will need a rebase. But I also wonder if using fmap will change anything with respect to the separate cases that were forced.

[jdchristensen]

I'd still like to try my GroupWithStructure idea (or maybe it should be called GroupWithProperty), but I'm behind on too many things right now to give it a shot. If someone else wants to try, that would be great. Or we could put this on the backburner for a while, if it isn't blocking anything else.

[Alizter]

Don't have time to work on this any longer.