Add property "regular-subobject-trivial" and associated implications

[dschepler]

In proofs that came up for #243 it turned out it would be useful to add a property "regular-subobject-trivial" (and its dual) for implications such as:
regular subobject classifier + Malcev -> regular-subobject-trivial
thin -> regular-subobject-trivial
regular-subobject-trivial + equalizers -> thin
subobject-trivial <-> regular-subobject-trivial + mono-regular

[ScriptRaccoon]

"regular-subobject-trivial -> thin" is the other way round

[dschepler]

Oh, OK, I guess regular-subobject-trivial is actually equivalent to thin. (=>) The equalizer of any parallel pair is a regular monomorphism, so it's an isomorphism, so the parallel pair is equal. (<=) Any equalizer of a parallel pair, in a thin category, is an isomorphism.

I guess I could incorporate this into #243 then.

[ScriptRaccoon]

It is equivalent if equalizers exist.

[ScriptRaccoon]

More precisely, thin <==> equalizers + regular-subobject-trivial.