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

fix(init.datatypes): make empty live in Type.{0}

Browse source
This commit is contained in:
Floris van Doorn 2015-05-05 18:05:07 -04:00 committed by Leonardo de Moura
parent 90f1a691fd
commit e5241f84ec
6 changed files with 7 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/hit/sphere.hlean
View file

@ -40,7 +40,7 @@ namespace sphere_index
definition add (n m : sphere_index) : sphere_index := definition add (n m : sphere_index) : sphere_index :=
sphere_index.rec_on m n (λ k l, l .+1) sphere_index.rec_on m n (λ k l, l .+1)
definition leq (n m : sphere_index) : Type₁ := definition leq (n m : sphere_index) : Type₀ :=
sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
infix `+1+`:65 := sphere_index.add infix `+1+`:65 := sphere_index.add

2
hott/init/datatypes.hlean
View file

@ -19,7 +19,7 @@ notation `Type₃` := Type.{3}
inductive unit.{l} : Type.{l} := inductive unit.{l} : Type.{l} :=
star : unit star : unit
inductive empty.{l} : Type.{l} inductive empty : Type₀
inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} := inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
refl : eq a a refl : eq a a

2
hott/init/logic.hlean
View file

@ -11,7 +11,7 @@ import init.reserved_notation
/- not -/ /- not -/
definition not.{l} (a : Type.{l}) := a → empty.{l} definition not (a : Type) := a → empty
prefix `¬` := not prefix `¬` := not
definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b := definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b :=

4
hott/init/trunc.hlean
View file

@ -20,7 +20,7 @@ namespace is_trunc
/- Truncation levels -/ /- Truncation levels -/
inductive trunc_index : Type₁ := inductive trunc_index : Type₀ :=
| minus_two : trunc_index | minus_two : trunc_index
| succ : trunc_index → trunc_index | succ : trunc_index → trunc_index
@ -38,7 +38,7 @@ namespace is_trunc
definition add (n m : trunc_index) : trunc_index := definition add (n m : trunc_index) : trunc_index :=
trunc_index.rec_on m n (λ k l, l .+1) trunc_index.rec_on m n (λ k l, l .+1)
definition leq (n m : trunc_index) : Type₁ := definition leq (n m : trunc_index) : Type₀ :=
trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
end trunc_index end trunc_index

2
hott/init/types.hlean
View file

@ -191,7 +191,7 @@ iff.intro (assume H, pr1 H) (assume H, pair H star)
definition unit_prod (a : Type) : unit × a ↔ a := definition unit_prod (a : Type) : unit × a ↔ a :=
iff.intro (assume H, pr2 H) (assume H, pair star H) iff.intro (assume H, pr2 H) (assume H, pair star H)
definition prod_empty.{l} (a : Type.{l}) : a × empty.{l} ↔ empty.{l} := definition prod_empty (a : Type) : a × empty ↔ empty :=
iff.intro (assume H, pr2 H) (assume H, !empty.elim H) iff.intro (assume H, pr2 H) (assume H, !empty.elim H)
definition empty_prod (a : Type) : empty × a ↔ empty := definition empty_prod (a : Type) : empty × a ↔ empty :=

10
hott/types/hprop_trunc.hlean
View file

@ -46,15 +46,7 @@ namespace is_trunc
{ apply equiv.to_is_equiv, apply is_contr.sigma_char}, { apply equiv.to_is_equiv, apply is_contr.sigma_char},
apply (@is_hprop.mk), intros, apply (@is_hprop.mk), intros,
fapply sigma_eq, {apply x.2}, fapply sigma_eq, {apply x.2},
apply (@is_hprop.elim), apply (@is_hprop.elim)},
apply is_trunc_pi, intro a,
apply is_hprop.mk, intro w z,
have H : is_hset A,
begin
apply is_trunc_succ, apply is_trunc_succ,
apply is_contr.mk, exact y.2
end,
fapply (@is_hset.elim A _ _ _ w z)},
{ intro n' IH A, { intro n' IH A,
apply is_trunc_is_equiv_closed, apply is_trunc_is_equiv_closed,
apply equiv.to_is_equiv, apply equiv.to_is_equiv,