Theorems · Definition · category theory

CategoryTheory.Limits.Fork.IsLimit.mk

{C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Fork f g) →
          (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) →
            (∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) →
              (∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt),
                  CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s) →
                CategoryTheory.Limits.IsLimit t

This is a slightly more convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category