Show that a monic (injective) and epic (surjective) function has an inverse in Coq

Question

A monic and epic function is an isomorphism, hence it has an inverse. I'd like a proof of that in Coq.

  Axiom functional_extensionality: forall A B (f g : A->B),  (forall a, f a = g a) -> f = g.
  Definition compose {A B C} (f : B->C) (g: A->B) a := f (g a).
  Notation "f ∘ g" := (compose f g) (at level 40).
  Definition id {A} (a:A) := a.
  Definition monic {A B} (f:A->B) := forall C {h k:C->A}, f ∘ h = f ∘ k -> h = k.
  Definition epic  {A B} (f:A->B) := forall C {h k:B->C}, h ∘ f = k ∘ f -> h = k.
  Definition iso {A B} (f:A->B) := monic f /\ epic f.

  Goal forall {A B} (f:A->B), iso f -> exists f', f∘f' = id /\ f'∘f = id.

The proofs I have found online (1, 2) do not give a construction of f' (the inverse). Is it possible to show this in Coq? (It is not obvious to me that the inverse is computable...)

Answer 1

First, a question of terminology. In category theory, an isomorphism is a morphism that has a left and a right inverse, so I am changing slightly your definitions:

Definition compose {A B C} (f : B->C) (g: A->B) a := f (g a).
Notation "f ∘ g" := (compose f g) (at level 40).
Definition id {A} (a:A) := a.
Definition monic {A B} (f:A->B) := forall C {h k:C->A}, f ∘ h = f ∘ k -> h = k.
Definition epic  {A B} (f:A->B) := forall C {h k:B->C}, h ∘ f = k ∘ f -> h = k.
Definition iso {A B} (f:A->B) :=
  exists g : B -> A, f ∘ g = id /\ g ∘ f = id.

It is possible to prove this result by assuming a few standard axioms, namely propositional extensionality and constructive definite description (a.k.a. the axiom of unique choice):

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.PropExtensionality.
Require Import Coq.Logic.Description.

Section MonoEpiIso.

Context (A B : Type).

Implicit Types (f : A -> B) (x : A) (y : B).

Definition surjective f := forall y, exists x, f x = y.

Lemma epic_surjective f : epic f -> surjective f.
Proof.
intros epic_f y.
assert (H : (fun y => exists x, f x = y) = (fun y => True)).
{ apply epic_f.
  apply functional_extensionality.
  intros x; apply propositional_extensionality; split.
  - intros _; exact I.
  - now intros _; exists x. }
now pattern y; rewrite H.
Qed.

Definition injective f := forall x1 x2, f x1 = f x2 -> x1 = x2.

Lemma monic_injective f : monic f -> injective f.
Proof.
intros monic_f x1 x2 e.
assert (H : f ∘ (fun a : unit => x1) = f ∘ (fun a : unit => x2)).
{ now unfold compose; simpl; rewrite e. }
assert (e' := monic_f _ _ _ H).
exact (f_equal (fun g => g tt) e').
Qed.

Lemma monic_epic_iso f : monic f /\ epic f -> iso f.
Proof.
intros [monic_f epic_f].
assert (Hf : forall y, exists! x, f x = y).
{ intros y.
  assert (sur_f := epic_surjective _ epic_f).
  destruct (sur_f y) as [x xP].
  exists x; split; trivial.
  intros x' x'P.
  now apply (monic_injective _ monic_f); rewrite xP, x'P. }
exists (fun a => proj1_sig (constructive_definite_description _ (Hf a))).
split; apply functional_extensionality; unfold compose, id.
- intros y.
  now destruct (constructive_definite_description _ (Hf y)).
- intros x.
  destruct (constructive_definite_description _ (Hf (f x))); simpl.
  now apply (monic_injective _ monic_f).
Qed.

End MonoEpiIso.

I believe it is not possible to prove this result without at least some form of unique choice. Assume propositional and functional extensionality. Note that, if exists! x : A, P x holds, then the unique function

{x | P x} -> unit

is both injective and surjective. (Injectivity follows from the uniqueness part, and surjectivity follows from the existence part.) If this function had an inverse for every P : A -> Type, then we could use this inverse to implement the axiom of unique choice. Since this axiom does not hold in Coq, it shouldn't be possible to build this inverse in the basic theory.