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

simplify definition of loop_ptrunc_maxm2_pequiv

Browse source
This commit is contained in:
Floris van Doorn 2017-06-30 15:29:52 +01:00
parent dce2832ead
commit 4ba4929cd7
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
homotopy/strunc.hlean
View file

@ -42,8 +42,8 @@ definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) :
begin begin
induction k with k k, induction k with k k,
{ exact loop_ptrunc_pequiv k X }, { exact loop_ptrunc_pequiv k X },
{ refine _ ⬝e* (pequiv_punit_of_is_contr _ !is_trunc_trunc)⁻¹ᵉ*, { refine pequiv_of_is_contr _ _ _ !is_trunc_trunc,
apply @loop_pequiv_punit_of_is_set, apply is_contr_loop,
cases k with k, cases k with k,
{ change is_set (trunc 0 X), apply _ }, { change is_set (trunc 0 X), apply _ },
{ change is_set (trunc -2 X), apply _ }} { change is_set (trunc -2 X), apply _ }}

3
pointed.hlean
View file

@ -195,6 +195,9 @@ namespace pointed
definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) := definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) :=
is_contr.mk idp (λa, !is_prop.elim) is_contr.mk idp (λa, !is_prop.elim)
definition pequiv_of_is_contr (A B : Type*) (HA : is_contr A) (HB : is_contr B) : A ≃* B :=
pequiv_punit_of_is_contr A _ ⬝e* (pequiv_punit_of_is_contr B _)⁻¹ᵉ*
definition loop_pequiv_punit_of_is_set (X : Type*) [is_set X] : Ω X ≃* punit := definition loop_pequiv_punit_of_is_set (X : Type*) [is_set X] : Ω X ≃* punit :=
pequiv_punit_of_is_contr _ (is_contr_loop X) pequiv_punit_of_is_contr _ (is_contr_loop X)