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

Fix bug

Browse source
This commit is contained in:
Yuri Sulyma 2017-06-08 14:03:29 -06:00
parent 7f637206a0
commit a3146d0d2a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
move_to_lib.hlean
View file

@ -1,6 +1,6 @@
-- definitions, theorems and attributes which should be moved to files in the HoTT library -- definitions, theorems and attributes which should be moved to files in the HoTT library
import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 homotopy.smash_adjoint import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 .homotopy.smash_adjoint
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
is_trunc function sphere unit sum prod bool is_trunc function sphere unit sum prod bool