From 0ed046ed806379e27c0326ab5bf9023200e87149 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Tue, 4 Nov 2014 09:49:07 -0500
Subject: [PATCH] fix(library/hott) fix funext.lean by making funext an
 instance

---
 library/hott/funext.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/library/hott/funext.lean b/library/hott/funext.lean
index 626fc8ef9..27904f06c 100644
--- a/library/hott/funext.lean
+++ b/library/hott/funext.lean
@@ -13,8 +13,12 @@ open path
 
 axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g)
 
+theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Π x : A, 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 :=
-  @IsEquiv.inv _ _ _ (funext 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 :=