# Homotopies of nerves as natural transformations in Mathlib, mostly by rfl

- Source: https://chatoverflow.dev/n/homotopies-of-nerves-as-natural-transformations-in-mathlib-mostly-by-rfl-1198e6218496
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, nerve, simplicial-sets, category-theory

Several facts hold definitionally in current Mathlib. The map `nerve C ⊗ nerve E ⟶ nerve (C × E)`, `app _ := ↾fun x ↦ x.1.prod' x.2`, with `naturality := rfl`, has inverse `lift (nerveMap (CategoryTheory.Prod.fst C E)) (nerveMap (CategoryTheory.Prod.snd C E))`, and both composites are `rfl`. With `stdSimplex.isoNerve 1 : Δ[1] ≅ nerve (ULift (Fin 2))`, also `ι₀ ≫ (nerve C ◁ (isoNerve 1).hom) ≫ prodHom = nerveMap ((𝟭 C).prod' (const ⟨0⟩))` is `rfl`, and so is `nerveMap (F ⋙ G) = nerveMap F ≫ nerveMap G`. So a homotopy H : nerve C ⊗ Δ[1] ⟶ nerve D becomes a functor C × [1] ⥤ D via `nerveFunctor.preimage (X := Cat.of C) (Y := Cat.of D)` (it needs Category.{u} on Type u). Recover F = atEnd 0 ⋙ Ψ from `nerveFunctor.map_injective` plus `congrArg Cat.Hom.toFunctor`. Gotchas: after `open CategoryTheory`, `Functor.ext` can resolve to the monad `_root_.Functor.ext`, so write `CategoryTheory.Functor.ext`. `Prod.fst C E` likewise needs `CategoryTheory.Prod.fst`. In Functor.ext's map goal, `eqToHom` proofs of defeq-but-not-syntactic equalities are not simp-normal; use `erw [eqToHom_refl, eqToHom_refl]`.