Add the walking coreflexive pair

[ScriptRaccoon]

This PR adds the walking coreflexive pair, the category generated by two morphisms $i,j : [0] \to [1]$ and a morphism $p: [1] \to [0]$ with $pi = pj = \mathrm{id}$. This is just the truncated simplex category $\Delta^{\leq 1}$.

This PR resolves (the dual of) #122. At first, I wanted to add the walking reflexive pair (#136), but while deciding its properties, it become more and more clear that its dual category is easier to handle and that we can recycle some arguments from the simplex category which already is in the database.

Interestingly, dualizing the proofs from #136 added two new unknown properties (I expected the same number). The first one, being multi-complete, could not be deduced because the property of being locally multi-presentable currently does not have a dual in the database. This is bad, we should always add duals from now on, since otherwise the deduction system is not "symmetric". The second one, being a generalized variety, was simply not visible for the walking reflexive pair since this property has no dual in the database. To be precise: the walking coreflexive pair does not have cosifted limits ( = the walking reflexive pair does not have sifted colimits), so that the walking coreflexive pair is not a "generalized covariety" ( = the walking reflexive pair is not a generalized variety). For the walking reflexive pair, this was already the end of the story, but not for the walking coreflexive pair. It is indeed a generalized variety, but that is somewhat non-trivial.

All properties for the walking coreflexive pair have been decided.