Require Export Classical.
Require Export Epsilon.
Require Export FunctionalExtensionality.
Require Export ProofIrrelevance.
Axiom prop_extensionality : ( P Q:Prop, (P Q) → P = Q).

Require Export ZFMType.

Module ZFAcz : ZF.

Inductive Acz : Type :=
Asup : A:Type, (AAcz) → Acz.

(*** Following Werner 97 ***)
Fixpoint Aeq (X Y:Acz) : Prop :=
match X,Y with
| Asup A f,Asup B g
     ( a, b, Aeq (f a) (g b))
   ( b, a, Aeq (f a) (g b))

Lemma Aeq_ref (X:Acz) : Aeq X X.

Lemma Aeq_sym (X Y:Acz) : Aeq X YAeq Y X.

Lemma Aeq_tra (X Y Z:Acz) : Aeq X YAeq Y ZAeq X Z.

Definition Ain (X Y:Acz) : Prop :=
match Y with
| Asup B g b, Aeq X (g b)

Lemma Ain_Asup A f (a:A) : Ain (f a) (Asup A f).

Lemma Ain_mor (X1 X2 Y1 Y2:Acz) : Aeq X1 X2Aeq Y1 Y2Ain X1 Y1Ain X2 Y2.

Definition ASubq (X Y:Acz) : Prop :=
z, Ain z XAin z Y.

Lemma Aeq_ext (X Y:Acz) : ASubq X YASubq Y XAeq X Y.

Lemma Ain_ind : (P:AczProp), ( X Y, Aeq X YP YP X) → ( X, ( x, Ain x XP x) → P X) → X, P X.

Definition AEmpty : Acz := Asup False (fun amatch a with end).

Definition AEps : (AczProp) → Acz := epsilon (inhabits AEmpty).

Lemma AEpsR (P:AczProp) : ( x:Acz, P x) → P (AEps P).

Lemma AEps_ext (P Q:AczProp) : ( x, P x Q x) → AEps P = AEps Q.

Definition N (X:Acz) : Acz := AEps (Aeq X).

Lemma Aeq_N (X:Acz) : Aeq X (N X).

Lemma N_idem (X:Acz) : N (N X) = N X.

Lemma Aeq_N_eq (X Y:Acz) : Aeq X YN X = N Y.

Lemma N_eq_Aeq (X Y:Acz) : N X = N YAeq X Y.

Definition set : Type := sig (fun XN X = X).

Definition NS (X:Acz) : set := exist (fun XN X = X) (N X) (N_idem X).

Lemma Aeq_p1_NS (X:Acz) : Aeq X (proj1_sig (NS X)).

Definition IN : setsetProp := fun X YAin (proj1_sig X) (proj1_sig Y).

Lemma Ain_IN_p1 (X Y:set) : Ain (proj1_sig X) (proj1_sig Y) → IN X Y.

Lemma Ain_IN_NS (X Y:Acz) : Ain X YIN (NS X) (NS Y).

Lemma Ain_IN_p1_NS X Y : Ain (proj1_sig X) YIN X (NS Y).

Lemma Ain_IN_NS_p1 X Y : Ain X (proj1_sig Y) → IN (NS X) Y.

Lemma IN_Ain_p1 (X Y:set) : IN X YAin (proj1_sig X) (proj1_sig Y).

Lemma IN_Ain_NS (X Y:Acz) : IN (NS X) (NS Y) → Ain X Y.

Lemma IN_Ain_p1_NS X Y : IN X (NS Y) → Ain (proj1_sig X) Y.

Lemma IN_Ain_NS_p1 X Y : IN (NS X) YAin X (proj1_sig Y).

Definition nIN (x y:set) : Prop := ¬IN x y.
Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).

Definition Subq (X Y:set) : Prop := z, z Xz Y.
Infix "⊆" := Subq (at level 70).

(*** subset_eq_compat from ProofIrrelevanceFacts doesn't work here because Acz is a Type, not a Set. I copied the proof from there changing Set to Type. ***)
Lemma subset_eq_compat_Type :
   (U:Type) (P:UProp) (x y:U) (p:P x) (q:P y),
    x = yexist P x p = exist P y q.

Lemma NS_p1_eq X : NS (proj1_sig X) = X.

Lemma Aeq_p1_NS_eq (X:set) (Y:Acz) : Aeq (proj1_sig X) YX = NS Y.

Lemma Aeq_p1_eq : X Y:set, Aeq (proj1_sig X) (proj1_sig Y) → X = Y.
intros X H1 Y H2 H3. simpl in H3. apply subset_eq_compat_Type.
rewrite <- H1. rewrite <- H2. now apply Aeq_N_eq.

(*** Extensionality ***)
Lemma set_ext : X Y, X YY XX = Y.

(*** Epsilon Induction (Foundation) ***)
Lemma eps_ind : (P:setProp), ( X, ( x, x XP x) → P X) → X, P X.

(*** Empty ***)
Definition empty : set := NS AEmpty.
Notation "∅" := empty.

Lemma emptyE : (x:set), x .

(*** Unordered Pairs ***)
Definition upair (x y : set) : set := NS (Asup bool (fun aif a then proj1_sig x else proj1_sig y)).
Notation "{ x , y }" := (upair x y).

Lemma upairAx : (x y z:set), z {x,y} z = x z = y.

(*** Unions -- a little tricky to get one of the matches to type check ***)
Definition union (x:set) :=
  NS (match (proj1_sig x) with
        | Asup A f
          Asup (sigT (fun a:Amatch (f a) with Asup B gB end))
               (fun abmatch ab with existT a bmatch (f a) as z return (match z with Asup B gB end) → Acz with Asup B gg end b end) end).
Notation "⋃" := union (at level 40).
Axiom unionAx : (x z:set), z x y, y x z y.

(*** Replacement (for functions) ***)
Definition repl (X:set) (f:setset) : set :=
NS (match (proj1_sig X) with Asup B gAsup B (fun bproj1_sig (f (NS (g b)))) end).
Notation "{ f | x ⋳ X }" := (repl X (fun x:setf)).
Lemma replAx : X f z, z {f x|x X} x, x X z = f x.

(*** Separation ***)
Definition sep (X:set) (P:setProp) : set :=
NS (match (proj1_sig X) with Asup A fAsup (sig (fun x:AP (NS (f x)))) (fun xpmatch xp with exist x pf x end) end).
Notation "{ x ⋳ X | P }" := (sep X (fun x:setP)).

Lemma sepAx : X P z, z {x X|P x} z X P z.

(*** Power Sets -- definition of Werner 97, using sep and impredicativity ***)
(*** Coq gives a universe inconsistency for this definition following Werner 97, although impredicativity should mean it's allowed. ***)
Definition power (X:set) : set :=
  NS (Asup (set -> Prop) (fun P => proj1_sig (sep X P))).

Definition power (X:set) : set :=
  NS (match proj1_sig X with Asup A fAsup (AProp) (fun PAsup (sig P) (fun xpmatch xp with exist x pf x end)) end).
Notation "℘" := power.
Lemma powerAx : (X:set), Y:set, Y X Y X.

(*** singleton definition ***)
Definition sing : setset := fun x{x,x}.

(*** binunion definition ***)
Definition binunion (X Y:set) := {X,Y}.

(*** infinity ***)
Fixpoint finord (n:nat) : set :=
  match n with
    | Oempty
    | S n'binunion (finord n') (sing (finord n'))

Definition omega : set := NS (Asup nat (fun nproj1_sig (finord n))).

Lemma infinity : X:set, X ( x, x Xbinunion x (sing x) X).

End ZFAcz.