Stream: Coq users

Topic: Bridge between set theory and type theory


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip choukh (May 15 2022 at 02:41):

Yes, it works. Thank you so much!


Last updated: Feb 06 2023 at 12:04 UTC