(** * Sets, Pairs and Functions ***)
(** Chad E. Brown, August 2013. **)

(** To process this file, Coq must be used with no initial state (i.e., start Coq with the -nois option). **)

(** * ZF without infinity ***)

Parameter set : Type.

(** ** Russell-Prawitz Definitions of Logical Constants. *)

Definition False : Prop := forall P:Prop, P.

Definition not : Prop->Prop := fun A:Prop => A -> False.

Notation "~ x" := (not x) (at level 75, right associativity).

Definition and : Prop->Prop->Prop := fun A B:Prop => forall P:Prop, (A -> B -> P) -> P.

Notation "A /\ B" := (and A B) (at level 80).

Theorem andI : forall (A B : Prop), A -> B -> A /\ B.
exact (fun A B a b P H => H a b).
Qed.

Definition or : Prop->Prop->Prop := fun (A B : Prop) => forall P:Prop, (A -> P) -> (B -> P) -> P.

Notation "A \/ B" := (or A B) (at level 85).

Theorem orIL : forall (A B : Prop), A -> A \/ B.
exact (fun A B a P H1 H2 => H1 a).
Qed.

Theorem orIR : forall (A B : Prop), B -> A \/ B.
exact (fun A B b P H1 H2 => H2 b).
Qed.

Definition iff : Prop->Prop->Prop := fun (A B:Prop) => (A -> B) /\ (B -> A).

Notation "A <-> B" := (iff A B) (at level 95).

Theorem iffI : forall A B:Prop, (A -> B) -> (B -> A) -> (A <-> B).
exact (fun A B => andI (A -> B) (B -> A)).
Qed.

(** Equality can be defined polymorphically as Leibniz equality. As we will only need equality at the type of sets,
 we only define equality on sets using Leibniz equality. **)
Definition eq : set->set->Prop := fun (x y : set) => forall Q:set -> Prop, Q x -> Q y.

Notation "x = y" := (eq x y) (at level 70).
Notation "x <> y" := (~ x = y) (at level 70).

Theorem eqI : forall x:set, x = x.
exact (fun x q H => H).
Qed.

Theorem eq_sym : forall x y:set, x = y -> y = x.
exact (fun x y H => H (fun y => eq y x) (eqI x)).
Qed.

(** Existentials can also be defined polymorphically, but we will only need them for sets and for functions from set to set.
    To emphasize this, we define existential quantification separately for these two instance types. **)
Definition ex : (set->Prop)->Prop := fun P:set->Prop => forall Q:Prop, (forall x, P x -> Q) -> Q.

Notation "'exists' x , p" := (ex (fun x => p))
  (at level 200, x ident).

Theorem exI : forall P:set->Prop, forall x:set, P x -> exists x, P x.
exact (fun P x H1 Q H2 => H2 x H1).
Qed.

Definition ex_f : ((set->set)->Prop)->Prop := fun P:(set->set)->Prop => forall Q:Prop, (forall x, P x -> Q) -> Q.

Notation "'existsf' x , p" := (ex_f (fun x => p))
  (at level 200, x ident).

Theorem exI_f : forall P:(set->set)->Prop, forall F:set->set, P F -> existsf F, P F.
exact (fun P F H1 Q H2 => H2 F H1).
Qed.

Definition exu : (set->Prop)->Prop := fun P:set->Prop => (exists x, P x) /\ (forall x y:set, P x -> P y -> x = y).

Notation "'exists!' x , p" := (exu (fun x => p))
  (at level 200, x ident).

Theorem exuI : forall P:set->Prop, (exists x, P x) -> (forall x y:set, P x -> P y -> x = y) -> exists! x, P x.
exact (fun P => andI (ex P) (forall x y:set, P x -> P y -> eq x y)).
Qed.

(** ** Description Operator *)

Parameter Descr : ((set->Prop)->set).

Axiom DescrR : forall P:set->Prop, (exists! x, P x) -> P (Descr P).

(** ** Axioms of Set Theory: ZF without Infinity **)

(** In is the membership relation on i.  We use x :e y as notation to mean "x is a member of y" and x /:e y as notation for "x is not a member of y." **)

Parameter In:set->set->Prop.

Notation "x ':e' y" := (In x y) (at level 70).
Notation "x '/:e' y" := (~ (In x y)) (at level 70).

(** Subq is the subset relation on set.  We use X c= Y as notation to mean "X is a subset of Y" and X /c= Y as notation for "X is not a subset of Y." **)

Definition Subq : set->set->Prop :=
fun X Y => forall x:set, x :e X -> x :e Y.

Notation "X 'c=' Y" := (Subq X Y) (at level 70).
Notation "X '/c=' Y" := (~ (Subq X Y)) (at level 70).

Lemma Subq_ref : forall X:set, X c= X.
intros X x H1. exact H1.
Qed.

Lemma Subq_tra : forall X Y Z:set, X c= Y -> Y c= Z -> X c= Z.
intros X Y Z H1 H2 x H3. apply H2. apply H1. exact H3.
Qed.

(** Two sets are equal if they have the same elements. Equivalently, we can always prove two sets are equal by proving they are subsets of each other. **)

Axiom set_ext : forall X Y:set, X c= Y -> Y c= X -> X = Y.

(** Sets are formed iteratively, so we can prove Properties about all sets by induction on membership.
Suppose P is a Property of sets. If we can prove P holds for X from the inductive hypothesis that P holds for all member of X,
then P must hold for all sets. **)

Axiom In_ind : forall P:set->Prop, (forall X:set, (forall x, x :e X -> P x) -> P X) -> forall X:set, P X.

(** Empty is the empty set. **)

Parameter Empty : set.

Axiom EmptyAx : ~ exists x, x :e Empty.

Lemma EmptyE : forall x:set, x /:e Empty.
exact (fun x H => EmptyAx (exI (fun x => x :e Empty) x H)).
Qed.

(** Given a set X, (Union X) is the set {x | there is some Y such that x :e Y and Y :e X}. That is, Union gives the union of a set of sets. **)

Parameter Union : set->set.

Axiom UnionEq : forall X:set, forall x:set, x :e Union X <-> exists Y, x :e Y /\ Y :e X.

Lemma UnionE :
forall X x:set, x :e (Union X) -> exists Y, x :e Y /\ Y :e X.
exact (fun X x : set =>
UnionEq X x (x :e Union X -> exists Y, x :e Y /\ Y :e X)
  (fun (H1 : x :e Union X -> exists Y, x :e Y /\ Y :e X)
     (_ : (exists Y, x :e Y /\ Y :e X) -> x :e Union X) => H1)).
Qed.

Lemma UnionI :
forall X x Y:set, x :e Y -> Y :e X -> x :e (Union X).
exact (fun (X x Y : set) (H1 : x :e Y) (H2 : Y :e X) =>
UnionEq X x (x :e Union X)
  (fun (_ : x :e Union X -> exists Y, x :e Y /\ Y :e X)
     (H4 : (exists Y, x :e Y /\ Y :e X) -> x :e Union X) =>
   H4
     (exI (fun Y0 : set => x :e Y0 /\ Y0 :e X) Y
        (andI (x :e Y) (Y :e X) H1 H2)))).
Qed.

(** (Power X) is the set of all subsets of X. **)

Parameter Power : set->set.

Axiom PowerEq : forall X Y:set, Y :e Power X <-> Y c= X.

Lemma PowerE : forall X Y:set, Y :e Power X -> Y c= X.
exact (fun X Y : set =>
PowerEq X Y (Y :e Power X -> Y c= X)
  (fun (H1 : Y :e Power X -> Y c= X) (_ : Y c= X -> Y :e Power X) => H1)).
Qed.

Lemma PowerI : forall X Y:set, Y c= X -> Y :e (Power X).
exact (fun X Y : set =>
PowerEq X Y (Y c= X -> Y :e Power X)
  (fun (_ : Y :e Power X -> Y c= X) (H2 : Y c= X -> Y :e Power X) => H2)).
Qed.

(** In classical set theory, Separation follows from Replacement.
Separation does not generally follow from Replacement in intuitionistic set theory,
although there are alternative formulations of Replacement which are intuitionistically equivalent to
the combination of Separation and Replacement as used here.
 **)
Parameter Sep : set -> (set -> Prop) -> set.

Notation "{ x :i X | P }" := (Sep X (fun x:set => P)).

Axiom SepEq : forall X:set, forall P:set -> Prop, forall x, x :e {z :i X | P z} <-> x :e X /\ P x.

Lemma SepI :  forall X:set, forall P:set -> Prop, forall x:set,
 x :e X -> P x -> x :e {z :i X|P z}.
exact (fun (X : set) (P : set -> Prop) (x : set) (H1 : x :e X) (H2 : P x) =>
SepEq X P x (x :e Sep X P)
  (fun (_ : x :e Sep X P -> x :e X /\ P x)
     (H3 : x :e X /\ P x -> x :e Sep X P) => H3 (andI (x :e X) (P x) H1 H2))).
Qed.

Lemma SepE :  forall X:set, forall P:set -> Prop, forall x:set,
 x :e {z :i X|P z} -> x :e X /\ P x.
intros X P x H1. apply (SepEq X P x). exact (fun H2 _ => H2 H1).
Qed.

Lemma SepE1 :  forall X:set, forall P:set -> Prop, forall x:set,
 x :e {z :i X|P z} -> x :e X.
exact (fun (X : set) (P : set -> Prop) (x : set) (H1 : x :e Sep X P) =>
SepEq X P x (x :e X)
  (fun (H2 : x :e Sep X P -> x :e X /\ P x)
     (_ : x :e X /\ P x -> x :e Sep X P) =>
   H2 H1 (x :e X) (fun (H3 : x :e X) (_ : P x) => H3))).
Qed.

Lemma SepE2 :  forall X:set, forall P:set -> Prop, forall x:set,
 x :e {z :i X|P z} -> P x.
exact (fun (X : set) (P : set -> Prop) (x : set) (H1 : x :e Sep X P) =>
SepEq X P x (P x)
  (fun (H2 : x :e Sep X P -> x :e X /\ P x)
     (_ : x :e X /\ P x -> x :e Sep X P) =>
   H2 H1 (P x) (fun (_ : x :e X) (H3 : P x) => H3))).
Qed.

(** Given a set X and a function F, (Repl X F) is the set {F x|x :e X}. That is, Repl allows us to form a set by
 replacing the elements x in a set X with corresponding elements F x.
 I write (Repl X F) in the eta-expanded form (Repl X (fun z => F z)) just so I can legitimately use the binder notation
 in the written description.
 **)

Parameter Repl : set->(set->set)->set.

Notation "{ F | x :i X }" := (Repl X (fun x:set => F)).

Axiom ReplEq :
forall X:set, forall F:set->set, forall y:set, y :e {F z|z :i X} <-> exists x, x :e X /\ y = F x.

