Theorems · Theorem · category theory

CategoryTheory.IsPushout.desc.congr_simp

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f f_1 : Z ⟶ X} (e_f : f = f_1)
  {g g_1 : Z ⟶ Y} (e_g : g = g_1) {inl inl_1 : X ⟶ P} (e_inl : inl = inl_1) {inr inr_1 : Y ⟶ P} (e_inr : inr = inr_1)
  (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h h_1 : X ⟶ W) (e_h : h = h_1) (k k_1 : Y ⟶ W) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  hP.desc h k w = ⋯.desc h_1 k_1 ⋯

Defined in

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

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category