Library ZFsum

Require Import ZFnats.
Require Import ZFpairs.

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

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

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

Lemma dest_sum_inl : ∀ x, dest_sum (inl x) == x.

Lemma dest_sum_inr : ∀ y, dest_sum (inr y) == y.

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

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

Definition sum X Y :=
  prodcart (singl zero) X ∪ prodcart (singl (succ zero)) Y.

Instance sum_morph : morph2 sum.
Qed.

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

Lemma inl_typ : ∀ X Y x, x ∈ X -> inl x ∈ sum X Y.

Lemma inr_typ : ∀ X Y y, y ∈ Y -> inr y ∈ sum X Y.

Lemma sum_mono : ∀ X X' Y Y',
  X ⊆ X' -> Y ⊆ Y' -> sum X Y ⊆ sum X' Y'.

  Definition sum_case f g x :=
    cond_set (fst x == zero) (f (dest_sum x)) ∪
    cond_set (fst x == succ zero) (g (dest_sum x)).

Lemma sum_case_inl0 : ∀ f g x,
  (exists a, x == inl a) ->
  sum_case f g x == f (dest_sum x).

Lemma sum_case_inr0 : ∀ f g x,
  (exists b, x == inr b) ->
  sum_case f g x == g (dest_sum x).

Lemma sum_case_ext : ∀ A1 A2 B1 B2 B1' B2',
  eq_fun A1 B1 B1' ->
  eq_fun A2 B2 B2' ->
  eq_fun (sum A1 A2) (sum_case B1 B2) (sum_case B1' B2').

Instance sum_case_morph : Proper
  ((eq_set ==> eq_set) ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set)
  sum_case.
Qed.

Lemma sum_case_ind0 :
  ∀ A B f g x (P:set->Prop),
  Proper (eq_set ==> iff) P ->
  x ∈ sum A B ->
  (∀ a, a ∈ A -> x == inl a -> P (f (dest_sum x))) ->
  (∀ b, b ∈ B -> x == inr b -> P (g (dest_sum x))) ->
  P (sum_case f g x).

Lemma sum_case_inl : ∀ f g a, morph1 f ->
  sum_case f g (inl a) == f a.

Lemma sum_case_inr : ∀ f g b, morph1 g ->
  sum_case f g (inr b) == g b.

Lemma sum_case_ind :
  ∀ A B f g (P:set->Prop),
  Proper (eq_set ==> iff) P ->
  morph1 f ->
  morph1 g ->
  (∀ a, a ∈ A -> P (f a)) ->
  (∀ b, b ∈ B -> P (g b)) ->
  ∀ x,
  x ∈ sum A B ->
  P (sum_case f g x).