Add property: has trivial split monos #383

The property that every split monomorphism is an isomorphism appears already implicitly in several places. It should be added separately.

It has been mentioned in comments to the implications right_cancellative_kernel_pairs and trivial_coreflexive_equalizer_preservation and thin_dominant_functor. But there are more places that can be refactored.

The property is self-dual, so maybe it is better to choose a name that reflects this. Maybe "splitting-trivial"?

I think it is also equivalent to the property that every split idempotent endomorphism is the identity.