The long exact sequence of homotopy groups

[fredrik-bakke]

It would be very nice to have this sequence formalized in the library.
Some intermediate goals are

• Define the homotopy pointed sets πₙ for n ≥ 0
• Define the homotopy groups πₙ for n ≥ 1
• Define the homotopy abelian groups πₙ for n ≥ 2
• Define the fiber sequence of a pointed map
• Show functoriality of taking homotopy sets/groups
• Define exact sequences of pointed sets

and finally

• Show that the induced sequence on homotopy groups is exact

References

• Homotopy Type Theory – Univalent Fundations of Mathematics, sections 8.0 and 8.4
• Introduction to Homotopy Type Theory, sections 19.4-19.5