∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ),
  (EquivFunctor.mapEquiv f ab).trans (EquivFunctor.mapEquiv f bc) = EquivFunctor.mapEquiv f (ab.trans bc)