no goals
ι : Type u_1
V : Type u
inst✝⁶ : Category V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
W : Type u_3
inst✝⁴ : Category W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
⊢ mapHomotopyCategory (α ≫ β) c = mapHomotopyCategory α c ≫ mapHomotopyCategory β c
aesop_cat