Theorems · Definition · category theory

CategoryTheory.Limits.pullback.congrHom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f₁ f₂ : X ⟶ Z} →
        {g₁ g₂ : Y ⟶ Z} →
          f₁ = f₂ →
            g₁ = g₂ →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ g₁] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₂ g₂] →
                  CategoryTheory.Limits.pullback f₁ g₁ ≅ CategoryTheory.Limits.pullback f₂ g₂

If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback