Injectivity, left inverses, and classical logic.

Classical.v

Definition injective {A B} (f : A -> B) := forall a1 a2, f a1 = f a2 -> a1 = a2.

Definition left_inverse {A B} (f : A -> B) :=
  exists g, forall a, g (f a) = a.

Definition f (P : Prop) (p : P + True) :=
match p with
| inl _ => inl I
| inr _ => inr I
end.

Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.

Lemma f_injective : forall P, injective (f P).
Proof.
  unfold injective, f.
  intros.
  destruct a1, a2; try discriminate.
  - apply f_equal, proof_irrelevance.
  - destruct t, t0. reflexivity.
Qed.

Theorem injective_left_inverse_iff_classical : forall P,
  (forall {A B} (f : A -> B), injective f -> left_inverse f) -> P \/ ~P.
Proof.
  unfold injective, left_inverse, not.
  intros.
  specialize (H _ _ (f P) (f_injective P)) as [g Hg].
  destruct (g (inl I)) eqn:H; auto.
  right.
  intros p.
  specialize (Hg (inl p)). simpl in Hg. rewrite Hg in H.
  congruence.
Qed.