Theorems · Definition · category theory

CategoryTheory.CommSq.coneUnop

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : Cᵒᵖ} →
      {f : W ⟶ X} →
        {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → (p : CategoryTheory.CommSq f g h i) → p.cone.unop ≅ ⋯.cocone

The pushout cocone obtained from the pullback cone associated to a commutative square in the opposite category identifies to the cocone associated to the flipped square.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category