∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : MulZeroOneClass γ] [inst_3 : MulZeroOneClass δ] (f : α →*₀ β) (g : β →*₀ γ) (h : γ →*₀ δ),
  (h.comp g).comp f = h.comp (g.comp f)