Smash products - symmetric monoidal structure

[aljungstrom]

This PR contains

1. A formalisation of symmetric monoidal precategories (mainly copy-pasted from other files in the library). Mainly done to wrap up the main result in a neat way. (I don't know much about this part of the library, so I'm open to suggestions if there's a better way of phrasing things)
2. A proof that the universe of pointed types is symmetric monoidal with the smash product as product

[mortberg]

Looks good to me modulo conflicts. Please fix then I'll merge

A question: could the precategory notions be used for the proofs of category stuff? Like prefunctor for functor, etc. Seems like there is some code duplication otherwise?

[felixwellen]

A question: could the precategory notions be used for the proofs of category stuff?

That works for a surprising amount of stuff. I think the 'right' way to do it is to prove what we can on the level of wild categories (which, I think, we don't have yet). That seems to have worked very well for coq-hott...

I'm not suggesting any of that should be done now, just using the opportunity to point something out.

[aljungstrom]

@mortberg done. And yeah, I agree that a lot of the cat stuff should be done for precats (which we should probably rename to wild categories or something) first. In the future maybe... (I never work with the category part of the library, so I'm probably not the right person to change this)

[mortberg]

@mortberg done. And yeah, I agree that a lot of the cat stuff should be done for precats (which we should probably rename to wild categories or something) first. In the future maybe... (I never work with the category part of the library, so I'm probably not the right person to change this)

I can open an issue about it so that we don't forget. I'll merge this now