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

chore(library/hott) cleanup

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-06 19:41:08 -05:00
parent f1cc0c4bd8
commit b8ec1a1649
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/hott/axioms/funext.lean
View file

@ -10,15 +10,15 @@ open path
-- Funext
-- ------
axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g)
axiom funext {A : Type} {P : A → Type} (f g : Πx, P x) : IsEquiv (@apD10 A P f g)
theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Π x : A, P x) :
theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Πx, 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 :=
definition path_forall {A : Type} {P : A → Type} (f g : Πx, P x) : f ∼ g → 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 :=
λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
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 :=
λE, path_forall f g (λx, path_forall (f x) (g x) (E x))

4
library/hott/axioms/ua.lean
View file

@ -1,6 +1,6 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad, Jakob von Raumer
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.path hott.equiv
open path Equiv