diff --git a/Cubical.Foundations.Isomorphism.html b/Cubical.Foundations.Isomorphism.html
index a69e7aa57f..e6d8d87421 100644
--- a/Cubical.Foundations.Isomorphism.html
+++ b/Cubical.Foundations.Isomorphism.html
@@ -218,4 +218,10 @@
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 _)