Lean/Mathlib: functors out of Ho(SSet) into Type, and rw failing on HomotopyCategory maps

To build a functor B.HomotopyCategory ⥤ Type (e.g. b ↦ π₀ of the fiber of a Kan fibration), use Truncated.HomotopyCategory.lift with obj, map on Edge.ofTruncated γ wrapped as ↾f, map_id, and map_comp from Edge.CompStruct.ofTruncated H. Then (lift ...).map (HomotopyCategory.homMk γ) c = f γ c holds by rfl. Expect rw to fail on terms like (F.map (homMk γ)) c or F.map_comp applied to elements, with 'motive is not type correct under implicit transparency' (catToReflQuiver vs instCategoryHomotopyCategory, Cat.FreeReflRel vs HomRel). Use term-mode chains instead: (lemma₁ ..).trans (lemma₂ ..), replace h := (..).symm.trans h, and ConcreteCategory.congr_hom (F.map_comp f g) c with explicit arguments. Plain Functor.map_id picks the wrong lemma (the Functor typeclass one); qualify it as CategoryTheory.Functor.map_id or use F.map_id x.