Lemma ReplE :
forall X:set, forall F:set->set, forall y:set, y :e {F z|z :i X} -> exists x, x :e X /\ y = F x.
exact (fun (X : set) (F : set -> set) (y : set) =>
ReplEq X F y
  (y :e Repl X (fun x : set => F x) -> exists x, x :e X /\ y = F x)
  (fun
     (H1 : y :e Repl X (fun x : set => F x) ->
           exists x, x :e X /\ y = F x)
     (_ : (exists x, x :e X /\ y = F x) ->
          y :e Repl X (fun x : set => F x)) => H1)).
Qed.

Lemma ReplI :
forall X:set, forall F:set->set, forall x:set, x :e X -> F x :e {F x|x :i X}.
exact (fun (X : set) (F : set -> set) (x : set) (H1 : x :e X) =>
ReplEq X F (F x) (F x :e Repl X (fun x0 : set => F x0))
  (fun
     (_ : F x :e Repl X (fun x0 : set => F x0) ->
          exists x0, x0 :e X /\ F x = F x0)
     (H4 : (exists x0, x0 :e X /\ F x = F x0) ->
           F x :e Repl X (fun x0 : set => F x0)) =>
   H4
     (exI (fun x0 : set => x0 :e X /\ F x = F x0) x
        (andI (x :e X) (F x = F x) H1 (eqI (F x)))))).
Qed.

Lemma Subq_Empty : forall X:set, Empty c= X.
exact (fun (X x : set) (H : x :e Empty) => EmptyE x H (x :e X)).
Qed.

Lemma Empty_Power : forall X:set, Empty :e Power X.
intros X. apply PowerI. apply Subq_Empty.
Qed.

Lemma In_Power : forall X:set, X :e Power X.
intros X. apply PowerI. apply Subq_ref.
Qed.

