Theorems · Definition · category theory

CategoryTheory.Limits.Fork.ext

{C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s t : CategoryTheory.Limits.Fork f g} →
          (i : s.pt ≅ t.pt) →
            autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Fork.ext._auto_1 →
              (s ≅ t)

To construct an isomorphism between forks, it suffices to give an isomorphism between the cone points and check that it commutes with the ι morphisms.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category