From 2d9621892bace31156fbc9c830ac9ddec7ff14aa Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 20 Nov 2014 01:08:23 -0500
Subject: [PATCH] fix(library/hott) fill both gaps (I don't know why it works
 that way), change name from funext.apply to funext.ap, since apply seems to
 be a tactic name?

---
 library/hott/axioms/funext.lean    | 8 ++++----
 library/hott/axioms/ua.lean        | 5 ++---
 library/hott/funext_varieties.lean | 2 +-
 3 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/library/hott/axioms/funext.lean b/library/hott/axioms/funext.lean
index a17d79ff5..497cb71d2 100644
--- a/library/hott/axioms/funext.lean
+++ b/library/hott/axioms/funext.lean
@@ -14,7 +14,7 @@ set_option pp.universes true
 
 -- Define function extensionality as a type class
 inductive funext.{l} [class] : Type.{l+3} :=
-  mk : (Π {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Π x, P x), IsEquiv (@apD10 A P f g))
+  mk : (Π (A : Type.{l+1}) (P : A → Type.{l+2}) (f g : Π x, P x), IsEquiv (@apD10 A P f g))
          → funext.{l}
 
 namespace funext
@@ -23,11 +23,11 @@ namespace funext
     universe l
     parameters [F : funext.{l}] {A : Type.{l+1}} {P : A → Type.{l+2}} (f g : Π x, P x)
 
-    protected definition apply [instance] : IsEquiv (@apD10 A P f g) :=
-      rec_on F (λ H, sorry)
+    protected definition ap [instance] : IsEquiv (@apD10 A P f g) :=
+      rec_on F (λ (H : Π A P f g, _), !H)
 
     definition path_forall : f ∼ g → f ≈ g :=
-      @IsEquiv.inv _ _ (@apD10 A P f g) apply
+      @IsEquiv.inv _ _ (@apD10 A P f g) ap
 
   end
 
diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean
index 12439ebc4..fa3179006 100644
--- a/library/hott/axioms/ua.lean
+++ b/library/hott/axioms/ua.lean
@@ -5,7 +5,6 @@
 import hott.path hott.equiv
 open path Equiv
 
-set_option pp.universes true
 --Ensure that the types compared are in the same universe
 section
   universe variable l
@@ -29,8 +28,8 @@ namespace ua_type
     parameters [F : ua_type.{k}] {A B: Type.{k}}
 
     -- Make the Equivalence given by the axiom an instance
-    protected definition inst [instance] : IsEquiv (equiv_path A B) :=
-      rec_on F (λ H, sorry)
+    protected definition inst [instance] : IsEquiv (equiv_path.{k} A B) :=
+      rec_on F (λ H, H A B)
 
     -- This is the version of univalence axiom we will probably use most often
     definition ua : A ≃ B →  A ≈ B :=
diff --git a/library/hott/funext_varieties.lean b/library/hott/funext_varieties.lean
index c593f5934..6e1f05012 100644
--- a/library/hott/funext_varieties.lean
+++ b/library/hott/funext_varieties.lean
@@ -28,7 +28,7 @@ definition weak_funext.{l} :=
 definition funext_implies_naive_funext [F : funext] : naive_funext :=
   (λ A P f g h,
     have Fefg: IsEquiv (@apD10 A P f g),
-      from (@funext.apply F A P f g),
+      from (@funext.ap F A P f g),
     have eq1 : _, from (@IsEquiv.inv _ _ (@apD10 A P f g) Fefg h),
     eq1
   )