Définition d'une application inversible

Bonjour ou bonsoir à tous.
Je me place dans ZFC.

Pour bien comprendre, voici mes définitions préliminaires, même si je pense que pour la plupart, voire toutes, vous avez les mêmes que moi. Je les mets juste au cas où vous vous posiez la question.

1- Étant donné deux ensembles $x$ et $y$, j'ai défini l'ensemble $(x;y)$ comme étant $\big\{\{x\};\{x;y\}\big\}$.
2 - Je dis qu'un ensemble $c$ est un couple si et seulement s'il existe deux ensembles $x$ et $y$ tels que $c=(x;y)$.
3 - Je dis qu'un ensemble $\mathcal{R}$ est une relation binaire si et seulement si tous ses éléments sont des couples. Pour $x$ et $y$ deux ensembles, je note $x\mathcal{R}y$ si et seulement si $(x;y)\in\mathcal{R}$.
4 - Étant donné une relation binaire $\mathcal{R}$, je note $\text{dom}(\mathcal{R})$ et $\text{im}(\mathcal{R})$ des ensembles que j'ai définis de sorte à avoir $\forall x,\big(x\in\text{dom}(\mathcal{R})\iff\exists y,x\mathcal{R}y\big)$ et $\forall y,\big(y\in\text{im}(\mathcal{R})\iff\exists x,x\mathcal{R}y\big)$.
5 - Je dis qu'une relation binaire $f$ est une application si et seulement si $\forall x,\forall y,\forall y',\Big(\big(xfy\text{ et }xfy'\big)\implies y=y'\Big)$.

C'est à partir d'ici je pense que la racine du problème va se cacher.
6 - Étant donné une application $f$, et deux ensembles $E$ et $F$, je dis que $f$ est une application de $E$ dans $F$, et je note $f:E\to F$, si et seulement si $\text{dom}(f)=E$ et $\text{im}(f)\subseteq F$.
Cette définition est un peu "asymétrique" : pour le domaine je demande spécifiquement que $E$ en soit le domaine, alors que je demande juste à $F$ d'être un sur-ensemble de l'image. C'est notamment dans l'optique plus tard de pouvoir dire qu'une suite réelle est aussi une suite complexe sans avoir à sourciller ou à faire quoi que ce soit. C'est peut-être contestable, mais j'ai trouvé cette définition très adaptée. Au contraire que ça soit défini partout sur l'ensemble de départ me semble primordial, d'où ce choix, mais peut-être que vous y trouverez quelque chose à dire.

7 - J'ai défini la composition de deux relations binaires $\mathcal{R}$ et $\mathcal{S}$ comme étant une relation telle que $\forall x,\forall z,\Big(x(\mathcal{S}\circ\mathcal{R})z\iff\exists z,\big(x\mathcal{R}y\text{ et }y\mathcal{S}\big)\Big)$. Je précise que c'est réalisable peu importe quelles relations sont $\mathcal{R}$ et $\mathcal{S}$ : leur composition est toujours possible.
8 - Étant donné un ensemble $E$, j'ai défini l'identité sur $E$ comme étant la relation $\{(x;y)\in E^{2}|x=y\}$, et j'ai montré plus tard que c'était même une application.

Voici alors où se situe mon questionnement : étant donné une application $f$, comment définir le fait que c'est inversible à gauche, et inversible à droite.

Initialement, j'étais parti ainsi : on suppose que $f:E\to F$ avec $E$ et $F$ deux ensembles.
a) Je que $f$ est inversible à gauche si et seulement s'il existe une application $g$ telle que $g\circ f=\text{id}_{E}$. Je dis alors que $g$ est une inverse à gauche de $f$.
b) Je dis que $f$ est inversible à droite depuis $F$ si et seulement s'il existe une application $h$ telle que $f\circ h=\text{id}_{F}$. Je dis alors que $h$ est une inverse à droite depuis $F$.

Vous voyez déjà là une asymétrie entre gauche et droite, causée par ma définition de "aller de $E$ dans $F$" puisque pour l'inversibilité à gauche, je prends forcément le domaine pour l'ensemble de l'identité, et pour l'inversibilité à droite je ne prends qu'un sur-ensemble de l'image.

Mais j'avais aussi pensé qu'une définition plus générale pourrait être intéressante : je prends $f$ une application.
a') Étant donné un ensemble $A$, je dis que $f$ est inversible à gauche dans $A$ si et seulement s'il existe une application $g$ telle que $g\circ f=\text{id}_{A}$. Je dis alors que $g$ est une inverse à gauche de $f$ dans $A$.
b') Etant donné un ensemble $B$, je dis que $f$ est inversible à droite depuis $B$ si et seulement s'il existe une application $h$ telle que $f\circ h=\text{id}_{B}$. Je dis alors que $h$ est une inverse à droite de $f$ depuis $B$.

Ici je crois que c'est très général et assez satisfaisant dans un certain sens, car on a défini ça pour tous ensembles $A$ et $B$ quelconques, et ce n'est même plus asymétrique, en tout cas a priori.
Mais ces définitions, si elles ont l'avantage d'être générales, font capturer dans notre filets beaucoup d'applications un peu "inutiles en pratique".
C'est pourquoi on pourrait restreindre les définitions (que ça soit a) et b), ou a') et b')) afin de rendre unique les inverses, ou encore les rendre de telle sorte que l'inversibilité à gauche soit équivalente à l'injectivité par exemple (ou au fait que la relation réciproque soit une application, ce genre de choses).

Ma question est de savoir ce que selon-vous il est le plus pertinent de prendre pour la pratique ?

Merci d'avoir pris le temps de lire tout cela !