diff --git a/library/hott/funext.lean b/library/hott/funext.lean index f204af9f0..081b1f347 100644 --- a/library/hott/funext.lean +++ b/library/hott/funext.lean @@ -14,7 +14,7 @@ open path axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g) definition path_forall {A : Type} {P : A → Type} (f g : Π x : A, P x) : f ∼ g → f ≈ g := -(funext f g)⁻¹ + IsEquiv.inv (funext f g) 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 :=