Add classes as records

[georgydunaev]

Due to uncertainty in using the raw (Ens->Prop) expression as a type of classes, I propose the next definition of the class with built-in soundness proof:

(* 'class' is the type of well-defined classes. *)
Record class := {
 prty :> Ens->Prop;
 sound : forall (a b : Ens), EQ a b -> (prty a <-> prty b);
}.

Definition EQC (A B:class) := forall z:Ens, A z <-> B z.

(* set to class *)
Definition stoc : Ens -> class.
Proof.
intro x.
unshelve eapply Build_class.
+ intro y. exact (IN y x).
+ intros a b aeqb. split.
  - apply IN_sound_left. exact aeqb.
  - apply IN_sound_left. apply EQ_sym. exact aeqb.
Defined.

Coercion stoc : Ens >-> class.

[herbelin]

Good idea.

I contacted Benjamin Werner to know his opinion on potential future extensions of zfc. I'll come back to you later.

[georgydunaev]

Good idea.

I contacted Benjamin Werner to know his opinion on potential future extensions of zfc. I'll come back to you later.

Thanks! I also tried, but I didn't succeed. (from georgedunaev@gmail.com)

One also may find useful my theorems from https://github.com/georgydunaev/Jech (My intention there is to verify Tomas Jech's "Set theory" book as long as I find it worth to be done. The important thing is that I want it to be 100% close to the theorems from the textbook. So I redefined ordered pair and cartesian product in the traditional way. I needn't yet to use classical axioms of logic as it mentioned in Cartesian.v)

[herbelin]

Hi @georgydunaev, I met Benjamin Werner who told me that he is ok with your projects of extension of zfc. So, we can continue interacting on the PR.

Besides, the project of formalizing Jech's book is a very nice project. I'm fully supporting you.