no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G H I✝ : C ⥤ D
I J K : D ⥤ E
α : F ⟶ G
β : G ⟶ H
γ : I ⟶ J
δ : J ⟶ K
⊢ (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ
aesop_cat