diff --git a/library/hott/algebra/precategory/morphism.lean b/library/hott/algebra/precategory/morphism.lean
index b9a83bb09..6bda4626e 100644
--- a/library/hott/algebra/precategory/morphism.lean
+++ b/library/hott/algebra/precategory/morphism.lean
@@ -46,10 +46,6 @@ namespace morphism
   theorem id_is_iso [instance] : is_iso (ID a) :=
   is_iso.mk !id_compose !id_compose
 
-  -- In a precategory, equal objects are isomorphic
-  definition iso_of_path (p : a ≈ b) : Σ (f : hom a b), is_iso f :=
-  path.rec_on p ⟨ id , id_is_iso ⟩
-
   theorem inverse_is_iso [instance] (f : a ⟶ b) [H : is_iso f] : is_iso (f⁻¹) :=
   is_iso.mk !compose_inverse !inverse_compose
 
@@ -150,6 +146,10 @@ namespace morphism
   --is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
   end isomorphic
 
+  -- In a precategory, equal objects are isomorphic
+  definition iso_of_path (p : a ≈ b) : isomorphic a b :=
+  path.rec_on p (isomorphic.mk id)
+
   inductive is_mono [class] (f : a ⟶ b) : Type :=
   mk : (∀c (g h : hom c a), f ∘ g ≈ f ∘ h → g ≈ h) → is_mono f
   inductive is_epi  [class] (f : a ⟶ b) : Type :=