Add powers and copowers

[ScriptRaccoon]

While working on #32 it became clear that it is useful to refine the existence of products even more by using powers, in all sorts of sizes.

In particular, we have the following little lemma: If a cartesian closed category has countable copowers, then it has countable powers. In fact, $X^I$ is $[I \otimes 1, X]$. This can be used to prove that certain categories are not cartesian closed, for example the category of manifolds and the category of schemes.

What has been done in detail:

• Add new properties: powers, countable powers, finite powers, binary powers (squares)
• Add new properties: copowers, countable copowers, finite copowers, binary copowers (doubles)
• Add obvious implications for the new properties
• Refine an existing implication that did only need (co)powers (codiagonal-no-mono)
• Add result: cartesian closed + countable copowers => countable products
• Add result: cartesian closed + copowers => products
• Decide the properties for most categories (the rest will be done in Fill reasons #32)
• Refine existing property assignments (for example, the non-existence of products was almost always caused by the non-existence of powers!)
• Fix some typos