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

rename pequiv.sigma_char_equiv' to pequiv.sigma_char_pmap

Browse source
This commit is contained in:
Ulrik Buchholtz 2018-01-26 18:15:32 +01:00
parent 3a09e743a2
commit f51dac9045
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
higher_groups.hlean
View file

@ -245,7 +245,7 @@ begin
apply @is_trunc_equiv_closed_rev _ _ (n + 1) (Grp_equiv n k), apply @is_trunc_equiv_closed_rev _ _ (n + 1) (Grp_equiv n k),
apply is_trunc_succ_intro, intros X Y, apply is_trunc_succ_intro, intros X Y,
apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y), apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y),
apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_equiv' X Y), apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_pmap X Y),
apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)), apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)),
apply is_trunc_pmap_of_is_conn X k.-2 (n.-1) (n + k) Y, apply is_trunc_pmap_of_is_conn X k.-2 (n.-1) (n + k) Y,
{ apply le_of_eq, exact (sub_one_add_plus_two_sub_one n k)⁻¹ ⬝ !add_plus_two_comm }, { apply le_of_eq, exact (sub_one_add_plus_two_sub_one n k)⁻¹ ⬝ !add_plus_two_comm },

2
move_to_lib.hlean
View file

@ -627,7 +627,7 @@ begin
refine !idp_con ⬝ _, reflexivity }, refine !idp_con ⬝ _, reflexivity },
end end
definition pequiv.sigma_char_equiv' [constructor] (X Y : Type*) : definition pequiv.sigma_char_pmap [constructor] (X Y : Type*) :
(X ≃* Y) ≃ Σ(f : X →* Y), is_equiv f := (X ≃* Y) ≃ Σ(f : X →* Y), is_equiv f :=
begin begin
fapply equiv.MK, fapply equiv.MK,