Add various examples of functors to witness property combinations

[ScriptRaccoon]

This PR adds various examples of functors that satisfy some property P, but not some other property Q. That is, they are witnesses of combinations of functor properties of the form P ∧ ¬ Q.

Before this PR, there were 99 consistent combinations of functor properties without witnesses (listed on the page /missing). After this PR, 87 remain.

This PR also adds support for functor implications that have no functor assumptions, only category assumptions. Various implications of this type are added. For example, a functor whose domain is a groupoid is automatically conservative, and a functor whose codomain is trivial is automatically continuous.

Concretely, the following functors have been added:

1. the simple-group probing functor* $Grp \to Set$ which is a kind of large product of representable functors
2. the trivial functor $BG \to 1$
3. the trivial functor $Idem \to 1$
4. the "endpoint" inclusion functor from the discrete category $\{0,2\}$ to the walking span $\{1 \leftarrow 0 \rightarrow 2\}$

All of their properties have been decided.

*no official name, this is just my choice

They are witnesses of the following 12 combinations:

combination	witnesses
continuous ∧ ¬ right adjoint	functors 1, 2, 3, 4
cocontinuous ∧ ¬ left adjoint	functors 2, 3, 4
conservative ∧ ¬ faithful	functor 2
essentially injective ∧ ¬ conservative	functor 3
essentially injective ∧ ¬ faithful	functors 2, 3
full on isomorphisms ∧ ¬ conservative	functor 3
full on isomorphisms ∧ ¬ faithful	functors 2, 3
full on isomorphisms ∧ ¬ fully faithful	functors 2, 3
full on isomorphisms ∧ ¬ left-invertible	functors 2, 3, 4
full on isomorphisms ∧ ¬ pseudomonic	functors 2, 3
fully faithful ∧ ¬ left-invertible	functor 4
pseudomonic ∧ ¬ left-invertible	functor 4