Excellent job Lawrence,
This essay is well-written and presents a Tour de Force of interesting Maths relevant to Physics. You have managed to work in a lot of topics that are very interesting to me, and about which I have much to learn, such as Homotopy Type Theory. The HoTT program is especially interesting to me, as it has a constructive geometric basis on the one hand, and a rigorous analytic procedure on the other. I also like that you wove in the Bott periodicity, which I was trying to find a way to fit into my own essay, because it is one of those invariant structures that one seems to bump into - as though it was there before you found it.
Being a constructivist, I think that perhaps numbers and counting are not the first Maths to arise, however. Having a Set of objects requires preexisting elements of geometric topology, so that objects with surfaces and containers to hold them are well-defined. Also, it is seen in young children that a sense of greater and lesser quantity is a kind of numeracy that exists apart from counting itself, and develops sooner. I would think that just as ontogeny recapitulates phylogeny, for developing organisms; so individual patterns of learning are reflected in the development of cultures. Perhaps counting is merely the earliest form of mathematical reckoning that could be written down.
I think you come out on the side of the formalists and logicists in the Brouwer Hilbert debate, while I am firmly in the intuitionist camp - and while this is sometimes termed anti-realist, I believe it is more realistic yo imagine that everything should be constructable for Physics. But at least you mention that there is a debate about this among mathematicians, which some might miss otherwise. It was a great effort overall, and you get high marks from me.
Regards,
Jonathan