Separation axiom

czf.v

@@ -196,3 +196,61 @@ Proof.
     destruct (HBA (g y) Hgy) as [x Hx].
     exists x. symmetry. apply Hx.
 Qed.
+
+(** * Axioms *)
+
+(** Extensionality *)
+(* ... *)
+
+(** Paring *)
+Lemma CZF_pairing (x y : V) :
+  forall (w : V), w ∈ ({[x; y]} : V)
+                ↔ w ≡ x ∨ w ≡ y.
+Proof.
+  intros w. split.
+  - intros [[?|?] ?]; eauto.
+  - intros [Hw|Hw].
+    + exists (inl ()). eauto.
+    + exists (inr ()). eauto.
+Qed.
+
+(** Union *)
+(* TODO: need big union operation *)
+
+(** Empty set *)
+Lemma CZF_empty :
+  forall y, ¬ (y ∈ (∅ : V)).
+Proof. intros ? [[] ?]. Qed.
+
+(** Infinity *)
+Definition suc (x : V) := x ∪ {[x]}.
+Lemma CZF_infinity :
+  ∅ ∈ NN ∧ (forall y, y ∈ NN → suc y ∈ NN).
+Proof.
+  split.
+  - exists 0. reflexivity.
+  - intros y [n Hn]. exists (S n).
+    unfold suc. rewrite Hn.
+    reflexivity.
+Qed.
+
+(** Separation *)
+Definition sep (a : V) (ϕ : V → Prop) : V.
+Proof.
+  destruct a as [A f].
+  refine (sup (sigT (λ (x:A), ϕ (f x))) _).
+  intros [x ?]. exact (f x).
+Defined.
+
+Class SetPredicate (ϕ : V → Prop) :=
+  pred_proper :> Proper ((≡) ==> impl) ϕ.
+Lemma CZF_separation a ϕ `{SetPredicate ϕ} :
+  forall y, (y ∈ sep a ϕ ↔ y ∈ a ∧ ϕ y).
+Proof.
+  intros y. destruct a as [A f]. split.
+  - intros [[x Hϕ] Hx]. simpl in *.
+    rewrite Hx. split; [exists x|]; eauto.
+  - intros [[x Hx] Hϕ]. simpl in *.
+    rewrite Hx in Hϕ.
+    exists (existT x Hϕ). assumption.
+Qed.