choukh (May 14 2022 at 08:12): choukh (May 14 2022 at 08:12):Assume a type of set theory, i.e.
Axiom Class : Type.
Axiom In : Class -> Class -> Prop.
Axiom Extensionality : blabla.
(and some other set theory axioms)
what are the consequences of adding following axioms?
30D8B794-68F2-4CB9-BDED-AF735580ACA3.png
The motivation is that it may be easier to express something like
∀ f : TypeOfClass A → TypeOfClass B, blabla.
instead of
∀ f, is_function f → Domain f = A → Range f ⊆ B → blabla.
Gaëtan Gilbert (May 14 2022 at 09:23):no need to make them axioms
Axiom Class : Type.
Axiom In : Class -> Class -> Prop.
Notation "a ∈ b" := (In a b) (at level 43). (* NB: I picked a random level *)
Definition TypeOfClass X := { Y | Y ∈ X }.
Definition SetOfTerm {A} (X:TypeOfClass A) := proj1_sig X.
Definition TermToMembership {A} (t:TypeOfClass A) : SetOfTerm t ∈ A
:= proj2_sig t.
Definition MembershipToTerm {A a} (H:a ∈ A) : TypeOfClass A := exist _ a H.
Definition TermIdentity {A} (t:TypeOfClass A) : MembershipToTerm (TermToMembership t) = t.
Proof. destruct t;reflexivity. Qed.
Definition SetIdentity {A a} (H:a ∈ A) : SetOfTerm (MembershipToTerm H) = a
:= eq_refl.
alternatively
Set Primitive Projections.
Record TypeOfClass A := MakeType {
SetOfTerm : Class;
TermToMembership : SetOfTerm ∈ A;
}.
Arguments SetOfTerm {_} _.
Arguments TermToMembership {_} _.
Definition MembershipToTerm {A a} (H:a ∈ A) : TypeOfClass A := MakeType _ a H.
Definition TermIdentity {A} (t:TypeOfClass A) : MembershipToTerm (TermToMembership t) = t
:= eq_refl. (* works because primitive record *)
Definition SetIdentity {A a} (H:a ∈ A) : SetOfTerm (MembershipToTerm H) = a
:= eq_refl.
Yes, it works. Thank you so much!
Last updated: Oct 03 2023 at 04:02 UTC