ofCofork — Mathlib

Lean4
/-- This is a helper construction that can be useful when verifying that a category has all
coequalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)`, and a cofork on `F.map left` and `F.map right`,
we get a cocone on `F`.

If you're thinking about using this, have a look at
`hasCoequalizers_of_hasColimit_parallelPair`, which you may find to be an easier way of
achieving your goal. -/
def ofCofork {F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right)) : Cocone F
    where
  pt := t.pt
  ι :=
    { app := fun X => eqToHom (by simp) ≫ t.ι.app X
      naturality := by rintro _ _ (_ | _ | _) <;> simp [t.condition] }
Похожие утверждения