Declare Scope mynat_scope.
Local Open Scope mynat_scope.
Set Printing Projections.

Inductive mynat : Set :=
  | zero : mynat
  | succ : mynat -> mynat.

Notation "0" := zero.
Notation "x `" := (succ x) (at level 5, left associativity, format "x `").

Fixpoint repeat {A : Type} (n : mynat) (f : A -> A) (x : A) : A :=
  match n with
  | 0 => x
  | n2` => f (repeat n2 f x)
  end.

Definition plus (a b : mynat) : mynat :=
  repeat b succ a.
Infix "+" := plus.

Definition fin (a : mynat) : Set :=
  repeat a (fun (x : Set) => x + unit)%type Empty_set.

Definition inv {A B : Type} (g : B -> A) (f : A -> B) : Prop :=
  forall x, g (f x) = x.

Record bij (A B : Type) : Type := make_bij {
  fw_map : A -> B;
  bw_map : B -> A;
  left_inv : inv bw_map fw_map;
  right_inv : inv fw_map bw_map;
}.
Arguments fw_map {A B}.
Arguments bw_map {A B}.
Arguments left_inv {A B}.
Arguments right_inv {A B}.

Definition size (A : Type) (a : mynat) : Prop :=
  inhabited (bij A (fin a)).

Definition bij_id (A : Type) : bij A A.
  exists
    (fun x => x)
    (fun y => y);
  intro x; trivial.
Defined.

Definition bij_rev {A B : Type} (f : bij A B) : bij B A.
  exists
    (f.(bw_map))
    (f.(fw_map)).
  - exact f.(right_inv).
  - exact f.(left_inv).
Defined.

Definition bij_comp {A B C : Type} (f : bij A B) (g : bij B C) : bij A C.
  exists
    (fun x => g.(fw_map) (f.(fw_map) x))
    (fun z => f.(bw_map) (g.(bw_map) z)).
  - intro x. repeat rewrite left_inv. trivial.
  - intro z. repeat rewrite right_inv. trivial.
Defined.

Theorem size_fin : forall a, size (fin a) a.
  intro a. split. exact (bij_id (fin a)).
Defined.

Definition injective {A B : Type} (f : A -> B) : Prop :=
  forall x y, f x = f y -> x = y.

Theorem injective_left_inv : forall {A B} (g : B -> A) (f : A -> B), inv g f -> injective f.
  intros A B f g H x y H2.
  rewrite <- (H x), <- (H y), H2.
  trivial.
Qed.

Definition drop_right {A B : Type} (x : A + B) (P : forall y, x <> inr y) : A :=
  match x with
  | inl y => fun H => y
  | inr y => fun H => False_rect A (P y H)
  end eq_refl.

Theorem drop_right_spec :
  forall {A B} (x : A + B) (P : forall y, x <> inr y), inl (drop_right x P) = x.
Proof.
  intros A B x P.
  unfold drop_right.
  destruct x as [y|y].
  - trivial.
  - pose (P y) as H.
    contradict H.
    trivial.
Qed.

Definition untangle_unit {A B : Type} (f : A + unit -> B + unit) (x : A) : B + unit :=
  match f (inl x) with
  | inl y => inl y
  | inr tt => f (inr tt)
  end.

Theorem untangle_unit_spec :
  forall {A B} (f : A + unit -> B + unit),
    injective f -> forall x y, untangle_unit f x <> inr y.
Proof.
  intros A B f H x [].
  unfold untangle_unit.
  destruct (f (inl x)) as [z|[]] eqn:E.
  - discriminate.
  - rewrite <- E.
    intro H2.
    apply H in H2.
    discriminate.
Qed.

Definition drop_unit {A B : Type} (f : A + unit -> B + unit) (P : injective f) (x : A) : B :=
  drop_right (untangle_unit f x) (untangle_unit_spec f P x).

Theorem inl_injective : forall {A} B (x y : A), (inl x : A + B) = inl y -> x = y.
  intros A B x y H.
  inversion H.
  trivial.
Qed.

Theorem drop_unit_inv :
  forall {A B} (f : A + unit -> B + unit) (g : B + unit -> A + unit) (PL : inv g f) (PR : inv f g),
    inv (drop_unit g (injective_left_inv f g PR)) (drop_unit f (injective_left_inv g f PL)).
Proof.
  intros A B f g PL PR x.
  set (HF := injective_left_inv g f PL).
  set (HG := injective_left_inv f g PR).
  apply (inl_injective unit).
  unfold drop_unit at 1, untangle_unit.
  simpl.
  rewrite drop_right_spec.
  destruct (g (inl (drop_unit f HF x))) as [z|[]] eqn:E;
    unfold drop_unit, untangle_unit in E;
    rewrite drop_right_spec in E;
    destruct (f (inl x)) as [y|[]] eqn:E2.
  - rewrite <- E, <- E2.
    apply PL.
  - rewrite PL in E.
    discriminate.
  - rewrite <- E2, PL in E.
    discriminate.
  - rewrite <- E2.
    apply PL.
Qed.

Definition bij_drop_unit {A B : Type} (f : bij (A + unit) (B + unit)) : bij A B.
  exists
    (drop_unit f.(fw_map) (injective_left_inv f.(bw_map) f.(fw_map) f.(left_inv)))
    (drop_unit f.(bw_map) (injective_left_inv f.(fw_map) f.(bw_map) f.(right_inv)));
  apply drop_unit_inv.
Defined.

Definition bij_sum_empty_r (A : Type) : bij (A + Empty_set) A.
  exists
    (sum_rect (fun _ => A) (fun x => x) (Empty_set_rect (fun _ => A)))
    inl;
  intro x; tauto.
Defined.

Definition bij_sum {A B C D : Type} (f : bij A B) (g : bij C D) : bij (A + C) (B + D).
  exists
    (sum_rect _ (fun a => inl (f.(fw_map) a)) (fun c => inr (g.(fw_map) c)))
    (sum_rect _ (fun b => inl (f.(bw_map) b)) (fun d => inr (g.(bw_map) d))).
  - intros [a|c]; simpl; rewrite left_inv; trivial.
  - intros [b|d]; simpl; rewrite right_inv; trivial.
Defined.

Definition bij_sum_assoc (A B C : Type) : (bij (A + (B + C)) ((A + B) + C))%type.
  exists
    (sum_rect _ (fun a => inl (inl a)) (sum_rect _ (fun b => inl (inr b)) (fun c => inr c)))
    (sum_rect _ (sum_rect _ (fun a => inl a) (fun b => inr (inl b))) (fun c => inr (inr c)));
  intro x; tauto.
Defined.

Fixpoint bij_plus (a b : mynat) : bij (fin a + fin b)%type (fin (a + b)) :=
  match b with
  | 0 => bij_sum_empty_r (fin a)
  | c` => 
      bij_comp
        (bij_sum_assoc (fin a) (fin c) unit)
        (bij_sum (bij_plus a c) (bij_id unit))
  end.

Theorem size_plus : forall A B a b, size A a -> size B b -> size (A + B)%type (a + b).
  intros A B a b [fa] [fb]. split.
  exact (bij_comp (bij_sum fa fb) (bij_plus a b)).
Qed.