isomorphismClasses — Mathlib

Lean4

/-- The functor that sends each category to the quotient space of its objects up to an isomorphism.
-/
def isomorphismClasses : Cat.{v, u} ⥤ Type u
    where
  obj C := Quotient (isIsomorphicSetoid C.α)
  map {_ _} F := Quot.map F.obj fun _ _ ⟨f⟩ => ⟨F.mapIso f⟩
  map_id
    {C} := by -- Porting note: this used to be `tidy`

    apply funext; intro x
    apply @Quot.recOn _ _ _ x
    · intro _ _ p
      simp only [types_id_apply]
    · intro _
      rfl
  map_comp {C D E} f
    g := by -- Porting note(s): idem

    apply funext; intro x
    apply @Quot.recOn _ _ _ x
    · intro _ _ _
      simp only
    · intro _
      rfl

Похожие утверждения