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'.
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'.