Add functor properties: essentially injective / left-invertible

[ScriptRaccoon]

This PR adds two properties of functors $F$:

• $F$ is left-invertible: there is a functor $G$ with $G \circ F \cong \mathrm{id}$
• $F$ is essentially injective*: $F(X) \cong F(Y) \implies X \cong Y$

It is worth mentioning that it is undecidable in ZFC (cf. Easton's theorem) if the power set functor $P : Set \to Set$ is essentially injective; likewise for the contravariant version.

Apart from that, both properties have been decided for all functors in the database.

The two properties distinguish the free group functor from the monoid ring functor (which had the same properties before) as well as the countable copower functor from the doubling functor (dito).

This PR implements #234 in particular.

*Thank you @varkor for pointing out this terminology. Before, I had named this "reflects isomorphic objects".

[varkor]

Instead of "reflects isomorphic objects", how about essentially injective?

Instead of "left-invertible", how about "pseudo-section"? I think using "left" and "right" with respect to composition can be confusing, because some people prioritise traditional composition order and some people prioritise diagrammatic composition order in naming conventions, and so one has to always double-check which order is meant (whereas "section" is unambiguous).

[ScriptRaccoon]

Instead of "reflects isomorphic objects", how about essentially injective?

Thank you! I have adjusted the naming.

Instead of "left-invertible", how about "pseudo-section"? I think using "left" and "right" with respect to composition can be confusing, because some people prioritise traditional composition order and some people prioritise diagrammatic composition order in naming conventions, and so one has to always double-check which order is meant (whereas "section" is unambiguous).

I don't agree with this point.

The real problem is that mathematicians have not settled on conventions for even the most basic notions. The solution, in my view, is to adopt a convention and (yes, literally) ban every usage that conflicts with it. I really like this paper for example. I don't think that introducing terminology that tries to be agnostic about conventions solves the problem. It reduces the expressiveness of the language just to accommodate a small number of mathematicians who go against the norm.

As for composition order specifically, it is defined on the foundations page https://catdat.app/content/foundations and is already used consistently throughout CatDat. We already have the property left cancellative (https://catdat.app/category-property/left_cancellative), which generalizes the well-established notion of a left-cancellative monoid. Moreover, in algebra, left-invertible and left inverse are standard terms. It is natural to extend these notions to morphisms and, in particular, to functors.

Actually, if one regards the term "left invertible" as ambiguous (which I do not; see above), then exactly the same objection applies to the term "section". After all, when one writes $f \circ g = \mathrm{id}$, does this mean first $g$ and then $f$, or first $f$ and then $g$?

[varkor]

I disagree with several of your counterpoints, but I don't think it's a big enough issue to be worth pursuing. Let me just reply to this point:

exactly the same objection applies to the term "section"

Everyone uses the same convention for "section" and "retraction", regardless of the convention for composition; the terminology is not connected to the notation.