English
Let p be a commutative square in the opposite category. Then the square obtained by applying the opposite operation to each edge is again a commutative square.
Русский
Пусть p — коммутативный квадрат в противоположной категории. Тогда квадрат, получаемый применением операции противоположности ко всем ребрам, снова является коммутативным квадратом.
LaTeX
$$$CommSq\ f\ g\ h\ i \rightarrow CommSq\ i.unop\ h.unop\ g.unop\ f.unop$$$
Lean4
/-- The commutative square associated to a commutative square in the opposite category. -/
theorem unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CommSq f g h i) :
CommSq i.unop h.unop g.unop f.unop :=
⟨by simp only [← unop_comp, p.w]⟩
