Theorems · Definition · category theory

CategoryTheory.Limits.Cofan.ext

{β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        {c₁ c₂ : CategoryTheory.Limits.Cofan f} →
          (e : c₁.pt ≅ c₂.pt) →
            autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b)
                CategoryTheory.Limits.Cofan.ext._auto_1 →
              (c₁ ≅ c₂)

A version of Cocone.ext for Cofans.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category