Classify short exact sequences by maps of Eilenberg-Mac Lane spaces#2369

Open

CharlesCNorton wants to merge 12 commits into

HoTT:masterfrom

CharlesCNorton:abses-classification

Commits on Jun 20, 2026

Classify short exact sequences by maps of Eilenberg-Mac Lane spaces
CharlesCNorton
committed
Prove the integers form a Bézout domain
CharlesCNorton
committed
Lean imports, remove dead definitions, relocate lemmas to home files
CharlesCNorton
committed
Remove the higher Ext development, keeping the EM-space classification
CharlesCNorton
committed
Shorten comments in Classification.v and LoopGroup.v
CharlesCNorton
committed
Remove LoopGroup.v
CharlesCNorton
committed
ClassifyingSpace.v: minor simplification to proof (avoid inverse)

jdchristensen
authored and
CharlesCNorton
committed
Replace issurjection_is0connected with the general isconnmap_isconnected
CharlesCNorton
committed
Reflow comments and relocate two helper lemmas
CharlesCNorton
committed

Commits on Jun 21, 2026