Various additions to functors

[ScriptRaccoon]

Features

1. On the functor list page /functors, show only tags that are actually used at least once.
2. Small text adjustment on functor detail page.
3. In generated proofs for functors using a functor implication, mention source and target assumptions if applicable.

New properties of functors

• fully faithful
• right-invertible
• reflector
• coreflector
• full on isomorphisms
• pseudomonic
• dominant
• preserves binary products
• preserves binary coproducts

The new properties have been decided for all functors.

At some stage, this PR also added the properties of lifting small (co)limits. But this was removed: it was the non-strict version, which is very close to preserving small limits (see commit history). In fact, it was equivalent to (co)continuous in all examples. It becomes only interesting if we add support for functor implications that allow conclusions about the categories, e.g. "if $C \to D$ lifts limits and $D$ is complete, then $C$ is complete". Also, before we add the strict version ("lifts small limits strictly"), which is not invariant under equivalences, we should first add the property "strictly monadic" since otherwise it will be a pain to associate the property to various forgetful functors.

New functors

• the forgetful functor from groups to pointed sets
• the indiscrete topology functor²
• the path components functor $\pi_0$

All properties of these new functors have been decided.

²It's interesting that currently it is undistinguishable from the forgetful functor from abelian groups to groups.

New implications

• In SAFT, replace "locally small" with "locally essentially small".
• A functor between pointed categories preserves initial objects iff it preserves terminal objects.
• A functor between semiadditive categories preserves finite coproducts iff it preserves finite products.
• ... and several implications for the new properties