Theorems · Definition · category theory

CategoryTheory.IsPullback.isoIsPullback

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : C} →
      (X Y : C) →
        {Z : C} →
          {fst : P ⟶ X} →
            {snd : P ⟶ Y} →
              {f : X ⟶ Z} →
                {g : Y ⟶ Z} →
                  {P' : C} →
                    {fst' : P' ⟶ X} →
                      {snd' : P' ⟶ Y} →
                        CategoryTheory.IsPullback fst snd f g → CategoryTheory.IsPullback fst' snd' f g → (P ≅ P')

Any object at the top left of a pullback square is isomorphic to the object at the top left of any other pullback square with the same cospan.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category