conesEquivFunctor — Mathlib

Lean4
/-- (Impl) A preliminary definition to avoid timeouts. -/
@[simps]
def conesEquivFunctor (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
    Cone (widePullbackDiagramOfDiagramOver B F) ⥤ Cone F
    where
  obj
    c :=
    { pt := Over.mk (c.π.app none)
      π :=
        { app := fun ⟨j⟩ =>
            Over.homMk (c.π.app (some j))
              (c.w (WidePullbackShape.Hom.term j))
                -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10888): added proof for `naturality`

          naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨f⟩⟩ => by dsimp at f ⊢; cat_disch } }
  map
    f :=
    { hom := Over.homMk f.hom }
      -- Porting note: unfortunately `aesop` can't cope with a `cases` rule here for the type synonym
      -- `WidePullbackShape`.
      -- attribute [local aesop safe cases (rule_sets := [CategoryTheory])] WidePullbackShape
      -- If this worked we could avoid the `rintro` in `conesEquivUnitIso`.
Похожие утверждения