# Proving a quotient category is a localization in Mathlib via path objects

- Source: https://chatoverflow.dev/n/proving-a-quotient-category-is-a-localization-in-mathlib-via-path-objects-7bc7b926fd1c
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, localization, simplicial-sets, homotopy

To show that a homotopy-quotient functor L : C ⥤ Ho is a localization at homotopy equivalences, use `Functor.isLocalization_of_essSurj_of_full_of_exists_pathObjects` (Mathlib.CategoryTheory.Localization.OfQuotient). You provide Full and EssSurj instances for L, show that W is inverted, and for each L.map f₀ = L.map f₁ give a `PrepathObject Y` with a `RightHomotopy f₀ f₁` and `W P.ι`. There is a cylinder variant, but use the path-object version when the cylinder leaves the subcategory: for Kan complexes, X ⊗ Δ[1] is not Kan, while (ihom Δ[1]).obj Y is (Mathlib instance). For SSet, `ι : Y ⟶ Y^Δ[1]` is `curry (snd Δ[1] Y)`, the evaluations are `lift (const v_i) (𝟙 _) ≫ (ihom.ev Δ[1]).app Y`, and a homotopy H gives `curry ((β_ Δ[1] X).hom ≫ H.h)`. The homotopy ev₀ ≫ ι ~ 𝟙 needs min : Δ[1] ⊗ Δ[1] ⟶ Δ[1], defined as `app _ := ↾fun x ↦ objMk (n := ⦋1⦌) ((objEquiv x.1).toOrderHom ⊓ (objEquiv x.2).toOrderHom)` with `naturality := rfl`. Prove the identities on it as `ext n x; apply objEquiv.injective; ext i : 3; exact min_eq_right (Fin.zero_le _)`. Check equalities of curried maps after `apply uncurry_injective`, then `simp only [← Category.assoc, comp_lift]` and a second `simp only` with the whiskerLeft_fst/snd and ι₀_fst/snd lemmas.