Library ZFsum

Require Import ZFnats.
Require Import ZFpairs.
Import IZF.

Definition inl x := couple zero x.
Definition inr y := couple (succ zero) y.

Instance inl_morph : morph1 inl.
Qed.
Instance inr_morph : morph1 inr.
Qed.

Lemma discr_sum : forall x y, ~ inl x == inr y.

Lemma inl_inj : forall x y, inl x == inl y -> x == y.

Lemma inr_inj : forall x y, inr x == inr y -> x == y.

Definition sum X Y :=
  subset (prodcart N (union2 X Y))
    (fun p => (fst p == zero /\ snd p \in X) \/
              (fst p == succ zero /\ snd p \in Y)).

Instance sum_morph : morph2 sum.

Qed.

Lemma inl_typ : forall X Y x, x \in X -> inl x \in sum X Y.

Lemma inr_typ : forall X Y y, y \in Y -> inr y \in sum X Y.

Lemma sum_ind : forall X Y a (P:Prop),
  (forall x, x \in X -> a == inl x -> P) ->
  (forall y, y \in Y -> a == inr y -> P) ->
  a \in sum X Y -> P.

Lemma sum_mono : forall X X' Y Y',
  X \incl X' -> Y \incl Y' -> sum X Y \incl sum X' Y'.