## Stream: Coq users

### Topic: Bridge between set theory and type theory

#### 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.
∀ 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.
``````

#### Gaëtan Gilbert (May 14 2022 at 09:26):

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.
``````

#### choukh (May 15 2022 at 02:41):

Yes, it works. Thank you so much!

Last updated: Oct 03 2023 at 04:02 UTC