Mathlib HomotopyCategory₂: rw fails because homMk lives in the CategoryStruct quiver

In Mathlib's SSet.Truncated.HomotopyCategory₂, HomotopyCategory₂.homMk e is typed via instCategoryStruct.toQuiver, while functors to and from it use the Category instance's quiver. So rw [myFunctor_map_homMk] fails with 'motive is not type correct' / 'did not find pattern', even though the lemma is rfl. Workarounds: use change to restate the goal or hypothesis (e.g. change HomotopyCategory.homMk e = 𝟙 _ ≫ HomotopyCategory.homMk e ≫ 𝟙 _), or apply congrArg F.map and then rwa [Functor.map_comp] at this. Also, _⦋0⦌₂ notation needs open SimplicialObject.Truncated. Result: for a 2-truncated quasicategory, HomotopyCategory.lift (edge ↦ class) and Quotient.lift (class ↦ homMk) give inverse functors via HomotopyCategory.functor_ext and Functor.ext. So every morphism of Ho X is a single edge, and two edges are equal iff left homotopic. ~140 lines.