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

fix(tests): update tests to reflect the change of notation from \~ to ~

Browse source
This commit is contained in:
Floris van Doorn 2015-06-25 22:55:05 -04:00
parent 24762fe843
commit 9ef1ae0848
4 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
tests/lean/hott/433.hlean
View file

@ -24,7 +24,7 @@ namespace pi
/- 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 (right_inv apd10 h)
definition path_pi_eta (H : funext) (p : f = g) : eq_of_homotopy (apd10 p) = p :=
@ -37,27 +37,27 @@ namespace pi
/- 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
definition is_equiv_path_pi [instance] (H : funext) (f g : Πx, B x)
: is_equiv (@eq_of_homotopy _ _ f g) :=
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)
/- Transport -/
protected definition transport (p : a = a') (f : Π(b : B a), C a b)
: (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)
/- A special case of [transport_pi] where the type [B] does not depend on [A],
and so it is just a fixed type [B]. -/
definition transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b)
: (eq.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, eq.transport (λa, C a b) p (f b)) :=
: (eq.transport (λa, Π(b : A'), C a b) p f) ~ (λb, eq.transport (λa, C a b) p (f b)) :=
eq.rec_on p (λx, idp)
/- Maps on paths -/

2
tests/lean/hott/calc_auto_trans_eq.hlean
View file

@ -1,6 +1,6 @@
constant list : Type → Type
constant R.{l} : Π {A : Type.{l}}, A → A → Type.{l}
infix `~`:50 := R
infix `~` := R
example {A : Type} {a b c d : list nat} (H₁ : a ~ b) (H₂ : b = c) (H₃ : c = d) : a ~ d :=
calc a ~ b : H₁

2
tests/lean/run/calc_auto_trans_eq.lean
View file

@ -1,6 +1,6 @@
import data.list
constant R : Π {A : Type}, A → A → Prop
infix `~`:50 := R
infix `~` := R
example {A : Type} {a b c d : list nat} (H₁ : a ~ b) (H₂ : b = c) (H₃ : c = d) : a ~ d :=
calc a ~ b : H₁

6
tests/lean/slow/path_groupoids.lean
View file

@ -197,12 +197,12 @@ definition ap01 := ap
definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
Πx : A, f x ≈ g x
infix `∼` := pointwise_paths
infix `~` := pointwise_paths
definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g :=
definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ~ g :=
λx, path.rec_on H idp
definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H
definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ~ g := apD10 H
definition ap11 {A B} {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y :=
path.rec_on H (path.rec_on p idp)