Commit 2026-08-31 10:08 a644e6e5

chore(Algebra/Homology): unexpose HomologicalComplexUpToQuasiIso.Qh (#43103) The consequence is that the natural isomorphism HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ≅ DerivedCategory.Q is no longer Iso.refl _, which prevents "abuse" of defeq in the syntax. At the same time, this allows to get better definitional properties for DerivedCategory.singleFunctor. (When working on individual objects, it is more convenient to work with cochain complexes rather than objects in the homotopy category, which is the reason why I am making this design choice.)