Added transportIsoToPath and transportIsoToPath⁻ (agda#1109)

* Added transportIsoToPath and transportIsoToPath⁻

* fixed whitespace

Author: oisdk

Cubical/Foundations/Isomorphism.agda

@@ -217,3 +217,9 @@ rightInv (Iso≡Set hA hB f g hfun hinv i) x j =
   isSet→isSet' hB (rightInv f x) (rightInv g x) (λ i → hfun (hinv x i) i) refl i j
 leftInv (Iso≡Set hA hB f g hfun hinv i) x j =
   isSet→isSet' hA (leftInv f x) (leftInv g x) (λ i → hinv (hfun x i) i) refl i j
+
+transportIsoToPath : (f : Iso A B) (x : A) → transport (isoToPath f) x ≡ f .fun x
+transportIsoToPath f x = transportRefl _
+
+transportIsoToPath⁻ : (f : Iso A B) (x : B) → transport (sym (isoToPath f)) x ≡ f .inv x
+transportIsoToPath⁻ f x = cong (f .inv) (transportRefl _)