oops, shuffled some definitions Too Hard

intro.tt

@@ -1631,11 +1631,11 @@ EquivJ {X} P d {Y} e = subst {(Y : Type) * Equiv Y X} (\x -> P x.1 x.2) path d w
   path : Path {(Y : Type) * Equiv Y X} (X, the X, idEquiv {X}) (Y, e)
   path = isContr_isProp {(Y : Type) * Equiv Y X} contrSinglEquiv (X, the X, idEquiv {X}) (Y, e)
 
+pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
+pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A})
+
 uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B)
 uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where
-  pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
-  pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A})
-
   pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A})
   pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A})