Commit 2025-05-20 14:06 9baf55b0

refactor: change CWComplex from abbrev to its own class (#24712) This PR makes the classical absolute CW complex into its own class. This is done to

• make typeclass inference able to infer facts about CWComplex without always passing through RelCWComplexes, and
• to give CWComplex a constructor so constructing instances of CWComplex is easier. The reason why the fields of CWComplex are protected is that we always want cell and map to refer to RelCWComplex.cell and RelCWComplex.map through the instance: that ensures that lemmas about RelCWComplex directly apply to CWComplex. Since all of these fields talk about the CWComplex versions of map and cell they should never be used.