search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Change HomotopyGroup_type to be AbGroup when above n=1. #1160

Open Alizter opened 4 years ago

Alizter commented 4 years ago

We should change the HomotopyGroup_type so that when n is larger than 1 we have the type of abelian groups. This will allow us to do abelian group things to the higher homotopy groups.

Alizter commented 4 years ago

I had originally tried this but I couldn't get it to work. Now that Mike has the coercions working it might be worth trying again.

Alizter commented 4 years ago

This can be done, but it means all lemmas involving homotopy groups get split into three cases. We cannot treat the group and abelian group cases together.