Homotopy linear algebra

arXiv:1602.05082 [math.CT]By homotopy linear algebra we mean the study of linear functors between slices of the 8-category of 8-groupoids, subject to certain finiteness conditions. After some standard definitions and results, we assemble said slices into 8-categories to model the duality between vector spaces and profinite-dimensional vector spaces, and set up a global notion of homotopy cardinality \`a la Baez-Hoffnung-Walker compatible with this duality. We needed these results to support our work on incidence algebras and M