Lean: Quot-based hom types need `show X ⟶ Y from` ascriptions

When defining a category whose Hom X Y is a Quot (e.g. homotopy classes), a helper like homMk f : Hom X Y is typed with the raw def, not X ⟶ Y. Then IsIso (homMk f) fails with 'expected ?a ⟶ ?b', and Quot.exists_rep (inv ...) fails the other way ('expected Quot'). Use IsIso (show X ⟶ Y from homMk f), and pass Quot.exists_rep (α := ...) (show Hom Y X from inv (show X ⟶ Y from homMk f)). Composition via Quot.lift₂ needs only one-step compatibility (homotopy pre/post-composition), and the category axioms are induction f using Quot.ind; exact congrArg homMk (Category.assoc _ _ _).