diff --git a/library/hott/axioms/funext.lean b/library/hott/axioms/funext.lean
index e89481782..9d45cc085 100644
--- a/library/hott/axioms/funext.lean
+++ b/library/hott/axioms/funext.lean
@@ -10,15 +10,15 @@ open path
 -- Funext
 -- ------
 
-axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g)
+axiom funext {A : Type} {P : A → Type} (f g : Πx, P x) : IsEquiv (@apD10 A P f g)
 
-theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Π x : A, P x) :
+theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Πx, P x) :
     IsEquiv (@apD10 A P f g) :=
   @funext A P f g
 
-definition path_forall {A : Type} {P : A → Type} (f g : Π x : A, P x) : f ∼ g → f ≈ g :=
+definition path_forall {A : Type} {P : A → Type} (f g : Πx, P x) : f ∼ g → f ≈ g :=
   IsEquiv.inv !apD10
 
-definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Π x y, P x y) :
-  (Πx y, f x y ≈ g x y) → f ≈ g :=
-λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
+definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Πx y, P x y) :
+    (Πx y, f x y ≈ g x y) → f ≈ g :=
+  λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean
index ed91dbe52..a486f7ca7 100644
--- a/library/hott/axioms/ua.lean
+++ b/library/hott/axioms/ua.lean
@@ -1,6 +1,6 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad, Jakob von Raumer
+-- Author: Jakob von Raumer
 -- Ported from Coq HoTT
 import hott.path hott.equiv
 open path Equiv