@[simp]

def Category.whisker_pre (O : Type u) [𝓒 : Category O] {A B C : O} (f g : Category.Struct.Mor A B) (h : Category.Struct.Mor B C) : f = g → f ≫ h = g ≫ h

Equations

• ⋯ = ⋯

@[simp]

def Category.whisker_post (O : Type u) [𝓒 : Category O] {B C A : O} (f g : Category.Struct.Mor B C) (h : Category.Struct.Mor A B) : f = g → h ≫ f = h ≫ g

Equations

• ⋯ = ⋯

theorem Category.double_square_commutes (O : Type u) [𝓒 : Category O] {A0 A1 A2 B0 B1 B2 : O} {a0 : Category.Struct.Mor A0 A1} {a1 : Category.Struct.Mor A1 A2} {c0 : Category.Struct.Mor B0 B1} {c1 : Category.Struct.Mor B1 B2} {b0 : Category.Struct.Mor A0 B0} {b1 : Category.Struct.Mor A1 B1} {b2 : Category.Struct.Mor A2 B2} (square0 : a0 ≫ b1 = b0 ≫ c0) (square1 : a1 ≫ b2 = b1 ≫ c1) : a0 ≫ a1 ≫ b2 = b0 ≫ c0 ≫ c1

A non-trivial technical result involving the gluing of two commutative diagrams.