(*
A quick demonstration of a shallow embedding of set theory in Coq.
See https://coq.inria.fr/doc/v8.9/stdlib/Coq.Sets.Ensembles.html
 *)

Parameter U : Type.

Definition Seti := U -> Prop.

Definition In (x : U) (X : Seti) : Prop := X x.

Notation "x ∈ X" := (In x X) (at level 65, no associativity).

Definition eq (X Y : Seti) : Prop :=
  forall x, x ∈ X <-> x ∈ Y.

Notation "X =s Y" := (eq X Y) (at level 85, no associativity).

Definition subset (X Y : Seti) : Prop :=
  forall x, x ∈ X -> x ∈ Y.

Notation "X ⊆ Y" := (subset X Y) (at level 75, no associativity).

Definition proper_subset (X Y : Seti) : Prop :=
  X ⊆ Y /\ ~ (X =s Y).

Definition union (X Y : Seti) : Seti :=
  fun u => (u ∈ X) \/ (u ∈ Y).

Definition intersect (X Y : Seti) : Seti :=
  fun u => (u ∈ X) /\ (u ∈ Y).