Lemma Repl_restr_1 : forall X:set, forall F G:set -> set, (forall x, x :e X -> F x = G x) -> {F x|x :i X} c= {G x|x :i X}.
exact (fun (X : set) (F G : set -> set) (H1 : forall x : set, x :e X -> F x = G x)
  (z : set) (H2 : z :e Repl X F) =>
ReplE X F z H2 (z :e Repl X G)
  (fun (x : set) (H2' : x :e X /\ z = F x) =>
   H2' (z :e Repl X G)
     (fun (H3 : x :e X) (H4 : z = F x) =>
      eq_sym z (F x) H4 (fun z0 : set => z0 :e Repl X G)
        (eq_sym (F x) (G x) (H1 x H3) (fun s : set => s :e Repl X G)
           (ReplI X G x H3))))).
Qed.

Lemma Repl_restr : forall X:set, forall F G:set -> set, (forall x, x :e X -> F x = G x) -> {F x|x :i X} = {G x|x :i X}.
exact (fun (X : set) (F G : set -> set) (H1 : forall x : set, x :e X -> F x = G x) =>
set_ext (Repl X F) (Repl X G) (Repl_restr_1 X F G H1)
  (Repl_restr_1 X G F
     (fun (x : set) (H2 : x :e X) =>
      H1 x H2 (fun s : set => s = F x) (eqI (F x))))).
Qed.

Lemma Repl_Empty : forall F:set -> set, {F x|x :i Empty} = Empty.
exact (fun F : set -> set =>
set_ext (Repl Empty F) Empty
  (fun (x : set) (H1 : x :e Repl Empty F) =>
   ReplE Empty F x H1 (x :e Empty)
     (fun (y : set) (H1' : y :e Empty /\ x = F y) =>
      H1' (x :e Empty)
        (fun (H2 : y :e Empty) (_ : x = F y) => EmptyE y H2 (x :e Empty))))
  (fun (x : set) (H1 : x :e Empty) => EmptyE x H1 (x :e Repl Empty F))).
Qed.

(** Given two sets y and z, (UPair y z) is {y,z}. **)
(** Unordered pairs are often taken as primitives in ZF, but they are definable from the primitives above.
    Zermelo [1930] pointed this out in classical ZF. The argument is given in Suppes [1960;Dover version 1972]
    and formalized in Isabelle-ZF by Paulson [1993].
    The argument in the classical case is a little simpler since (Power (Power Empty)) is a two element set.
    In the intuitionistic case, we use separation to extract a two element subset of (Power (Power Empty)) before using replacement.
 **)
Definition TSet : set := {X :i Power (Power Empty) | Empty :e X \/ Empty /:e X}.
Definition UPair : set->set->set :=
 fun y z:set =>
 {Descr (fun w:set => forall p:set->Prop, (Empty /:e X -> p y) -> (Empty :e X  -> p z) -> p w)|X :i TSet}.

Notation "{ x , y }" := (UPair x y).

Lemma UPairE :
forall x y z:set, x :e {y,z} -> x = y \/ x = z.
intros x y z H1. apply ReplE in H1. apply H1.
intros u H2. apply H2. intros H3 H4.
apply (SepE _ _ _ H3). intros H5 H6. apply (eq_sym _ _ H4).
apply (DescrR (fun v:set => forall p:set->Prop, (Empty /:e u -> p y) -> (Empty :e u  -> p z) -> p v)).
- apply exuI.
  + apply H6.
    * intros H7. apply (exI _ z). intros p _ H8. exact (H8 H7).
    * intros H7. apply (exI _ y). intros p H8 _. exact (H8 H7).
  + intros v w H7 H8. apply H7.
    * { intros H9 p H10. apply H8.
        - intros _. exact H10.
        - intros H11. apply (H9 H11).
      }
    * { intros H9 p H10. apply H8.
        - intros H11. apply (H11 H9).
        - intros _. exact H10.
      }
- intros _. apply orIL. apply eqI.
- intros _. apply orIR. apply eqI.
Qed.

Lemma UPairI1 :
forall y z:set, y :e {y,z}.
intros y z.
assert (H1:Descr (fun v => forall p:set->Prop, (Empty /:e Empty -> p y) -> (Empty :e Empty  -> p z) -> p v) = y).
{
  apply (DescrR (fun v => forall p:set->Prop, (Empty /:e Empty -> p y) -> (Empty :e Empty  -> p z) -> p v)).
  - apply exuI.
    + apply (exI _ y). intros p H2 _. apply H2. apply EmptyE.
    + intros v w H2 H3. apply H2.
      * { intros H4 p H5. apply H3.
          - intros _. exact H5.
          - intros H6. apply (EmptyE _ H6).
        }
      * intros H4. apply (EmptyE _ H4).
  - intros _. apply eqI.
  - intros H2. apply (EmptyE _ H2).
}
apply (H1 (fun w => w :e UPair y z)).
change ((fun u => Descr (fun v => forall p:set->Prop, (Empty /:e u -> p y) -> (Empty :e u  -> p z) -> p v)) Empty :e UPair y z).
apply ReplI. apply SepI.
- apply Empty_Power.
- apply orIR. apply EmptyE.
Qed.

Lemma UPairI2 :
forall y z:set, z :e {y,z}.
intros y z.
assert (H1:Descr (fun v => forall p:set->Prop, (Empty /:e Power Empty -> p y) -> (Empty :e Power Empty  -> p z) -> p v) = z).
{
  apply (DescrR (fun v => forall p:set->Prop, (Empty /:e Power Empty -> p y) -> (Empty :e Power Empty  -> p z) -> p v)).
  - apply exuI.
    + apply (exI _ z). intros p _ H2. apply H2. apply Empty_Power.
    + intros v w H2 H3. apply H2.
      * intros H4. apply H4. apply Empty_Power.
      * { intros H4 p H5. apply H3.
          - intros H6. apply H6. apply Empty_Power.
          - intros _. exact H5.
        }
  - intros H2. apply H2. apply Empty_Power.
  - intros _. apply eqI.
}
apply (H1 (fun w => w :e UPair y z)).
change ((fun u => Descr (fun v => forall p:set->Prop, (Empty /:e u -> p y) -> (Empty :e u  -> p z) -> p v)) (Power Empty) :e UPair y z).
apply ReplI. apply SepI.
- apply In_Power.
- apply orIL. apply Empty_Power.
Qed.

Lemma UPairEq :
forall x y z, x :e {y,z} <-> x = y \/ x = z.
intros x y z. apply andI. apply UPairE. intros H1. apply H1.
intros H2. apply H2. apply UPairI1.
intros H2. apply H2. apply UPairI2.
Qed.

Definition Sing : set->set := fun y:set => {y,y}.

Notation "{| y |}" := (Sing y).

Lemma SingI : forall y, y :e {| y |}.

Proof.
  intros y. unfold Sing. apply UPairI1.
Qed.

Lemma SingE : forall x y, x :e {| y |} -> x = y.

Proof.
  intros x y H1. apply (UPairE _ _ _ H1). exact (fun H => H). exact (fun H => H).
Qed.

Lemma SingEq : forall x y, x :e {| y |} <-> x = y.
intros x y. apply andI. apply SingE. intros H. apply H. apply SingI.
Qed.

(** Given sets X and Y, binunion X Y is the binary union of X and Y. **)
Definition binunion : set -> set -> set := fun X Y => Union {X,Y}.

Notation "X :u: Y" := (binunion X Y) (at level 40).

Lemma binunionI1 : forall X Y z, z :e X -> z :e X :u: Y.
exact (fun (X Y z : set) (H1 : z :e X) => UnionI (UPair X Y) z X H1 (UPairI1 X Y)).
Qed.

Lemma binunionI2 : forall X Y z, z :e Y -> z :e X :u: Y.
exact (fun (X Y z : set) (H1 : z :e Y) => UnionI (UPair X Y) z Y H1 (UPairI2 X Y)).
Qed.

Lemma binunionE : forall X Y z, z :e X :u: Y -> z :e X \/ z :e Y.
exact (fun (X Y z : set) (H1 : z :e binunion X Y) =>
UnionE (UPair X Y) z H1 (z :e X \/ z :e Y)
  (fun (w : set) (H1' : z :e w /\ w :e UPair X Y) =>
   H1' (z :e X \/ z :e Y)
     (fun (H2 : z :e w) (H3 : w :e UPair X Y) =>
      UPairE w X Y H3 (z :e X \/ z :e Y)
        (fun H4 : w = X =>
         orIL (z :e X) (z :e Y) (H4 (fun X0 : set => z :e X0) H2))
        (fun H4 : w = Y =>
         orIR (z :e X) (z :e Y) (H4 (fun Y0 : set => z :e Y0) H2))))).
Qed.

Lemma binunionEq : forall X Y z, z :e X :u: Y <-> z :e X \/ z :e Y.
intros X Y z. apply andI. apply binunionE. intros H1. apply H1. apply binunionI1. apply binunionI2.
Qed.

(** Given sets X and Y, setminus X Y is {x :e X | x /:e Y}. **)
Definition setminus : set -> set -> set := fun X Y => {x :i X| x /:e Y}.

Notation "X \ Y" := (setminus X Y) (at level 40).

Lemma setminusI : forall X Y z, z :e X -> z /:e Y -> z :e X \ Y.
exact (fun (X Y z : set) (H1 : z :e X) (H2 : z /:e Y) => SepI X (fun x : set => x /:e Y) z H1 H2).
Qed.

Lemma setminusE1 : forall X Y z, z :e X \ Y -> z :e X.
exact (fun (X Y z : set) (H1 : z :e setminus X Y) => SepE1 X (fun x : set => x /:e Y) z H1).
Qed.

Lemma setminusE2 : forall X Y z, z :e X \ Y -> z /:e Y.
exact (fun (X Y z : set) (H1 : z :e setminus X Y) => SepE2 X (fun x : set => x /:e Y) z H1).
Qed.

Lemma setminusEq : forall X Y z, z :e X \ Y <-> z :e X /\ z /:e Y.
intros X Y. apply SepEq.
Qed.

(** Given a set X and a function F from sets to sets, famunion X F is the union of all F x where x ranges over X. **)
Definition famunion : set -> (set -> set) -> set :=
fun X F => Union {F x|x :i X}.

Notation "'U' x : X , F" := (famunion X (fun x => F))
  (at level 200, x ident).

Lemma famunionI : forall X:set, forall F:set -> set, forall x y:set, x :e X -> y :e (F x) -> y :e U x:X, F x.
exact (fun (X : set) (F : set -> set) (x y : set) (H1 : x :e X) (H2 : y :e F x) =>
UnionI (Repl X F) y (F x) H2 (ReplI X F x H1)).
Qed.

Lemma famunionE : forall X:set, forall F:set -> set, forall y:set, y :e (U x:X, F x) -> exists x, x :e X /\ y :e (F x).
exact (fun (X : set) (F : set -> set) (y : set) (H1 : y :e famunion X F) =>
UnionE (Repl X F) y H1 (exists x, x :e X /\ y :e F x)
  (fun (z : set) (H1' : y :e z /\ z :e Repl X F) =>
   H1' (exists x, x :e X /\ y :e F x)
     (fun (H2 : y :e z) (H3 : z :e Repl X F) =>
      ReplE X F z H3 (exists x, x :e X /\ y :e F x)
        (fun (x : set) (H3' : x :e X /\ z = F x) =>
         H3' (exists x0, x0 :e X /\ y :e F x0)
           (fun (H4 : x :e X) (H5 : z = F x) =>
            exI (fun x0 : set => x0 :e X /\ y :e F x0) x
              (andI (x :e X) (y :e F x) H4 (H5 (fun s : set => y :e s) H2))))))).
Qed.

Lemma famunionEq : forall X:set, forall F:set -> set, forall y:set, y :e (U x:X, F x) <-> exists x, x :e X /\ y :e (F x).
intros X F y. apply andI. apply famunionE. intros H1. apply H1. intros x H2. apply H2. intros H3 H4.
exact (famunionI _ _ _ _ H3 H4).
Qed.

(** ** Natural Numbers as Finite Ordinals ***)

(** Given a set X, ordsucc X is X union {X}. **)
Definition ordsucc : set->set := fun X => X :u: {|X|}.

Notation "n +" := (ordsucc n) (at level 20).

Lemma ordsucc_Subq : forall X:set, X c= X+.
intros X y H1. apply binunionI1. exact H1.
Qed.

Lemma ordsucc_in : forall X:set, X :e X+.
intros X. apply binunionI2. apply SingI.
Qed.

Lemma ordsuccE : forall X z:set, z :e X+ -> z :e X \/ z = X.
intros X z H1. apply binunionE in H1. apply H1.
- apply orIL.
- intros H2. apply SingE in H2. apply orIR. exact H2.
Qed.

Opaque ordsucc.

Notation "0" := Empty.
Notation "1" := (0+).
Notation "2" := (1+).

Lemma in_0_1 : 0 :e 1.
Proof.
  apply ordsucc_in.
Qed.

Lemma in_0_2 : 0 :e 2.

Proof.
  apply ordsucc_Subq.
  apply ordsucc_in.
Qed.

Lemma in_1_2 : 1 :e 2.

Proof.
  apply ordsucc_in.
Qed.

Lemma neq_0_1 : 0 <> 1.
intros H1. apply (EmptyE 0). apply (eq_sym _ _ H1 (fun z => 0 :e z)). apply in_0_1.
Qed.

Lemma in_1_E : forall X:set, X :e 1 -> X = 0.

Proof.
  intros X H1. apply ordsuccE in H1. apply H1.
  - intros H2. apply (EmptyE _ H2).
  - exact (fun H => H).
Qed.

Lemma in_1_Eq : forall X:set, X :e 1 <-> X = 0.
intros X. apply andI. apply in_1_E. intros H. apply (eq_sym _ _ H). apply in_0_1.
Qed.

Lemma eq_1_Sing0 : 1 = {|0|}.
apply set_ext.
intros X H1. apply (in_1_E X H1). apply SingI.
intros X H1. apply (SingE _ _ H1). apply ordsucc_in.
Qed.

Lemma in_2_E : forall X:set, X :e 2 -> X = 0 \/ X = 1.

Proof.
  intros X H1. apply ordsuccE in H1. apply H1.
  - intros H2. apply (in_1_E _ H2). apply orIL. apply eqI.
  - apply orIR.
Qed.

Lemma in_2_Eq : forall X:set, X :e 2 <-> X = 0 \/ X = 1.
intros X. apply andI. apply in_2_E. intros H. apply H.
clear H. intros H. apply (eq_sym _ _ H). apply in_0_2.
clear H. intros H. apply (eq_sym _ _ H). apply in_1_2.
Qed.

Lemma eq_2_Sing0 : 2 = {0,1}.
apply set_ext.
intros X H1. apply (in_2_E X H1).
intros H2. apply (eq_sym _ _ H2). apply UPairI1.
intros H2. apply (eq_sym _ _ H2). apply UPairI2.
intros X H1. apply (UPairE _ _ _ H1).
intros H2. apply (eq_sym _ _ H2). apply in_0_2.
intros H2. apply (eq_sym _ _ H2). apply in_1_2.
Qed.

(** nat_p is the least predicate including 0 and closed under ordsucc. nat_p X holds if and only if X is a finite ordinal. **)
Definition nat_p (n:set) : Prop :=
forall p:set->Prop, p 0 -> (forall n, p n -> p (n+)) -> p n.

Lemma nat_0 : nat_p 0.
intros p H1 _. exact H1.
Qed.

Lemma nat_ordsucc : forall n:set, nat_p n -> nat_p (n+).
intros n H1 p H2 H3. apply H3. apply H1; assumption.
Qed.

Lemma nat_1 : nat_p 1.
  apply nat_ordsucc. apply nat_0.
Qed.

Lemma nat_2 : nat_p 2.
  apply nat_ordsucc. apply nat_1.
Qed.

Lemma nat_ind : forall p:set->Prop, p 0 -> (forall n, nat_p n -> p n -> p (n+)) -> forall n, nat_p n -> p n.
intros p H1 H2 n H3.
assert (L:nat_p n /\ p n).
{
  apply H3.
  - apply andI.
    + exact nat_0.
    + exact H1.
  - clear n H3. intros n H3. apply H3. intros H4 H5. apply andI.
    + apply nat_ordsucc. exact H4.
    + exact (H2 n H4 H5).
}
apply L. intros _ H. exact H.
Qed.

Lemma nat_inv : forall n, nat_p n -> n = 0 \/ exists m, nat_p m /\ n = m+.
apply (fun H2 H3 => nat_ind _ H2 H3).
- apply orIL. apply eqI.
- intros n H1 IH. apply orIR. apply (exI _ n). apply andI.
  + exact H1.
  + apply eqI.
Qed.

Lemma nat_complete_ind : forall p:set->Prop, (forall n, nat_p n -> (forall m, m :e n -> p m) -> p n) -> forall n, nat_p n -> p n.
intros p H1 n H2. apply H1. exact H2. apply (fun H3 H4 => nat_ind (fun n => forall m, m :e n -> p m) H3 H4 n H2).
- intros m H3. apply (EmptyE _ H3).
- clear n H2. intros n H2 H3 m H4. apply ordsuccE in H4. apply H4.
  + apply H3.
  + intros H5. apply (eq_sym _ _ H5). apply H1.
    * exact H2.
    * exact H3.
Qed.

Lemma nat_0_in_ordsucc : forall n, nat_p n -> 0 :e n+.
intros n H1. apply H1.
- apply in_0_1.
- clear n H1. intros n H1. apply ordsucc_Subq. exact H1.
Qed.

Lemma nat_in_nat : forall n, nat_p n -> forall m, m :e n -> nat_p m.
apply (nat_ind (fun n => forall m, m :e n -> nat_p m)).
- intros m H1. apply (EmptyE _ H1).
- intros n H1 IH m H2. apply ordsuccE in H2. apply H2.
  + apply IH.
  + intros H3. apply (eq_sym _ _ H3). exact H1.
Qed.

Lemma nat_trans : forall n, nat_p n -> forall m, m :e n -> m c= n.
apply (fun H1 H2 => nat_ind (fun n => forall m, m :e n -> m c= n) H1 H2).
- intros m H1. apply (EmptyE m H1).
- intros n H1 IH m H2. apply ordsuccE in H2. apply H2.
  + intros H3 x H4. apply ordsucc_Subq. apply (IH m H3 x H4).
  + intros H3. apply (eq_sym _ _ H3). apply ordsucc_Subq.
Qed.

Lemma nat_ordsucc_in_ordsucc : forall n, nat_p n -> forall m, m :e n -> m+ :e n+.
intros n H1. apply H1.
- intros m H2. apply (EmptyE _ H2).
- clear n H1. intros n H1 m H2. apply ordsuccE in H2. apply H2.
  + intros H3. apply ordsucc_Subq. apply H1. exact H3.
  + intros H3. apply (eq_sym _ _ H3). apply ordsucc_in.
Qed.

(** Membership on natural numbers is decidable. **)
Lemma nat_in_dec : forall n, nat_p n ->
 forall m, nat_p m -> m :e n \/ m /:e n.
apply (nat_ind (fun n => forall m, nat_p m -> m :e n \/ m /:e n)).
- intros m H1. apply orIR. apply EmptyE.
- intros n H1 IH. intros m H2. apply (nat_inv _ H2).
  + intros H3. apply orIL. apply (eq_sym _ _ H3). apply nat_0_in_ordsucc. exact H1.
  + intros H3. apply H3. intros k H4. apply H4. intros H5 H6.
    assert (L: nat_p k).
    {
      apply (nat_in_nat m H2 k). apply (eq_sym _ _ H6). apply ordsucc_in.
    }
    apply (IH k L).
    * intros H7. apply orIL. apply (eq_sym _ _ H6). apply (nat_ordsucc_in_ordsucc _ H1 _ H7).
    * { intros H7. apply orIR. apply (eq_sym _ _ H6). intros H8. apply (ordsuccE _ _ H8).
        - intros H9. apply H7. apply (nat_trans n H1 _ H9). apply ordsucc_in.
        - intros H9. apply H7. apply H9. apply ordsucc_in.
      }
Qed.

(** ** Knaster Tarski ***)
Section KnasterTarski.
Variable Psi:(set -> set -> Prop) -> set -> set -> Prop.

Definition lfp : set -> set -> Prop := fun X Y =>
forall R:set -> set -> Prop, (forall X Y:set, Psi R X Y -> R X Y) -> R X Y.

Definition Psi_monotone : Prop := forall R S:set -> set -> Prop, (forall X Y, R X Y -> S X Y) -> (forall X Y, Psi R X Y -> Psi S X Y).
Hypothesis Psim : Psi_monotone.

Lemma lfp_pre : forall X Y, Psi lfp X Y -> lfp X Y.
intros X Y H1 R H2. apply H2. revert X Y H1. apply Psim.
intros X Y H1. apply (H1 R). exact H2.
Qed.

Lemma lfp_post : forall X Y, lfp X Y -> Psi lfp X Y.
intros X Y H1. apply (H1 (Psi lfp)). apply (Psim (Psi lfp) lfp). exact lfp_pre.
Qed.

Lemma lfp_eq : forall X Y, Psi lfp X Y <-> lfp X Y.
intros X Y. apply andI.
- apply lfp_pre.
- apply lfp_post.
Qed.

End KnasterTarski.

(** ** Epsilon Recursion ***)
Section EpsilonRec.
Variable Phi:set -> (set -> set) -> set.

Let Psi : (set -> set -> Prop) -> set -> set -> Prop :=
(fun R X Y => existsf F, (forall x, x :e X -> R x (F x)) /\ Y = Phi X F).

Definition In_rec_G : set -> set -> Prop :=
lfp Psi.

Definition In_rec : set -> set := fun X => Descr (In_rec_G X).

Lemma PhiPsim : Psi_monotone Psi.
intros R S H1 X Y H2. apply H2. intros F H3. apply H3. intros H4 H5.
apply (exI_f _ F). apply andI.
- intros x H6. apply H1. apply H4. exact H6.
- exact H5.
Qed.

Lemma In_rec_G_c : forall X:set, forall F:set->set, (forall x, x :e X -> In_rec_G x (F x)) -> In_rec_G X (Phi X F).

Proof.
  intros X F H1. apply (lfp_pre Psi PhiPsim).
  apply (exI_f _ F). apply andI.
  - exact H1.
  - apply eqI.
Qed.

Definition Cond_Phi : Prop := forall X:set, forall F G:set -> set, (forall x, x :e X -> F x = G x) -> Phi X F = Phi X G.

Hypothesis Phir:Cond_Phi.

Lemma In_rec_G_f : forall X Y Z:set, In_rec_G X Y -> In_rec_G X Z -> Y = Z.

Proof.
  apply (In_ind (fun X => forall Y Z:set, In_rec_G X Y -> In_rec_G X Z -> Y = Z)).
  intros X IH Y Z H1 H2.
  apply (lfp_post Psi PhiPsim _ _ H1).
  intros F H3. apply H3. intros H4 H5.
  apply (lfp_post Psi PhiPsim _ _ H2).
  intros G H6. apply H6. intros H7 H8.
  apply (eq_sym _ _ H5). apply (eq_sym _ _ H8). apply Phir.
  intros x H9. apply (IH x H9 (F x) (G x)). exact (H4 x H9). exact (H7 x H9).
Qed.

Lemma In_rec_G_In_rec : forall X:set, In_rec_G X (In_rec X).

Proof.
  apply (In_ind (fun X => In_rec_G X (In_rec X))).
  intros X IH. unfold In_rec. apply DescrR. apply exuI.
  - apply (exI _ (Phi X In_rec)).
    apply In_rec_G_c. exact IH.
  - apply In_rec_G_f.
Qed.

Lemma In_rec_G_In_rec_d : forall X:set, In_rec_G X (Phi X In_rec).

Proof.
  intros X. apply In_rec_G_c. intros x _. apply In_rec_G_In_rec.
Qed.

Lemma In_rec_eq : forall X:set, In_rec X = Phi X In_rec.

Proof.
  intros X. apply (In_rec_G_f X). apply In_rec_G_In_rec. apply In_rec_G_In_rec_d.
Qed.

End EpsilonRec.

(** * Specification for Pairs and Functions ***)
Module Type PairFun.

Parameter pair : set -> set -> set.

Local Notation "( x , y )" := (pair x y).

Axiom pair_spec : forall x y w z:set, (x,y) = (w,z) <-> x = w /\ y = z.

Parameter lam : set -> (set -> set) -> set.

Notation "'lambda' x : X , F" := (lam X (fun x:set => F))
  (at level 200, x ident).

Axiom lam_spec : forall X, forall F G:set -> set, (forall x, x :e X -> F x = G x) <-> (lambda x:X, F x) = (lambda x:X, G x).

Parameter SIGMA : set -> (set -> set) -> set.

Local Notation "'Sigma' x : X , Y" := (SIGMA X (fun x:set => Y))
  (at level 200, x ident).

Axiom pair_SigmaEq : forall X:set, forall Y:set->set, forall z:set, z :e (Sigma x : X, Y x) <-> exists x, x :e X /\ exists y, y :e Y x /\ z = (x,y).

Parameter PI : set -> (set -> set) -> set.

Notation "'Pi' x : X , Y" := (PI X (fun x:set => Y))
  (at level 200, x ident).

Axiom lam_PiEq : forall X:set, forall Y:set -> set, forall f:set, f :e (Pi x : X, Y x) <-> existsf F, (forall x, x :e X -> F x :e Y x) /\ f = lambda x:X, F x.

Parameter ap : set -> set -> set.
Axiom beta : forall X:set, forall F:set -> set, forall x:set, x :e X -> ap (lambda x:X, F x) x = F x.
Axiom ap_Pi : forall X:set, forall Y:set -> set, forall f:set, forall x:set, f :e (Pi x:X, Y x) -> x :e X -> (ap f x) :e (Y x).

Axiom lam2_pair : forall F, (lambda z:2, F z) = (F 0,F 1).

Axiom beta0 : forall X:set, forall F:set -> set, forall x:set, x /:e X -> ap (lambda x : X, F x) x = 0.

Axiom Sigma_Power_1 : forall X:set, X :e Power 1 -> forall Y:set->set, (forall x, x :e X -> Y x :e Power 1) -> (Sigma x:X, Y x) :e Power 1.

Axiom Pi_Power_1 : forall X:set, forall Y:set->set, (forall x, x :e X -> Y x :e Power 1) -> (Pi x:X, Y x) :e Power 1.

End PairFun.

(** * Consequences of the Specification ***)
(** These are proven here to make clear that they follow from the specification.
 The ones I really need are reproven in the implementation because the proofs are sometimes clearer there.
 **)
Module PairFunConseq (P:PairFun).
  Import P.

Local Notation "( x , y )" := (pair x y).

Notation "'lambda' x : X , F" := (lam X (fun x:set => F))
  (at level 200, x ident).

Local Notation "'Sigma' x : X , Y" := (SIGMA X (fun x:set => Y))
  (at level 200, x ident).

Notation "'Pi' x : X , Y" := (PI X (fun x:set => Y))
  (at level 200, x ident).

Lemma pair_lam2_ex : forall x y, existsf F, F 0 = x /\ F 1 = y /\ (x,y) = lambda z:2, F z.
intros x y. apply (exI_f _ (fun z => Descr (fun w => (z = 0 -> w = x) /\ (z = 1 -> w = y)))).
assert (L0:(exu (fun w => (0 = 0 -> w = x) /\ (0 = 1 -> w = y)))).
{
  apply andI.
  - apply (exI _ x). apply andI.
    + intros _. apply eqI.
    + intros H1. apply (neq_0_1 H1).
  - intros u v H1 H2. apply H1. intros H3 _. apply H2. intros H4 _.
    apply (eq_sym _ _ (H4 (eqI 0))). apply H3. apply eqI.
}
assert (L1:(exu (fun w => (1 = 0 -> w = x) /\ (1 = 1 -> w = y)))).
{
  apply andI.
  - apply (exI _ y). apply andI.
    + intros H1. apply (neq_0_1 (eq_sym _ _ H1)).
    + intros _. apply eqI.
  - intros u v H1 H2. apply H1. intros _ H3. apply H2. intros _ H4.
    apply (eq_sym _ _ (H4 (eqI 1))). apply H3. apply eqI.
}
assert (L2:Descr (fun w => (0 = 0 -> w = x) /\ (0 = 1 -> w = y)) = x).
{
  apply (DescrR (fun w => (0 = 0 -> w = x) /\ (0 = 1 -> w = y)) L0). intros H1 _. apply H1. apply eqI.
}
assert (L3:Descr (fun w => (1 = 0 -> w = x) /\ (1 = 1 -> w = y)) = y).
{
  apply (DescrR (fun w => (1 = 0 -> w = x) /\ (1 = 1 -> w = y)) L1). intros _ H1. apply H1. apply eqI.
}
apply andI. apply andI. exact L2. exact L3.
apply (eq_sym _ _ (lam2_pair (fun z => Descr (fun w => (z = 0 -> w = x) /\ (z = 1 -> w = y))))).
apply (eq_sym _ _ L2). apply (eq_sym _ _ L3). apply eqI.
Qed.

Local Notation "X * Y" := (Sigma _:X, Y) (at level 40).

Local Notation "X ^ Y" := (Pi _:Y, X) (at level 30).

Lemma setexp_2_eq : forall X:set, X * X = X ^ 2.
Proof.
intros X. apply set_ext.
- intros u H1. apply (pair_SigmaEq X (fun _ => X) u). intros H1a _. specialize (H1a H1).
  apply H1a. intros x H1b. apply H1b. intros H1c H1d. apply H1d. intros y H1e. apply H1e. intros H1f H1g.
  apply (eq_sym _ _ H1g).
  apply (pair_lam2_ex x y). intros F G1. apply G1. intros G2 G3. apply G2. intros G4 G5. apply (eq_sym _ _ G3).
  apply (lam_PiEq 2 (fun _ => X) (lam 2 (fun z => F z))). intros _ H1h. apply H1h. apply (exI_f _ F). apply andI.
  + intros w G6. apply (in_2_E _ G6).
    * intros G7. apply (eq_sym _ _ G7). apply (eq_sym _ _ G4). exact H1c.
    * intros G7. apply (eq_sym _ _ G7). apply (eq_sym _ _ G5). exact H1f.
  + apply eqI.
- intros f H1.
  apply (lam_PiEq 2 (fun _ => X) f). intros G1 _. apply (G1 H1). intros F G2. apply G2.
  intros G3 G4. apply (eq_sym _ _ G4).
  change (lam 2 (fun z => F z) :e X * X).
  apply (eq_sym _ _ (lam2_pair F)).
  apply (pair_SigmaEq X (fun _ => X) (pair (F 0) (F 1))). intros _ G5. apply G5.
  apply (exI _ (F 0)). apply andI.
  + apply G3. exact in_0_2.
  + apply (exI _ (F 1)). apply andI.
    * apply G3. exact in_1_2.
    * apply eqI.
Qed.

Lemma pair_ap_0 : forall x y:set, ap (x,y) 0 = x.

Proof.
  intros x y.
  apply (pair_lam2_ex x y). intros F G1. apply G1. intros G2 G3. apply G2. intros G4 G5. apply (eq_sym _ _ G3).
  apply (eq_sym _ _ (beta 2 F 0 in_0_2)). exact G4.
Qed.

Lemma pair_ap_1 : forall x y:set, ap (x,y) 1 = y.

Proof.
  intros x y.
  apply (pair_lam2_ex x y). intros F G1. apply G1. intros G2 G3. apply G2. intros G4 G5. apply (eq_sym _ _ G3).
  apply (eq_sym _ _ (beta 2 F 1 in_1_2)). exact G5.
Qed.

Lemma pair_ap_n2 : forall x y i:set, i /:e 2 -> ap (x,y) i = 0.

Proof.
  intros x y i H1.
  apply (pair_lam2_ex x y). intros F G1. apply G1. intros G2 G3. apply G2. intros G4 G5. apply (eq_sym _ _ G3).
  apply (eq_sym _ _ (beta0 2 F i H1)). apply eqI.
Qed.

Lemma ap0_Sigma : forall X:set, forall Y:set -> set, forall z:set, z :e (Sigma x:X, Y x) -> (ap z 0) :e X.

Proof.
  intros X Y z H1. apply (pair_SigmaEq X Y z). intros H2 _. apply (H2 H1). intros x H3. apply H3. intros H4 H5.
  apply H5. intros y H6. apply H6. intros H7 H8. apply (eq_sym _ _ H8).
  apply (eq_sym _ _ (pair_ap_0 x y)). exact H4.
Qed.

Lemma ap1_Sigma : forall X:set, forall Y:set -> set, forall z:set, z :e (Sigma x:X, Y x) -> (ap z 1) :e (Y (ap z 0)).

Proof.
  intros X Y z H1. apply (pair_SigmaEq X Y z). intros H2 _. apply (H2 H1). intros x H3. apply H3. intros H4 H5.
  apply H5. intros y H6. apply H6. intros H7 H8. apply (eq_sym _ _ H8).
  apply (eq_sym _ _ (pair_ap_0 x y)). 
  apply (eq_sym _ _ (pair_ap_1 x y)). exact H7.
Qed.

End PairFunConseq.

(** * Implementation of Pairs and Functions ***)
Module PairFunImpl : PairFun.

(** Inj1 is an injection of set into itself that will correspond to x |-> (1,x) after pairing is defined. ***)
Definition Inj1 : set -> set := In_rec (fun X F => {| 0 |} :u: {F x|x :i X}).

Lemma Inj1_eq : forall X:set, Inj1 X = {| 0 |} :u: {Inj1 x|x :i X}.

Proof.
  apply In_rec_eq. intros X F G H.
  assert (L:Repl X (fun x => F x) = Repl X (fun x => G x)).
  {
    apply Repl_restr. exact H.
  }
  apply L. apply eqI.
Qed.

Lemma Inj1I1 : forall X:set, Empty :e Inj1 X.
intros X. apply (fun X => (eq_sym _ _ (Inj1_eq X))). apply binunionI1. apply SingI.
Qed.

Lemma Inj1I2 : forall X x:set, x :e X -> Inj1 x :e Inj1 X.
intros X. apply (fun X => (eq_sym _ _ (Inj1_eq X))). intros x H1. apply binunionI2. apply ReplI. exact H1.
Qed.

Lemma Inj1E : forall X y:set, y :e Inj1 X -> y = Empty \/ exists x, x :e X /\ y = Inj1 x.
intros X y. apply (eq_sym _ _ (Inj1_eq X)). intros H1. apply (binunionE _ _ _ H1); intros H2.
apply orIL. exact (SingE _ _ H2).
apply orIR. exact (ReplE X Inj1 y H2).
Qed.

(** Inj0 is an injection of set into itself that will correspond to x |-> (0,x) after pairing is defined. ***)
Definition Inj0 : set -> set := fun X => {Inj1 x|x :i X}.

Lemma Inj0I : forall X x:set, x :e X -> Inj1 x :e (Inj0 X).
intros X x H1. unfold Inj0. apply ReplI. exact H1.
Qed.

Lemma Inj0E : forall X y:set, y :e Inj0 X -> exists x, x :e X /\ y = Inj1 x.
intros X y. intros H1. exact (ReplE X Inj1 y H1).
Qed.

(** Unj is a left inverse of both Inj1 and Inj0. ***)
Definition Unj : set -> set := In_rec (fun X F => {F x|x :i X \ {|0|} }).

Lemma Unj_eq : forall X:set, Unj X = {Unj x|x :i X \ {|0|} }.

Proof.
  apply In_rec_eq. intros X g h H1. apply Repl_restr. intros x H2. apply H1. exact (setminusE1 _ _ _ H2).
Qed.

Lemma Unj_Inj1_eq : forall X:set, Unj (Inj1 X) = X.
apply (In_ind (fun X => Unj (Inj1 X) = X)).
intros X IHX. apply set_ext.
intros x H1.
generalize H1. apply (fun X => eq_sym _ _ (Unj_eq X)). intros H2. apply (ReplE _ _ x H2). intros y H34. apply H34. intros H3 H4.
generalize (setminusE1 _ _ y H3). intros H5. generalize (setminusE2 _ _ y H3). intros H6.
generalize H5. apply (fun X => eq_sym _ _ (Inj1_eq X)). intros H7. apply (binunionE _ _ y H7); intros H8.
apply (H6 H8).
apply (ReplE X Inj1 y H8). intros z H910. apply H910. intros H9 H10.
apply (eq_sym _ _ H4). apply (eq_sym _ _ H10). apply (eq_sym _ _ (IHX z H9)). exact H9.
intros x H1.
apply (fun X => eq_sym _ _ (Unj_eq X)). apply (IHX x H1). apply ReplI. apply setminusI.
exact (Inj1I2 X x H1).
intros H2. generalize (SingE _ _ H2). intros H3.
assert (H4:~ (Empty /:e (Inj1 x))).
intros H4. apply H4. apply Inj1I1.
apply H4. apply (eq_sym _ _ H3). apply EmptyE.
Qed.

Lemma Inj1_inj : forall X Y:set, Inj1 X = Inj1 Y -> X = Y.
intros X Y H1. apply (Unj_Inj1_eq X). apply (Unj_Inj1_eq Y). apply H1. apply eqI.
Qed.

Lemma Unj_Inj0_eq : forall X:set, Unj (Inj0 X) = X.
intros X. apply set_ext.
intros x H1.
generalize H1. apply (fun X => eq_sym _ _ (Unj_eq X)). intros H2. apply (ReplE _ _ x H2). intros y H34. apply H34. intros H3 H4.
generalize (setminusE1 _ _ y H3). intros H5.
apply (ReplE X Inj1 y H5). intros z H78. apply H78. intros H7 H8.
apply (eq_sym _ _ H4). apply (eq_sym _ _ H8). apply (fun X => eq_sym _ _ (Unj_Inj1_eq X)). exact H7.
intros x H1.
apply (fun X => eq_sym _ _ (Unj_eq X)). apply (Unj_Inj1_eq x).
apply ReplI. apply setminusI.
apply ReplI. exact H1.
intros H2. generalize (SingE _ _ H2). intros H3.
assert (H4:~ (Empty /:e (Inj1 x))).
intros H4. apply H4. apply Inj1I1.
apply H4. apply (eq_sym _ _ H3). apply EmptyE.
Qed.

Lemma Inj0_inj : forall X Y:set, Inj0 X = Inj0 Y -> X = Y.
intros X Y H1. apply (Unj_Inj0_eq X). apply (Unj_Inj0_eq Y). apply H1. apply eqI.
Qed.

Lemma Inj0_Inj1_neq : forall X Y:set, Inj0 X <> Inj1 Y.
intros X Y H1.
generalize (Inj1I1 Y).
apply H1. unfold Inj0. intros H2. apply (ReplE X Inj1 Empty H2). intros x H34. apply H34. intros H3 H4.
generalize (Inj1I1 x). apply H4. apply EmptyE.
Qed.

Lemma Inj0_0 : Inj0 0 = 0.
unfold Inj0. apply Repl_Empty.
Qed.

(** ** Pairing as Disjoint Union ***)
Definition pair : set -> set -> set := fun X Y => {Inj0 x|x :i X} :u: {Inj1 y|y :i Y}.

Notation "( x , y )" := (pair x y).

Lemma pair_0_0 : (0,0) = 0.
apply set_ext.
intros z H1. apply (binunionE _ _ _ H1); intros H2.
generalize (Repl_Empty Inj0 (fun w => z :e w) H2). intros H2'. apply (EmptyE _ H2').
generalize (Repl_Empty Inj1 (fun w => z :e w) H2). intros H2'. apply (EmptyE _ H2').
intros z H1. apply (EmptyE _ H1).
Qed.

Lemma pair_0_x : forall x, Inj0 x = (0,x).
intros x. apply set_ext.
- intros z H1. apply (ReplE _ _ _ H1). intros w H23. apply H23. intros H2 H3.
  apply (eq_sym _ _ H3). apply binunionI2. apply ReplI. exact H2.
- intros z H1. apply (binunionE _ _ _ H1); intros H2.
  generalize (Repl_Empty Inj0 (fun w => z :e w) H2). intros H2'. apply (EmptyE _ H2').
  apply (ReplE _ _ _ H2). intros w H34. apply H34. intros H3 H4. apply (eq_sym _ _ H4). apply ReplI. exact H3.
Qed.

Lemma pair_1_x : forall x, Inj1 x = (1,x).
intros x. apply set_ext.
- intros z H1. apply (Inj1E _ z H1).
  + intros H2. generalize (eq_sym _ _ Inj0_0 (fun w => z = w) H2).
    intros H3. apply (eq_sym _ _ H3).
    apply binunionI1. apply ReplI. apply in_0_1.
  + intros wH23. apply wH23. intros w H23. apply H23. intros H2 H3.
    apply binunionI2. apply (eq_sym _ _ H3). apply ReplI. exact H2.
- intros z H1. apply (binunionE _ _ _ H1); intros H2.
  + apply (ReplE _ _ _ H2). intros w H34. apply H34. intros H3 H4.
    apply (binunionE _ _ _ H3).
    * intros H5. apply (EmptyE _ H5).
    * intros H5. generalize (SingE _ _ H5 (fun w => z = Inj0 w) H4). intros H4'.
      generalize (Inj0_0 (fun u => z = u) H4'). intros H4''. apply (eq_sym _ _ H4''). apply Inj1I1.
  + apply (ReplE _ _ _ H2). intros w H34. apply H34. intros H3 H4. apply (eq_sym _ _ H4). apply Inj1I2. exact H3.
Qed.

(** Now that we know pair_0_x and pair_1_x and consequences, we need never use Inj0 or Inj1 again. ***)
Opaque Inj0 Inj1.

Lemma pairI0 : forall X Y x, x :e X -> (0,x) :e (X,Y).
intros X Y x H1. apply binunionI1. apply (pair_0_x x). apply ReplI. exact H1.
Qed.

Lemma pairI1 : forall X Y y, y :e Y -> (1,y) :e (X,Y).
intros X Y y H1. apply binunionI2. apply (pair_1_x y). apply ReplI. exact H1.
Qed.

Lemma pairE : forall X Y z, z :e (X,Y) -> (exists x, x :e X /\ z = (0,x)) \/ (exists y, y :e Y /\ z = (1,y)).
intros X Y z H1. apply (binunionE _ _ _ H1); intros H2.
apply orIL.
apply (ReplE _ Inj0 _ H2). intros x H3. apply (exI _ x).
apply (pair_0_x x). exact H3.
apply orIR.
apply (ReplE _ Inj1 _ H2). intros y H3. apply (exI _ y).
apply (pair_1_x y). exact H3.
Qed.

Lemma pairEq : forall X Y z, z :e (X,Y) <-> (exists x, x :e X /\ z = (0,x)) \/ (exists y, y :e Y /\ z = (1,y)).
intros X Y z. apply andI.
- apply pairE.
- intros H1. apply H1.
  + intros H2. apply H2. intros x H3. apply H3. intros H4 H5. apply (eq_sym _ _ H5). apply pairI0. exact H4.
  + intros H2. apply H2. intros x H3. apply H3. intros H4 H5. apply (eq_sym _ _ H5). apply pairI1. exact H4.
Qed.

Lemma pair_0_inj : forall x y, (0,x) = (0,y) -> x = y.
intros x y H1. apply Inj0_inj. generalize H1. apply pair_0_x. apply pair_0_x. exact (fun H => H).
Qed.

Lemma pair_1_inj : forall x y, (1,x) = (1,y) -> x = y.
intros x y H1. apply Inj1_inj. generalize H1. apply pair_1_x. apply pair_1_x. exact (fun H => H).
Qed.

Lemma pair_0_1_neq : forall x y, (0,x) <> (1,y).
intros x y. apply pair_0_x. apply pair_1_x. apply Inj0_Inj1_neq.
Qed.

Lemma pairE0 : forall X Y x, (0,x) :e (X,Y) -> x :e X.
intros X Y x H1. apply (pairE _ _ _ H1).
- intros H2. apply H2. intros w H3. apply H3. intros H4 H5.
  apply (eq_sym _ _ (pair_0_inj _ _ H5)). exact H4.
- intros H2. apply H2. intros y H3. apply H3. intros H4 H5.
  apply (pair_0_1_neq _ _ H5).
Qed.

Lemma pairE1 : forall X Y y, (1,y) :e (X,Y) -> y :e Y.
intros X Y y H1. apply (pairE _ _ _ H1).
- intros H2. apply H2. intros x H3. apply H3. intros H4 H5.
  apply (pair_0_1_neq _ _ (eq_sym _ _ H5)).
- intros H2. apply H2. intros w H3. apply H3. intros H4 H5.
  apply (eq_sym _ _ (pair_1_inj _ _ H5)). exact H4.
Qed.

Lemma pair_inj_Subq_0 : forall x y w z:set, (x,y) c= (w,z) -> x c= w.
intros x y w z H1 u H2.
generalize (pairI0 x y u H2). intros H3.
generalize (H1 _ H3). intros H4. apply pairE0 in H4. exact H4.
Qed.

Lemma pair_inj_Subq_1 : forall x y w z:set, (x,y) c= (w,z) -> y c= z.
intros x y w z H1 u H2.
generalize (pairI1 x y u H2). intros H3.
generalize (H1 _ H3). intros H4. apply pairE1 in H4. exact H4.
Qed.

Theorem pair_inj : forall x y w z:set, (x,y) = (w,z) -> x = w /\ y = z.
intros x y w z H1. apply andI.
- apply set_ext.
  + apply (pair_inj_Subq_0 x y w z). apply H1. apply Subq_ref.
  + apply (pair_inj_Subq_0 w z x y). apply H1. apply Subq_ref.
- apply set_ext.
  + apply (pair_inj_Subq_1 x y w z). apply H1. apply Subq_ref.
  + apply (pair_inj_Subq_1 w z x y). apply H1. apply Subq_ref.
Qed.

Theorem pair_spec : forall x y w z:set, (x,y) = (w,z) <-> x = w /\ y = z.
intros x y w z. apply andI. apply pair_inj.
intros H1. apply H1. intros H2 H3. apply H2. apply H3. apply eqI.
Qed.

(** ** Functions ***)
(** Functions are represented following Aczel's trace representation. The exact sets one obtains depends on the representation of pairs. **)

(** lam X F is {(x,y) | x :e X, y :e F x}. **)
Definition lam : set -> (set -> set) -> set :=
fun X F => U x:X, {(x,y)|y :i F x}.

Notation "'lambda' x : X , F" := (lam X (fun x:set => F))
  (at level 200, x ident).

Lemma lamI : forall X:set, forall F:set->set, forall x y:set, x :e X -> y :e F x -> (x,y) :e lambda x:X, F x.
intros X F x y H1 H2. unfold lam. apply famunionI with (x := x).
- exact H1.
- apply ReplI. exact H2.
Qed.

Lemma lamE : forall X:set, forall F:set->set, forall z:set, z :e (lambda x:X, F x) -> exists x, x :e X /\ exists y, y :e F x /\ z = (x,y).
intros X F z. unfold lam. intros H1. apply famunionE in H1. apply H1. intros x H2. apply H2. intros H3 H4. apply (exI _ x). apply andI.
- exact H3.
- apply ReplE in H4. exact H4.
Qed.

Lemma lamEq : forall X:set, forall F:set->set, forall z:set, z :e (lambda x:X, F x) <-> exists x, x :e X /\ exists y, y :e F x /\ z = (x,y).
intros X F z. apply andI.
- apply lamE.
- intros H1. apply H1. intros x H2. apply H2. intros H3 H4. apply H4. intros y H5. apply H5. intros H6 H7.
  apply (eq_sym _ _ H7). apply lamI.
  + exact H3.
  + exact H6.
Qed.

Lemma lamPE : forall X:set, forall F:set -> set, forall x y:set, (x,y) :e (lambda x:X, F x) -> x :e X /\ y :e F x.
intros X F x y H1. apply (lamE X F (pair x y) H1). intros w H2. apply H2.
intros H3 H4. apply H4. intros z H5. apply H5. intros H6 H7. apply (pair_inj x y w z H7).
intros H8 H9. apply (eq_sym _ _ H8). apply (eq_sym _ _ H9). apply andI.
exact H3. exact H6.
Qed.

Lemma lamPEq : forall X:set, forall F:set -> set, forall x y:set, (x,y) :e (lambda x:X, F x) <-> x :e X /\ y :e F x.
intros X F x y. apply andI. apply lamPE. intros H1. apply H1. apply lamI.
Qed.

(** ap f x is {y | (x,y) is in f}, i.e., {the y such that z = (x,y) | z :e f; exists y, z = (x,y)} **)
Definition ap : set -> set -> set :=
fun f x => {Descr (fun y => z = (x,y))|z :i {z :i f|exists y, z = (x,y)} }.

Theorem apEq : forall f x y, y :e ap f x <-> (x,y) :e f.

Proof.
  intros f x.
  assert (L1:forall y, pair x y = pair x (Descr (fun w => pair x y = pair x w))).
  {
    intros y. apply DescrR. apply andI.
    - apply (exI _ y). apply eqI.
    - intros w z H2 H3.
      apply (pair_inj x y x w H2). intros _ H4.
      apply (pair_inj x y x z H3). intros _ H5.
      apply H4. exact H5.
  }
  assert (L2:forall y, Descr (fun w => pair x y = pair x w) = y).
  {
    intros y. apply (pair_inj x y x (Descr (fun w => pair x y = pair x w)) (L1 y)). intros _ H2. apply eq_sym. exact H2.
  }
  intros y. unfold ap. apply andI.
  - intros H1. apply (ReplE _ _ _ H1). intros z H2. apply H2. intros H3 H4. apply (SepE _ _ _ H3). intros H5 H6. apply H6. intros w H7.
    generalize (L2 w). apply H7. apply H4. intros H8. apply (eq_sym _ _ H8). apply H7. exact H5.
  - intros H1. apply (L2 y).
    apply (ReplI _ (fun z => Descr (fun y => z = pair x y))). apply SepI.
    + exact H1.
    + apply (exI _ y). apply eqI.
Qed.

Lemma apI : forall f x y, (x,y) :e f -> y :e ap f x.
  intros f x y. apply (apEq f x y). exact (fun _ H => H).
Qed.

Lemma apE : forall f x y, y :e ap f x -> (x,y) :e f.
  intros f x y. apply (apEq f x y). exact (fun H _ => H).
Qed.

Theorem beta : forall X:set, forall F:set -> set, forall x:set, x :e X -> ap (lambda x:X, F x) x = F x.
intros X F x H1. apply set_ext.
- intros w H2. apply apE in H2. apply lamPE in H2. apply H2. exact (fun _ H => H).
- intros y H2. apply apI. apply lamI. exact H1. exact H2.
Qed.

Theorem beta0 : forall X:set, forall F:set -> set, forall x:set, x /:e X -> ap (lambda x:X, F x) x = 0.
intros X F x H1. apply set_ext.
- intros w H2. apply apE in H2. apply lamPE in H2. apply H2. intros H3. apply (H1 H3).
- apply Subq_Empty.
Qed.

Lemma lam_inj_lem : forall X, forall F G:set -> set, (forall x, x :e X -> F x = G x) -> (lambda x:X, F x) c= (lambda x:X, G x).
intros X F G H1 f H2. apply (lamE _ _ _ H2). intros x H3. apply H3. intros H4 H5. apply H5. intros y H6. apply H6. intros H7 H8.
apply (eq_sym _ _ H8). apply lamI. exact H4. apply (H1 x H4). exact H7.
Qed.

Lemma lam_inj : forall X, forall F G:set -> set, (forall x, x :e X -> F x = G x) -> (lambda x:X, F x) = (lambda x:X, G x).
intros X F G H1. apply set_ext.
exact (lam_inj_lem X F G H1).
apply (lam_inj_lem X G F). intros x H2. apply eq_sym. exact (H1 x H2).
Qed.

Theorem lam_spec : forall X, forall F G:set -> set, (forall x, x :e X -> F x = G x) <-> (lambda x:X, F x) = (lambda x:X, G x).
intros X F G. apply andI. apply lam_inj.
intros H1 x H2. apply (beta X F x H2). apply (beta X G x H2). apply H1. apply eqI.
Qed.

Opaque ap lam.

Lemma lam2_pair : forall F, (lambda z:2, F z) = (F 0,F 1).
intros F. apply set_ext.
- intros u H3. apply (lamE _ _ _ H3). intros z H4. apply H4. intros H5 H6. apply (in_2_E _ H5).
  + intros H7. generalize (H7 (fun z => exists y, y :e F z /\ u = pair z y) H6). intros H8. apply H8. intros v H9. apply H9. intros H10 H11.
    apply (eq_sym _ _ H11). apply pairI0. exact H10.
  + intros H7. generalize (H7 (fun z => exists y, y :e F z /\ u = pair z y) H6). intros H8. apply H8. intros v H9. apply H9. intros H10 H11.
    apply (eq_sym _ _ H11). apply pairI1. exact H10.
- intros u H3. apply (pairE _ _ _ H3).
  + intros H4. apply H4. intros v H5. apply H5. intros H6 H7. apply (eq_sym _ _ H7). apply lamI.
    * exact in_0_2.
    * exact H6.
  + intros H4. apply H4. intros v H5. apply H5. intros H6 H7. apply (eq_sym _ _ H7). apply lamI.
    * exact in_1_2.
    * exact H6.
Qed.

Theorem pair_ap_0 : forall x y:set, ap (x,y) 0 = x.
intros x y. apply set_ext.
- intros z H1. apply apE in H1. apply pairE0 in H1. exact H1.
- intros z H1. apply apI. apply pairI0. exact H1.
Qed.

Theorem pair_ap_1 : forall x y, ap (x,y) 1 = y.
intros x y. apply set_ext.
- intros z H1. apply apE in H1. apply pairE1 in H1. exact H1.
- intros z H1. apply apI. apply pairI1. exact H1.
Qed.

Theorem pair_ap_n2 : forall x y i:set, i /:e 2 -> ap (x,y) i = 0.
intros x y i H0. apply set_ext.
- intros z H1. apply H0. apply apE in H1. apply pairE in H1. apply H1.
  + intros H2. apply H2. intros w H3. apply H3. intros H4 H5.
    apply (pair_ap_0 i z). apply (eq_sym _ _ H5). apply (eq_sym _ _ (pair_ap_0 0 w)). apply in_0_2.
  + intros H2. apply H2. intros w H3. apply H3. intros H4 H5.
    apply (pair_ap_0 i z). apply (eq_sym _ _ H5). apply (eq_sym _ _ (pair_ap_0 1 w)). apply in_1_2.
- apply Subq_Empty.
Qed.

(** ** Sets of Pairs: Sigma as Lambda ***)
Definition SIGMA : set -> (set -> set) -> set := lam.

Notation "'Sigma' x : X , Y" := (SIGMA X (fun x:set => Y))
  (at level 200, x ident).

(** pair_SigmaI is the same as lamI and pair_SigmaE is the same as lamE. ***)
Theorem pair_SigmaI : forall X:set, forall Y:set -> set, forall x y:set, x :e X -> y :e (Y x) -> (x,y) :e (Sigma x:X, Y x).
exact lamI.
Qed.

Theorem pair_SigmaE : forall X:set, forall Y:set -> set, forall u:set, u :e (Sigma x:X, Y x) -> exists x, x :e X /\ exists y, y :e Y x /\ u = (x,y).
exact lamE.
Qed.

Theorem pair_SigmaEq : forall X:set, forall Y:set->set, forall z:set, z :e (Sigma x:X, Y x) <-> exists x, x :e X /\ exists y, y :e Y x /\ z = (x,y).
exact lamEq.
Qed.

Lemma ap0_Sigma : forall X:set, forall Y:set -> set, forall z:set,
z :e (Sigma x:X, Y x) -> (ap z 0) :e X.
intros X Y z H1. apply (famunionE _ _ _ H1). intros x H23. apply H23. intros H2 H3.
apply (ReplE _ _ _ H3). intros y H45. apply H45. intros H4 H5.
apply (eq_sym _ _ H5). apply (eq_sym _ _ (pair_ap_0 x y)). exact H2.
Qed.

Lemma ap1_Sigma : forall X:set, forall Y:set -> set, forall z:set,
z :e (Sigma x:X, Y x) -> (ap z 1) :e (Y (ap z 0)).
intros X Y z H1. apply (famunionE _ _ _ H1). intros x H23. apply H23. intros H2 H3.
apply (ReplE _ _ _ H3). intros y H45. apply H45. intros H4 H5.
apply (eq_sym _ _ H5). apply (eq_sym _ _ (pair_ap_0 x y)). apply (eq_sym _ _ (pair_ap_1 x y)). exact H4.
Qed.

Lemma Sigma_eta : forall X:set, forall Y:set -> set, forall z:set,
z :e (Sigma x:X, Y x) -> (ap z 0,ap z 1) = z.
intros X Y z H1. apply (famunionE _ _ _ H1). intros x H23. apply H23. intros H2 H3.
apply (ReplE _ _ _ H3). intros y H45. apply H45. intros H4 H5.
apply (eq_sym _ _ H5).
apply (eq_sym _ _ (pair_ap_0 x y)). 
apply (eq_sym _ _ (pair_ap_1 x y)). 
apply eqI.
Qed.

(** ** Sets of Functions: Pi ***)
(** PI X Y = {f in (Power (Sigma X (fun x => (Union (Y x))))) | forall x:X, ap f x : Y x} ***)
Definition PI : set -> (set -> set) -> set :=
fun X Y => {f :i (Power (Sigma x:X, (Union (Y x)))) | forall x, x :e X -> (ap f x) :e (Y x)}.

Notation "'Pi' x : X , Y" := (PI X (fun x:set => Y))
  (at level 200, x ident).

Lemma lam_PiI : forall X:set, forall Y:set -> set, forall F:set -> set,
(forall x:set, x :e X -> (F x) :e (Y x)) -> (lambda x:X, F x) :e (Pi x:X, Y x).
intros X Y F H1. apply SepI. apply PowerI. intros z H2.
apply (famunionE _ _ _ H2). intros x H34. apply H34. intros H3 H4.
apply (ReplE _ _ _ H4). intros y H56. apply H56. intros H5 H6.
apply (eq_sym _ _ H6). apply pair_SigmaI.
exact H3.
apply (UnionI _ _ (F x)). exact H5. exact (H1 x H3).
intros x H2. apply (eq_sym _ _ (beta X F x H2)). exact (H1 x H2).
Qed.

Lemma ap_Pi : forall X:set, forall Y:set -> set, forall f:set, forall x:set,
f :e (Pi x:X, Y x) -> x :e X -> (ap f x) :e (Y x).
intros X Y f x H1 H2.
generalize (SepE2 _ _ _ H1). intros H3.
exact (H3 x H2).
Qed.

Lemma Pi_eta : forall X:set, forall Y:set -> set, forall f:set,
f :e (Pi x:X, Y x) -> (lambda x:X, ap f x) = f.
intros X Y f H1.
apply set_ext.
- intros z H4. apply (lamE _ _ _ H4).  intros x H56. apply H56. intros H5 H6. apply H6.
intros y H78. apply H78. intros H7 H8.
apply (eq_sym _ _ H8). apply apE. exact H7.
- intros z H4. apply (SepE _ _ _ H1). intros H2 H3.
generalize (PowerE _ _ H2 z H4). intros H5. apply lamE in H5. apply H5. intros x H6. apply H6. intros H7 H8.
apply H8. intros y H9. apply H9. intros H10 H11. generalize H4. apply (eq_sym _ _ H11). intros H12. apply lamI.
+ exact H7.
+ apply apI. exact H12.
Qed.

Lemma lam_PiE : forall X:set, forall Y:set -> set, forall f:set, f :e (Pi x:X, Y x) -> existsf F, (forall x, x :e X -> F x :e Y x) /\ f = lambda x:X, F x.
intros X Y f H1. apply (exI_f _ (fun x => ap f x)). apply andI.
apply (SepE2 _ _ _ H1).
apply eq_sym. apply (Pi_eta X Y f H1).
Qed.

Lemma lam_PiEq : forall X:set, forall Y:set -> set, forall f:set, f :e (Pi x:X, Y x) <-> existsf F, (forall x, x :e X -> F x :e Y x) /\ f = lambda x:X, F x.
intros X Y f H1. apply andI. apply lam_PiE.
intros H2. apply H2. intros F H3. apply H3. intros H4 H5. apply (eq_sym _ _ H5). apply lam_PiI. exact H4.
Qed.

Notation "X * Y" := (Sigma _:X, Y) (at level 40).

Notation "X ^ Y" := (Pi _:Y, X) (at level 30).

Lemma setexp_2_eq : forall X:set, X * X = X ^ 2.

Proof.
intros X. apply set_ext.
- intros u H1. apply (Sigma_eta X (fun _ => X) u H1).
  apply lam2_pair.
  apply lam_PiI. intros z H2. apply (in_2_E _ H2).
  + intros H3. apply (eq_sym _ _ H3). apply (ap0_Sigma X (fun _ => X) u H1).
  + intros H3. apply (eq_sym _ _ H3). apply (ap1_Sigma X (fun _ => X) u H1).
- intros f H1. apply (Pi_eta 2 (fun _ => X) f H1). apply (eq_sym _ _ (lam2_pair (ap f))).
  apply pair_SigmaI.
  + apply (ap_Pi 2 (fun _ => X) f 0 H1 in_0_2).
  + apply (ap_Pi 2 (fun _ => X) f 1 H1 in_1_2).
Qed.

(** ** Closure of Power 1 under Sigma and Pi (with Pi impredicative) ***)
Lemma Sigma_Power_1 : forall X:set, X :e Power 1 -> forall Y:set->set, (forall x, x :e X -> Y x :e Power 1) -> (Sigma x:X, Y x) :e Power 1.
intros X H1 Y H2. apply PowerI. intros z H3.
generalize (ap0_Sigma _ _ _ H3). intros H4.
generalize (PowerE _ _ H1 _ H4). intros H5.
generalize (ap1_Sigma _ _ _ H3). intros H6.
generalize (PowerE _ _ (H2 (ap z 0) H4) _ H6). intros H7.
apply (Sigma_eta _ _ _ H3). apply (eq_sym _ _ (in_1_E _ H5)). apply (eq_sym _ _ (in_1_E _ H7)).
apply (eq_sym _ _ pair_0_0). apply in_0_1.
Qed.

Lemma Pi_Power_1 : forall X:set, forall Y:set->set, (forall x, x :e X -> Y x :e Power 1) -> (Pi x:X, Y x) :e Power 1.
intros X Y H2. apply PowerI. intros f H3.
cut (f = 0).
- intros H4. apply (eq_sym _ _ H4). apply in_0_1.
- apply set_ext.
  + intros z. apply (Pi_eta _ _ _ H3). intros H4.
    assert (L:False).
    { apply lamE in H4. apply H4.
      intros x H5. apply H5. intros H6. 
      intros H7. apply H7. intros y H8. apply H8. intros H9 _. generalize (ap_Pi _ _ _ _ H3 H6). intros H10.
      generalize (PowerE _ _ (H2 x H6) _ H10). intros H11.
      apply in_1_E in H11. revert H9. apply (eq_sym _ _ H11). apply EmptyE.
    }
    apply L.
  + apply Subq_Empty.
Qed.

(** ** Monotonicity Results **)

Lemma pairSubq : forall X Y W Z, X c= W -> Y c= Z -> (X,Y) c= (W,Z).
intros X Y W Z H1 H2 u H3. apply pairE in H3. apply H3.
- intros H4. apply H4. intros x H5. apply H5. intros H6 H7. apply (eq_sym _ _ H7). apply pairI0. apply H1, H6.
- intros H4. apply H4. intros y H5. apply H5. intros H6 H7. apply (eq_sym _ _ H7). apply pairI1. apply H2, H6.
Qed.

(** Covariance of subsets of Sigmas ***)
Lemma Sigma_mon : forall X Y:set, X c= Y -> forall Z W:set->set, (forall x, x :e X -> Z x c= W x) -> (Sigma x:X, Z x) c= (Sigma y:Y, W y).
intros X Y H1 Z W H2 u H3. apply (Sigma_eta _ _ _ H3).
apply lamI.
- apply H1. exact (ap0_Sigma _ _ _ H3).
- apply H2.
  + exact (ap0_Sigma _ _ _ H3).
  + apply (ap1_Sigma _ _ _ H3).
Qed.

Lemma Sigma_mon0 : forall X Y:set, X c= Y -> forall Z:set->set, (Sigma x:X, Z x) c= (Sigma y:Y, Z y).
intros X Y H1 Z. apply Sigma_mon with (W := Z).
- exact H1.
- intros x _. apply Subq_ref.
Qed.

Lemma Sigma_mon1 : forall X:set, forall Z W:set->set, (forall x, x :e X -> Z x c= W x) -> (Sigma x:X, Z x) c= (Sigma x:X, W x).
intros X Z W H1. apply Sigma_mon.
- apply Subq_ref.
- exact H1.
Qed.

(** Covariance of subsets of function spaces when codomain has 0 as a member.
 This depends on an assumption about decidability of X relative to Y.
 ***)
Lemma Pi_0_dom_mon : forall X Y:set, forall A:set->set,
 X c= Y ->
 (forall y, y :e Y -> y :e X \/ y /:e X) ->
 (forall y, y :e Y -> y /:e X -> 0 :e A y) ->
 (Pi x:X, A x) c= (Pi x:Y, A x).
intros X Y A H1 D1 H2 f H3. apply (SepE _ _ _ H3). intros H4 H5. apply SepI.
- apply PowerI. intros z H6. generalize (PowerE _ _ H4 z H6). apply Sigma_mon0. exact H1.
- intros y H6. apply (D1 y H6).
  + apply H5.
  + intros H7. apply (Pi_eta _ _ _ H3). apply (eq_sym _ _ (beta0 X (fun x => ap f x) y H7)). apply H2.
    * exact H6.
    * exact H7.
Qed.

Lemma setexp_0_dom_mon : forall A:set, 0 :e A -> forall X Y:set,
 X c= Y ->
 (forall y, y :e Y -> y :e X \/ y /:e X) ->
 A ^ X c= A ^ Y.
  intros A H1 X Y H2 D1. apply Pi_0_dom_mon.
  - exact H2.
  - exact D1.
  - intros y _ _. exact H1.
Qed.

Lemma Pi_cod_mon : forall X:set, forall A B:set->set, (forall x, x :e X -> A x c= B x) -> (Pi x:X, A x) c= (Pi x:X, B x).
intros X A B H1 f H2. apply (Pi_eta _ _ _ H2). apply lam_PiI. intros x H3. apply (H1 x H3).
apply (ap_Pi _ _ _ x H2 H3).
Qed.

Lemma Pi_0_mon : forall X Y:set, forall A B:set->set,
(forall x, x :e X -> A x c= B x) ->
 X c= Y ->
 (forall y, y :e Y -> y :e X \/ y /:e X) -> 
 (forall y, y :e Y -> y /:e X -> 0 :e B y) ->
 (Pi x:X, A x) c= (Pi y:Y, B y).
intros X Y A B H1 H2 H3 H4. apply (Subq_tra _ (Pi x:X, B x)).
- apply Pi_cod_mon. exact H1.
- apply Pi_0_dom_mon.
  + exact H2.
  + exact H3.
  + exact H4.
Qed.

Lemma setexp_0_mon : forall X Y A B:set,
 0 :e B -> A c= B ->
 X c= Y ->
 (forall y, y :e Y -> y :e X \/ y /:e X) ->
 A ^ X c= B ^ Y.
intros X Y A B H1 H2 H3 H4. apply Pi_0_mon.
- intros _ _. exact H2.
- exact H3.
- exact H4.
- intros _ _ _. exact H1.
Qed.

(** Combining transitivity of natural numbers (finite ordinals) with decidability of membership on natural numbers,
 we know that if 0 is in A, n is a natural number and m is in n (i.e., m < n),
 then the set of m-tuples from A is a subset of the set of n-tuples from A. **)
Lemma nat_in_setexp_mon : forall A:set, 0 :e A -> forall n, nat_p n ->
 forall m, m :e n -> A ^ m c= A ^ n.
intros A H1 n H2 m H3. apply setexp_0_dom_mon.
- exact H1.
- apply nat_trans.
  + exact H2.
  + exact H3.
- intros k H4. apply nat_in_dec.
  + apply (nat_in_nat _ H2 _ H3).
  + apply (nat_in_nat _ H2 _ H4).
Qed.

(** ** Sums are Pairs ***)
Definition sum : set -> set -> set := pair.

Notation "X :+: Y" := (sum X Y) (at level 50).

(** These next three are duplicates of pairI0, pairI1 and pairE. ***)
Lemma pair0_sum : forall X Y x:set, x :e X -> (0,x) :e X :+: Y.

Proof.
  exact pairI0.
Qed.

Lemma pair1_sum : forall X Y y:set, y :e Y -> (1,y) :e X :+: Y.

Proof.
  exact pairI1.
Qed.

Lemma sum_inv : forall X Y z:set, z :e X :+: Y -> (exists x, x :e X /\ z = (0,x)) \/ (exists y, y :e Y /\ z = (1,y)).

Proof.
  exact pairE.
Qed.

Lemma sumEq : forall X Y z, z :e X :+: Y <-> (exists x, x :e X /\ z = (0,x)) \/ (exists y, y :e Y /\ z = (1,y)).
exact pairEq.
Qed.

Lemma pair_1_0_1 : (1,0) = 1.
apply set_ext.
- intros z H1. apply pairE in H1. apply H1.
  + intros H2. apply H2. intros x H3. apply H3. intros H4 H5.
    apply (eq_sym _ _ H5). apply (eq_sym _ _ (in_1_E _ H4)).
    apply (eq_sym _ _ pair_0_0). apply in_0_1.
  + intros H2. apply H2. intros x H3. apply H3. intros H4 _. apply (EmptyE _ H4).
- intros z H1. apply (eq_sym _ _ (in_1_E  _ H1)). apply (pair_0_0 (fun z => z :e pair 1 0)). apply pairI0. apply in_0_1.
Qed.

Lemma nat_pair1_ordsucc : forall n:set, nat_p n -> (1,n) = ordsucc n.
apply nat_complete_ind. intros n H1 IH. apply set_ext.
- intros z H2. apply pairE in H2. apply H2.
  + intros H3. apply H3. intros x H4. apply H4. intros H5 H6.
    apply in_1_E in H5. apply H5 in H6. apply pair_0_0 in H6.
    apply (eq_sym _ _ H6). apply nat_0_in_ordsucc. exact H1.
  + intros H3. apply H3. intros y H4. apply H4. intros H5 H6.
    apply (eq_sym _ _ H6).
    apply (eq_sym _ _ (IH y H5)). apply nat_ordsucc_in_ordsucc.
    * exact H1.
    * exact H5.
- intros z H2. apply ordsuccE in H2. apply H2.
  + intros H3. generalize (nat_in_nat n H1 z H3). intros H4. apply (nat_inv z H4).
    * intros H5. apply (eq_sym _ _ H5). apply (pair_0_0 (fun z => z :e pair 1 n)). apply pairI0. apply in_0_1.
    * intros H5. apply H5. intros y H6. apply H6. intros H7 H8. 
      assert (L: y :e z).
      {
        apply (eq_sym _ _ H8). apply ordsucc_in.
      }
      generalize (nat_trans n H1 z H3 y L). intros H9.
      generalize (IH y H9). intros H10. apply (eq_sym _ _ H8). apply H10. apply pairI1. exact H9.
  + intros H3. apply (eq_sym _ _ H3). apply (nat_inv n H1).
    * intros H4. apply (eq_sym _ _ H4). apply (eq_sym _ _ pair_1_0_1). apply in_0_1.
    * intros H4. apply H4. intros x H5. apply H5. intros H6 H7.
      assert (L: x :e n).
      {
        apply (eq_sym _ _ H7). apply ordsucc_in.
      }
      apply (eq_sym _ _ H7). apply (IH x L (fun z => z :e pair 1 (ordsucc x))). apply pairI1. apply ordsucc_in.
Qed.

Lemma nat_sum1_ordsucc : forall n:set, nat_p n -> 1 :+: n = ordsucc n.
exact nat_pair1_ordsucc.
Qed.

Lemma sum_1_0_1 : 1 :+: 0 = 1.
exact pair_1_0_1.
Qed.

Lemma pair_1_1_2 : (1,1) = 2.
apply nat_pair1_ordsucc. exact nat_1.
Qed.

Lemma sum_1_1_2 : 1 :+: 1 = 2.
apply nat_sum1_ordsucc. exact nat_1.
Qed.

(** Covariance of subsets of sums (same as pairSubq) ***)
Lemma sum_mon : forall X Y W Z, X c= W -> Y c= Z -> X :+: Y c= W :+: Z.
exact pairSubq.
Qed.

End PairFunImpl.