ofπ — Mathlib

Lean4
/-- Construct a multicofork using a collection `π` of morphisms. -/
@[simps]
def ofπ {J : MultispanShape.{w, w'}} (I : MultispanIndex J C) (P : C) (π : ∀ b, I.right b ⟶ P)
    (w : ∀ a, I.fst a ≫ π (J.fst a) = I.snd a ≫ π (J.snd a)) : Multicofork I
    where
  pt := P
  ι :=
    { app := fun x =>
        match x with
        | WalkingMultispan.left a => I.fst a ≫ π _
        | WalkingMultispan.right _ => π _
      naturality :=
        by
        rintro (_ | _) (_ | _) (_ | _ | _) <;> dsimp <;>
          simp only [Functor.map_id, MultispanIndex.multispan_obj_left, Category.id_comp, Category.comp_id,
            MultispanIndex.multispan_obj_right]
        symm
        apply w }
Похожие утверждения