Commit 2026-01-22 20:26 e6acb374

fix(AlgebraicTopology/SimplicialNerve): make SimplicialThickening a one field structure (#33866) When debugging #33822, a build failure occured in AlgebraicTopology/SimplicialNerve, which was due to a bad instance: linear orders have an automatic Category instance. Thus, recording a LinearOrder instance on SimplicialThickening J (a type alias for J when J is a linear order) would conflict with the second Category instance put later on that type (where the homs are the type of paths). This is fixed by making SimplicialThickening J a one-field structure.