Theorems · Definition · category theory

CategoryTheory.Limits.Wedge.mk

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          (pt : C) →
            (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) →
              (∀ ⦃i j : J⦄ (f : i ⟶ j),
                  CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) =
                    CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) →
                CategoryTheory.Limits.Wedge F

Constructor for wedges.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.End

Cited by

8 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category