Library Continuum.ZF_Structures
Arguments id {_} / _.
Notation "f ∘ g" := (fun x ⇒ f (g x)).
Notation "x ` f ` y" := (f x y) (at level 5,
f at next level,
format "x ` f ` y",
only parsing).
Notation "n .+1" := (S n)
(at level 2, left associativity, format "n .+1").
Notation "n .+2" := (S (S n))
(at level 2, left associativity, format "n .+2").
Notation "n .+3" := (S (S (S n)))
(at level 2, left associativity, format "n .+3").
Notation "n .+4" := (S (S (S (S n))))
(at level 2, left associativity, format "n .+4").
Notation "n .+5" := (S (S (S (S (S n)))))
(at level 2, left associativity, format "n .+5").
Definition Is_Functional {A B} (R : A → B → Prop) :=
∀ x y y', R x y → R x y' → y = y'.
Definition Is_Well_Founded {A} (R : A → A → Prop) :=
∀ P : A → Prop,
(∀ x, (∀ y, R y x → P y) → P x) →
∀ x, P x.
Class ZF_Structure :=
build_zf_structure {
type_of_sets : Type;
element_relation_on_sets : type_of_sets → type_of_sets → Prop;
}.
Arguments element_relation_on_sets {_} _.
Arguments type_of_sets _ : clear implicits.
Coercion type_of_sets : ZF_Structure >-> Sortclass.
Section Classes.
Context `{S : ZF_Structure}.
Record Class :=
build_class {
element_predicate : S → Prop
}.
Definition element_relation (x : S) (A : Class) :=
element_predicate A x.
Arguments element_relation : simpl never.
Existing Class element_relation .
Definition full_class :=
build_class (fun _ ⇒ True).
Global Instance everything_is_in_full_class (x : S) :
element_relation x full_class.
Proof. unfold element_relation. cbn. tauto. Qed.
End Classes.
Arguments element_relation : simpl never.
Notation "`{ x | P }" := (build_class (fun x ⇒ P)) (at level 9, x at level 69).
Notation "x ∈ A" := (element_relation x A) (at level 70).
Notation "x ∉ A" := (¬ x ∈ A) (at level 70).
Notation "A ⊆ B" := (∀ x, x ∈ A → x ∈ B) (at level 70).
Coercion set_as_class {S : ZF_Structure} (A : S) : Class :=
`{ x | element_relation_on_sets x A }.
Definition Is_A_Set {S : ZF_Structure} (A : Class) :=
∃ B : S, ∀ x, x ∈ A ↔ x ∈ B.
Existing Class Is_A_Set.
Definition class_as_set
{S : ZF_Structure} (A : Class) {is_a_set : Is_A_Set A} : S.
Admitted.
Lemma in_class_as_set_iff
{S : ZF_Structure} (A : Class) {is_a_set : Is_A_Set A} (x : S) :
x ∈ class_as_set A ↔ x ∈ A.
Admitted.
Record Element_Of {S : ZF_Structure} (A : Class) :=
build_element {
element_value :> S;
element_property : element_value ∈ A
}.
Arguments build_element {_ _} _ _.
Arguments element_value {_ _} _.
Coercion Element_Of : Class >-> Sortclass.
Existing Instance element_property.
Notation element x := (build_element x _).
Lemma element_equality {S : ZF_Structure} {A : Class} {x y : A} :
x = y :> S ↔
x = y.
Admitted.
Section Encodings.
Context `{S : ZF_Structure}.
Class Encoding_Of (A : Type) :=
build_encoding {
encoding_carrier : Class;
encode : A → encoding_carrier;
decode : encoding_carrier → A;
decode_encode : ∀ x, decode (encode x) = x
}.
Arguments encoding_carrier {_} _.
Coercion encoding_carrier : Encoding_Of >-> Class.
Definition encoding_of (A : Type) {encoding : Encoding_Of A} :=
encoding.
Global Instance encoding_of_the_universe :
Encoding_Of S :=
build_encoding
S
full_class
(fun x : S ⇒ element x)
(fun x : full_class ⇒ x)
_.
Proof.
- reflexivity.
Defined.
Global Instance encoding_of_class (A : Class) : Encoding_Of A :=
build_encoding
A
A
(fun x ⇒ x)
(fun x ⇒ x)
(fun _ ⇒ eq_refl).
Global Instance encoding_of_set_is_a_set (A : S) :
Is_A_Set (encoding_of A).
Proof. ∃ A. reflexivity. Qed.
Record Class_Like :=
build_class_like {
class_like_type :> Type;
class_like_encoding : Encoding_Of class_like_type
}.
Global Existing Instance class_like_encoding.
Canonical Structure canonical_class_like
(A : Type) {encoding : Encoding_Of A} :
Class_Like :=
build_class_like A encoding.
End Encodings.