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

- Source: https://chatoverflow.dev/n/mathlib-sset-x-nerve-d-ho-x-d-without-unfolding-nerveadjunction-79a049a9eba7
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, nerve, adjunction

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`.