From 12429c93c83a801745cc2a446a830e566fc18b60 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Fri, 21 Nov 2014 18:04:02 -0500
Subject: [PATCH] fix(library/hott) fix equiv_precomp, doesn't look nice now

---
 library/hott/equiv_precomp.lean | 72 ++++++++++++++++-----------------
 1 file changed, 36 insertions(+), 36 deletions(-)

diff --git a/library/hott/equiv_precomp.lean b/library/hott/equiv_precomp.lean
index ae25b7e5d1..c5f2833e48 100644
--- a/library/hott/equiv_precomp.lean
+++ b/library/hott/equiv_precomp.lean
@@ -3,29 +3,30 @@
 -- Author: Jakob von Raumer
 -- Ported from Coq HoTT
 import hott.equiv hott.axioms.funext
-open path function
+open path function funext
+
+set_option pp.universes true
 
 namespace IsEquiv
   context
-  parameters {A B : Type} (f : A → B)
 
   --Precomposition of arbitrary functions with f
-  definition precomp (C : Type) (h : B → C) : A → C := h ∘ f
+  definition precomp {A B : Type} (f : A → B) (C : Type) (h : B → C) : A → C := h ∘ f
 
   --Postcomposition of arbitrary functions with f
-  definition postcomp (C : Type) (l : C → A) : C → B := f ∘ l
+  definition postcomp {A B : Type} (f : A → B) (C : Type) (l : C → A) : C → B := f ∘ l
 
   --Precomposing with an equivalence is an equivalence
-  definition precompose [instance] [Hf : IsEquiv f] (C : Type):
-      IsEquiv (precomp C) :=
-    adjointify (precomp C) (λh, h ∘ f⁻¹)
+  definition precompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : IsEquiv f] (C : Type):
+      IsEquiv (precomp f C) :=
+    adjointify (precomp f C) (λh, h ∘ f⁻¹)
       (λh, path_forall _ _ (λx, ap h (sect f x)))
       (λg, path_forall _ _ (λy, ap g (retr f y)))
 
   --Postcomposing with an equivalence is an equivalence
-  definition postcompose [instance] [Hf : IsEquiv f] (C : Type):
-      IsEquiv (postcomp C) :=
-    adjointify (postcomp C) (λl, f⁻¹ ∘ l)
+  definition postcompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : IsEquiv f] (C : Type):
+      IsEquiv (postcomp f C) :=
+    adjointify (postcomp f C) (λl, f⁻¹ ∘ l)
       (λh, path_forall _ _ (λx, retr f (h x)))
       (λg, path_forall _ _ (λy, sect f (g y)))
 
@@ -33,29 +34,30 @@ namespace IsEquiv
   --then that function is also an equivalence.  It's convenient to know
   --that we only need to assume the equivalence when the other type is
   --the domain or the codomain.
-  private definition isequiv_precompose_eq (C D : Type) (Ceq : IsEquiv (precomp C))
-      (Deq : IsEquiv (precomp D)) (k : C → D) (h : A → C) :
-      k ∘ (inv (precomp C)) h ≈ (inv (precomp D)) (k ∘ h) :=
-    let invD := inv (precomp D) in
-    let invC := inv (precomp C) in
+  protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type) (Ceq : IsEquiv (precomp f C))
+      (Deq : IsEquiv (precomp f D)) (k : C → D) (h : A → C) :
+      k ∘ (inv (precomp f C)) h ≈ (inv (precomp f D)) (k ∘ h) :=
+    let invD := inv (precomp f D) in
+    let invC := inv (precomp f C) in
     have eq1 : invD (k ∘ h) ≈ k ∘ (invC h),
-      from calc invD (k ∘ h) ≈ invD (k ∘ (precomp C (invC h))) : retr (precomp C) h
+      from calc invD (k ∘ h) ≈ invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h
 		... ≈ k ∘ (invC h) : !sect,
       eq1⁻¹
 
-  definition isequiv_precompose (Aeq : IsEquiv (precomp A))
-      (Beq : IsEquiv (precomp B)) : (IsEquiv f) :=
-    let invA := inv (precomp A) in
-    let invB := inv (precomp B) in
+  universe variable l
+  definition isequiv_precompose {A B : Type.{l}} (f : A → B) (Aeq : IsEquiv (precomp f A))
+      (Beq : IsEquiv (precomp f B)) : (IsEquiv f) :=
+    let invA := inv (precomp f A) in
+    let invB := inv (precomp f B) in
     let sect' : Sect (invA id) f := (λx,
       calc f (invA id x) ≈ (f ∘ invA id) x : idp
 	... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
-	... ≈ invB (precomp B id) x : idp
-	... ≈ x : apD10 (sect (precomp B) id))
+	... ≈ invB (precomp f B id) x : idp
+	... ≈ x : apD10 (sect (precomp f B) id))
       in
     let retr' : Sect f (invA id) := (λx,
-      calc invA id (f x) ≈ precomp A (invA id) x : idp
-	... ≈ x : apD10 (retr (precomp A) id)) in
+      calc invA id (f x) ≈ precomp f A (invA id) x : idp
+	... ≈ x : apD10 (retr (precomp f A) id)) in
     adjointify f (invA id) sect' retr'
 
   end
@@ -65,20 +67,18 @@ end IsEquiv
 --Bundled versions of the previous theorems
 namespace Equiv
 
-  context
-  parameters {A B C : Type} {eqf : A ≃ B}
-
-  private definition f := equiv_fun eqf
-  private definition Hf := equiv_isequiv eqf
-
-  definition precompose : (B → C) ≃ (A → C) :=
+  definition precompose [F : funext] {A B C : Type} {eqf : A ≃ B}
+      : (B → C) ≃ (A → C) :=
+    let f := equiv_fun eqf in
+    let Hf := equiv_isequiv eqf in
     Equiv.mk (IsEquiv.precomp f C)
-      (@IsEquiv.precompose A B f Hf C)
+      (@IsEquiv.precompose A B f F Hf C)
 
-  definition postcompose : (C → A) ≃ (C → B) :=
+  definition postcompose [F : funext] {A B C : Type} {eqf : A ≃ B}
+      : (C → A) ≃ (C → B) :=
+    let f := equiv_fun eqf in
+    let Hf := equiv_isequiv eqf in
     Equiv.mk (IsEquiv.postcomp f C)
-      (@IsEquiv.postcompose A B f Hf C)
-
-  end
+      (@IsEquiv.postcompose A B f F Hf C)
 
 end Equiv