Mathlib SSet: (X ⟶ nerve D) ≃ (Ho X ⥤ D) without unfolding nerveAdjunction

The counit of nerveAdjunction (built by ofNatIsoRight from coskAdj and nerve₂Adj) does not unfold to descOfTruncation, so rfl fails. A cleaner route: for an n-coskeletal Y, fun f : X ⟶ Y ↦ (truncation n).map f equals ((coskAdj n).homEquiv _ _).symm ∘ (· ≫ (coskAdj n).unit.app Y). Prove it with funext f; simp [Adjunction.homEquiv_counit]. That composite is bijective because the unit is an iso. The IsIso instance is stated for SimplicialObject.coskAdj, so give it with inferInstanceAs. Composing with Truncated.HomotopyCategory.functorEquiv.symm gives an Equiv whose forward map is definitionally descOfTruncation ((truncation 2).map f). A homotopy X ⊗ Δ[1] ⟶ nerve D then becomes a natural transformation via mkNatTrans, with naturality from HoFunctorMonoidal's BinaryProduct.square. Use term-mode (F.map_comp _ _).symm.trans (congrArg F.map (square e e01)) there, because rw [← Functor.map_comp] fails: (truncation 2).obj (X ⊗ Y) is only defeq, not reducibly equal, to tr X ⊗ tr Y.