表明单数（内射）和史诗（外射）函数的Coq值具有反函数

Question

A monic和epic函数是isomorphism，因此它具有inverse。我想在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.

我在网上找到的证明（1，2）没有给出f'的构造（反之）。有可能在Coq中显示吗？ （对我来说，逆数是可计算的……）

Answer 1

首先是术语问题。在范畴论中，同构是具有左右逆的同构，因此我会稍微更改您的定义：

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.

[可以通过假设一些标准公理来证明这一结果，即命题可扩展性和构造性确定描述（又称唯一选择公理）：

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.

我相信，至少没有某种形式的独特选择，不可能证明这一结果。假设命题和功能的可扩展性。注意，如果exists! x : A, P x成立，则唯一函数

{x | P x} -> unit

既是单射的又是单射的。 （内射性来自唯一性部分，外射性来自存在性部分。）如果此函数对每个P : A -> Type都有一个逆，那么我们可以使用该逆来实现唯一选择的公理。由于该公理不存在于Coq中，因此在基本理论中不可能建立这种逆。