I have been stuck on this problem for a couple days.
We know that every set theoretic injections have a left inverse: $$\forall x,y(f(x)=f(y)\implies x=y)$$
Iff ... $$\exists g:\text{im}(f)\to\text{dom}(f)\forall x(g\circ f(x)=x)$$
I have been trying to prove the same for second-order "injections".
$$\forall x,y(Fx=Fy\implies x=y)$$
Iff
$$\exists_FG\forall x(GFx=x)$$
Briefly, my tools are ...
Axiom of Choice $$\forall_PP(\forall x\exists yPxy\implies \exists_FF\forall xPxFx)$$
Theorem: Partial Function $$\forall_P P,Q(\forall x(Px\implies \exists yQxy)\implies\exists_FF \forall x(Px\implies QxFx))$$
Theorem: Unique Function $$\forall_PP(\forall x\exists! yPxy\implies\exists!_FF\forall xPxFx)$$
Theorem: Surjection iff Right Inverse $$\forall_FF(\forall x\exists y(Fy=x)\iff\exists_F G\forall x(FGx=x))$$
Axiom of Comprehension $$\exists_PP\forall\langle x\rangle_n(P^n\langle x\rangle_n\iff\Phi\langle x\rangle_n)$$
Where $\Phi$ is any formula and $\langle x\rangle_n$ is $n$ variables.
In addition, all first-order with equality axioms are theorems.
This is for my personal study, so there is no guarantee that this is proveable.
But there is so little study into second-order logic, I think any answer would be appreciated by many.
My Attempts at a Proof
Assumption: $$Fx=Fy\implies x=y$$
I know by first-order logic that there is some c for any arbitrary variable x: $$x=c$$
Therefore, by consequent's conditional: $$Fx=y\implies x=c$$
By comprehension we can define a predicate from here: $$Pyz$$
Existential generalization $$\exists zPyz$$
Universal generalization on $y$ $$\forall y\exists zPyz$$
We can use choice now: $$\exists_FG\forall yPyGy$$
And convert it back to a formula: $$\forall y(Fx=y\implies x=Gy)$$
Now choose $y$ to be $Fx$: $$Fx=Fx\implies x=GFx$$
Therefore ... $$x=GFx$$
And
$$GFx=x$$
Now existential generalization ... $$\exists_FG(GFx=x)$$
Universal generalization... $$\forall x\exists_FG(GFx=x)$$
But NO! I need ... $$\exists_F G\forall x(GFx=x)$$
This is where I get stuck. I know I must use the assumption somehow but I don't know how.
I can prove: $$\forall x(\exists_y(Fy=x)\iff \exists!y(Fy=x))$$
And from here maybe(?) I can do something. But I don't know. I'm stuck.