quotientPathsEquiv — Mathlib

Lean4
/-- The canonical quotient of the path category of a category
is equivalent to the original category. -/
def quotientPathsEquiv : Quotient (pathsHomRel C) ≌ C
    where
  functor := quotientPathsTo C
  inverse := toQuotientPaths C
  unitIso :=
    NatIso.ofComponents (fun X => by cases X; rfl)
      (Quot.ind fun f => by
        apply Quot.sound
        apply Quotient.CompClosure.of
        simp [Category.comp_id, Category.id_comp, pathsHomRel])
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (fun f => by simp)
  functor_unitIso_comp
    X := by
    cases X
    simp only [Functor.id_obj, quotientPathsTo_obj, Functor.comp_obj, toQuotientPaths_obj_as,
      NatIso.ofComponents_hom_app, Iso.refl_hom, quotientPathsTo_map, Category.comp_id]
    rfl
Похожие утверждения