no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
E : Type u₃
inst✝ : Category E
F G : C ⥤ D
α : F ≅ G
X : C
Z : D
g g' : F.obj X ⟶ Z
⊢ α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'
simp only [cancel_epi, refl]