fix(tests): adjust tests to reflect changes in the HoTT library

This commit is contained in:
Leonardo de Moura 2015-04-29 10:15:13 -07:00
parent 297d50378d
commit d1cb0018c0
7 changed files with 20 additions and 21 deletions

View file

@ -1,4 +1,4 @@
import algebra.precategory.basic import algebra.category
open category open category

View file

@ -24,11 +24,11 @@ namespace pi
/- Now we show how these things compute. -/ /- Now we show how these things compute. -/
definition apD10_path_pi (H : funext) (h : f g) : apD10 (eq_of_homotopy h) h := definition apd10_path_pi (H : funext) (h : f g) : apd10 (eq_of_homotopy h) h :=
apD10 (retr apD10 h) apd10 (right_inv apd10 h)
definition path_pi_eta (H : funext) (p : f = g) : eq_of_homotopy (apD10 p) = p := definition path_pi_eta (H : funext) (p : f = g) : eq_of_homotopy (apd10 p) = p :=
sect apD10 p left_inv apd10 p
print classes print classes
@ -38,11 +38,11 @@ namespace pi
/- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/ /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
definition path_equiv_homotopy (H : funext) (f g : Πx, B x) : (f = g) ≃ (f g) := definition path_equiv_homotopy (H : funext) (f g : Πx, B x) : (f = g) ≃ (f g) :=
equiv.mk _ !is_equiv_apD equiv.mk _ !is_equiv_apd
definition is_equiv_path_pi [instance] (H : funext) (f g : Πx, B x) definition is_equiv_path_pi [instance] (H : funext) (f g : Πx, B x)
: is_equiv (@eq_of_homotopy _ _ f g) := : is_equiv (@eq_of_homotopy _ _ f g) :=
is_equiv_inv apD10 is_equiv_inv apd10
definition homotopy_equiv_path (H : funext) (f g : Πx, B x) : (f g) ≃ (f = g) := definition homotopy_equiv_path (H : funext) (f g : Πx, B x) : (f g) ≃ (f = g) :=
equiv.mk _ (is_equiv_path_pi H f g) equiv.mk _ (is_equiv_path_pi H f g)
@ -51,7 +51,7 @@ namespace pi
protected definition transport (p : a = a') (f : Π(b : B a), C a b) protected definition transport (p : a = a') (f : Π(b : B a), C a b)
: (transport (λa, Π(b : B a), C a b) p f) : (transport (λa, Π(b : B a), C a b) p f)
(λb, transport (C a') !tr_inv_tr (transportD _ _ p _ (f (p⁻¹ ▹ b)))) := (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▹ b)))) :=
eq.rec_on p (λx, idp) eq.rec_on p (λx, idp)
/- A special case of [transport_pi] where the type [B] does not depend on [A], /- A special case of [transport_pi] where the type [B] does not depend on [A],
@ -102,7 +102,7 @@ namespace pi
: is_equiv (functor_pi f0 f1) := : is_equiv (functor_pi f0 f1) :=
begin begin
apply (adjointify (functor_pi f0 f1) (functor_pi (f0⁻¹) apply (adjointify (functor_pi f0 f1) (functor_pi (f0⁻¹)
(λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))), (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
intro h, apply eq_of_homotopy, intro h, apply eq_of_homotopy,
esimp [functor_pi, function.compose], -- simplify (and unfold function_pi and function.compose) esimp [functor_pi, function.compose], -- simplify (and unfold function_pi and function.compose)
--first subgoal --first subgoal
@ -110,13 +110,13 @@ namespace pi
rewrite adj, rewrite adj,
rewrite -transport_compose, rewrite -transport_compose,
rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _), rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
rewrite (retr (f1 _) _), rewrite (right_inv (f1 _) _),
apply apD, apply apd,
intro h, beta, intro h, beta,
apply eq_of_homotopy, intro a, esimp, apply eq_of_homotopy, intro a, esimp,
apply (transport_V (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)), apply (transport_V (λx, right_inv f0 a ▹ x = h a) (left_inv (f1 _) _)),
esimp [function.id], esimp [function.id],
apply apD apply apd
end end
end pi end pi

View file

@ -1,4 +1,4 @@
import algebra.group algebra.precategory.basic import algebra.group algebra.category
open eq sigma unit category path_algebra open eq sigma unit category path_algebra

View file

@ -1,4 +1,4 @@
import algebra.groupoid algebra.group import algebra.group algebra.category
open eq sigma unit category path_algebra equiv open eq sigma unit category path_algebra equiv

View file

@ -1,4 +1,4 @@
import algebra.precategory.basic import algebra.category
open category open category

View file

@ -1,4 +1,4 @@
import init.axioms.ua import init.ua
open nat unit equiv is_trunc open nat unit equiv is_trunc
inductive vector (A : Type) : nat → Type := inductive vector (A : Type) : nat → Type :=

View file

@ -17,8 +17,7 @@ definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f 2 g) : f = g :=
eq_of_homotopy (λa, eq_of_homotopy (H a)) eq_of_homotopy (λa, eq_of_homotopy (H a))
definition apD100 {f g : Πa b, C a b} (p : f = g) : f 2 g := definition apD100 {f g : Πa b, C a b} (p : f = g) : f 2 g :=
λa b, apD10 (apD10 p a) b λa b, apd10 (apd10 p a) b
local attribute eq_of_homotopy [reducible] local attribute eq_of_homotopy [reducible]
@ -26,8 +25,8 @@ definition foo (f g : Πa b, C a b) (H : f 2 g) (a : A)
: apD100 (eq_of_homotopy2 H) a = H a := : apD100 (eq_of_homotopy2 H) a = H a :=
begin begin
esimp [apD100, eq_of_homotopy2, eq_of_homotopy], esimp [apD100, eq_of_homotopy2, eq_of_homotopy],
rewrite (retr apD10 (λ(a : A), eq_of_homotopy (H a))), rewrite (right_inv apd10 (λ(a : A), eq_of_homotopy (H a))),
apply (retr apD10) apply (right_inv apd10)
end end
end hide end hide