diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean
index cd31e8eb8..ed91dbe52 100644
--- a/library/hott/axioms/ua.lean
+++ b/library/hott/axioms/ua.lean
@@ -5,6 +5,7 @@
 import hott.path hott.equiv
 open path Equiv
 
+--Ensure that the types compared are in the same universe
 universe l
 variables (A B : Type.{l})
 
@@ -16,7 +17,21 @@ definition equiv_path (H : A ≈ B) : A ≃ B :=
 
 axiom ua_equiv (A B : Type) : IsEquiv (equiv_path A B)
 
+-- Make the Equivalence given by the axiom an instance
 definition ua_inst [instance] {A B : Type} := (@ua_equiv A B)
 
-definition ua {A B : Type} (H : A ≃ B) : A ≈ B :=
-  IsEquiv.inv (@equiv_path A B) H
+-- This is the version of univalence axiom we will probably use most often
+definition ua {A B : Type} : A ≃ B →  A ≈ B :=
+  IsEquiv.inv (@equiv_path A B)
+
+-- One consequence of UA is that we can transport along equivalencies of types
+namespace Equiv
+
+  protected definition subst (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
+      : P A → P B :=
+    path.transport P (ua H)
+
+  -- We can use this for calculation evironments
+  calc_subst subst
+
+end Equiv