Theorems · Definition · category theory

CategoryTheory.Limits.Cowedge.ext

{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)} →
          {W₁ W₂ : CategoryTheory.Limits.Cowedge F} →
            (e : W₁.pt ≅ W₂.pt) →
              autoParam
                  (∀ (j : J),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π W₁ j) e.hom =
                      CategoryTheory.Limits.Multicofork.π W₂ j)
                  CategoryTheory.Limits.Cowedge.ext._auto_1 →
                (W₁ ≅ W₂)

A variant of CategoryTheory.Limits.Cocone.ext specialized to produce isomorphisms of cowedges.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.End

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category