michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/hott) fix funext.lean to match equivalence notation

Browse source
This commit is contained in:
Jakob von Raumer 2014-10-23 00:30:17 -04:00 committed by Leonardo de Moura
parent abd5c574ad
commit f182299459
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/hott/funext.lean
View file

@ -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 :=