no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
X Y : C
f : X ⟶ Y
⊢ f = eqToHom (_ : X = X) ≫ f ≫ eqToHom (_ : Y = Y)
simp only [Category.id_comp, eqToHom_refl, Category.comp_id]