linkfix

add functoriality of gloopn'

refactor: use notation for trunc_index

rename nondep to constant

fix two errors in the hott library

reverse sigma_assoc_equiv, and add variant

make instances in sigma explicit

small additions to group theory

move files from Spectral

move more results and make arguments explicit

homomorphisms of abelian groups form an abelian group

use psquare for naturality squares consistently

remove connectivity requirement for elimination out of an K(G,n)

various cleanup changes in library

backport some changes from lean 3