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

fix typo

Browse source
This commit is contained in:
Floris van Doorn 2017-01-25 12:14:20 -05:00
parent cde8333151
commit 216a25af4f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
homotopy/EM.hlean
View file

@ -262,7 +262,7 @@ namespace EM
(ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*,
apply ptrunc_elim_phomotopy,
refine _ ⬝* !psusp_elim_psusp_functor⁻¹*,
refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_mul_hom_EM_up eX rX) _ (@is_conn_loop _ _ H1)
refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1)
(@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)),
apply psusp_elim_natural }
end