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

feat(hott/types/equiv): add is_trunc_equiv to equiv.hlean

Browse source
This commit is contained in:
seulbaek 2016-01-19 13:20:18 -08:00 committed by Leonardo de Moura
parent aa5e188179
commit 2c81c93d69
1 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
hott/types/equiv.hlean
View file

@ -182,4 +182,21 @@ namespace equiv
apply is_hprop.elimo}
end
definition is_contr_equiv (A B : Type) [HA : is_contr A] [HB : is_contr B] : is_contr (A ≃ B) :=
begin
apply @is_contr_of_inhabited_hprop, apply is_hprop.mk,
intro x y, cases x with fx Hx, cases y with fy Hy, generalize Hy,
apply (eq_of_homotopy (λ a, !eq_of_is_contr)) ▸ (λ Hy, !is_hprop.elim ▸ rfl),
apply equiv_of_is_contr_of_is_contr
end
definition is_trunc_succ_equiv (n : trunc_index) (A B : Type)
[HA : is_trunc n.+1 A] [HB : is_trunc n.+1 B] : is_trunc n.+1 (A ≃ B) :=
@is_trunc_equiv_closed _ _ n.+1 (equiv.symm !equiv.sigma_char)
(@is_trunc_sigma _ _ _ _ (λ f, !is_trunc_succ_of_is_hprop))
definition is_trunc_equiv (n : trunc_index) (A B : Type)
[HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) :=
by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv
end equiv