Require Import HFS.Extensionality.

Inductive R (X Y : HF) : X -> Y -> Prop :=
| R_empty : R 0 0
| R_adj a x b y : R a b -> R x y -> R (a@x) (b@y).

Section R.
  Variables X Y : HF.
  Implicit Types a x : X.
  Implicit Types b y : Y.

  Fact R_symm x y :
    R x y -> R y x.
  Proof.
    intros A; induction A; eauto using R.
  Qed.

  Fact R_total x :
    Sigma y, R x y.
  Proof.
    hf_induction x.
    - exists 0. constructor.
    - intros a x (b&IHa) (y&IHx).
      exists (b@y). now constructor.
  Qed.

  Lemma R_sim x y a:
    R x y -> a el x -> exists b, b el y /\ R a b.
  Proof.
    intros A. revert a.
    induction A as [|a' x' b' y' A _ _ IHx].
    - intros a [] % discrim.
    - intros a [->|B] % member.
      + exists b'. hfs.
      + destruct (IHx _ B) as (b&C&D). exists b. hfs.
  Qed.
End R.

Section R_functional.
  Variables X Y : HF.
  Implicit Types a x : X.
  Implicit Types b y : Y.

  Fact R_fun x y y' :
    R x y -> R x y' -> y = y'.
  Proof.
    revert y y'. epsilon_induction x. intros x IH y y' B C.
    extensio as b; split; intros D.
    - apply R_symm in B.
      destruct (R_sim B D) as (a&E&F).
      destruct (R_sim C E) as (b'&E'&F').
      enough (b = b') by congruence.
      apply R_symm in F. eauto.
    - apply R_symm in C.
      destruct (R_sim C D) as (a&E&F).
      destruct (R_sim B E) as (b'&E'&F').
      enough (b = b') by congruence.
      apply R_symm in F. eauto.
  Qed.
End R_functional.

Section Homo.
  Variables X Y : HF.
  Implicit Types a x : X.
  Implicit Types b y : Y.

  Definition homo (f: X -> Y) :=
    f eset = eset /\ forall a x, f (a@x) = f a @ f x.

  Lemma homo_R f x:
    homo f -> R x (f x).
  Proof.
    intros [A B].
    hf_induction x.
    - rewrite A. constructor.
    - intros a x IHa IHx. rewrite B. now constructor.
  Qed.

  Lemma homo_unique f g x:
    homo f -> homo g -> f x = g x.
  Proof.
    intros A % (homo_R x).
    intros B % (homo_R x).
    apply (R_fun A B).
  Qed.
End Homo.

Definition F (X Y : HF) : X -> Y := fun x => projT1 (R_total Y x).

Section F.
  Variables X Y: HF.
  Implicit Types a x : X.
  Implicit Types b y : Y.

  Fact F_cancel x :
    (F X (F Y x)) = x.
  Proof.
    unfold F.
    destruct (R_total Y x) as (y&A). cbn.
    destruct (R_total X y) as (x'&B). cbn.
    apply R_symm in A. apply (R_fun B A).
  Qed.

  Fact F_homo :
    homo (@F X Y).
  Proof.
    split.
    - unfold F. destruct (R_total Y 0) as [b A]. inv A; hfs.
    - intros a x. unfold F.
      destruct (R_total Y (a@x)) as (y&A),
               (R_total Y a) as (b&B),
               (R_total Y x) as (y'&C); cbn.
      assert (D: R (a@x) (b@y')) by now constructor.
      apply (R_fun A D).
  Qed.
End F.

Theorem categoricity (X Y: HF) :
  Sigma (f : X -> Y) (g : Y -> X),
  homo f /\ homo g /\ (forall x, g (f x) = x) /\ (forall y, f (g y) = y).
Proof.
  exists (F Y), (F X); auto using F_homo, F_cancel.
Qed.