Hacky version of the Collection axiom

czf.v

@@ -1,5 +1,4 @@
 From stdpp Require Import base.
-From Coq Require Import Logic.PropExtensionality.
 
 (** * Cumulative hierarchy *)
 Inductive V : Type :=
@@ -205,6 +204,10 @@ Qed.
 
 (** * Axioms *)
 
+(** First, we define a class of set predicates: predicates that respect the equality on V *)
+Class SetPredicate (ϕ : V → Prop) :=
+  pred_proper :> Proper ((≡) ==> impl) ϕ.
+
 (** Extensionality *)
 Theorem CZF_extensionality (a b : V) :
   a ⊆ b ∧ b ⊆ a ↔ a ≡ b.
@@ -215,7 +218,7 @@ Proof.
 Qed.
 
 (** Paring *)
-Lemma CZF_pairing (x y : V) :
+Theorem CZF_pairing (x y : V) :
   forall (w : V), w ∈ ({[x; y]} : V)
                 ↔ w ≡ x ∨ w ≡ y.
 Proof.
@@ -230,13 +233,23 @@ Qed.
 (* TODO: need big union operation *)
 
 (** Empty set *)
-Lemma CZF_empty :
+Theorem CZF_empty :
   forall y, ¬ (y ∈ (∅ : V)).
 Proof. intros ? [[] ?]. Qed.
 
+(** Set Induction *)
+Theorem CZF_induction ϕ `{SetPredicate ϕ} :
+  (forall x, (forall y, y ∈ x → ϕ y) → ϕ x) → (forall x, ϕ x).
+Proof.
+  intros Hϕ x.
+  induction x as [A f IH].
+  apply Hϕ.
+  intros y [a ->]. apply IH.
+Qed.
+
 (** Infinity *)
 Definition suc (x : V) := x ∪ {[x]}.
-Lemma CZF_infinity :
+Theorem CZF_infinity :
   ∅ ∈ NN ∧ (forall y, y ∈ NN → suc y ∈ NN).
 Proof.
   split.
@@ -254,9 +267,8 @@ Proof.
   intros [x ?]. exact (f x).
 Defined.
 
-Class SetPredicate (ϕ : V → Prop) :=
+(* Note that we have non-restricted separation *)
-  pred_proper :> Proper ((≡) ==> impl) ϕ.
+Theorem CZF_separation a ϕ `{SetPredicate ϕ} :
-Lemma CZF_separation a ϕ `{SetPredicate ϕ} :
   forall y, (y ∈ sep a ϕ ↔ y ∈ a ∧ ϕ y).
 Proof.
   intros y. destruct a as [A f]. split.
@@ -266,3 +278,36 @@ Proof.
     rewrite Hx in Hϕ.
     exists (existT x Hϕ). assumption.
 Qed.
+
+(** Collection *)
+(** Collection holds only if we use types-as-proposition
+interpretation, by using Σ-types (landing in Type) instead of ∃
+(landing in Prop). Curiously, the predicate ϕ doesn't have to be
+proper. *)
+Definition coll (a : V) (ϕ : V → V → Prop) :
+  (forall (x : V), x ∈ a → { y | ϕ x y }) →
+  V.
+Proof.
+  intros Hϕ.
+  destruct a as [A f].
+  refine (sup A _).
+  intros x.
+  assert (f x ∈ sup A f) as Hfx. { exists x; reflexivity. }
+  exact (proj1_sig (Hϕ (f x) Hfx)).
+Defined.
+
+(* ∀a[∀x∈a ∃y φ(x,y) → ∃b∀x∈a ∃y∈b φ(x,y)]  *)
+Theorem CZF_collection (a : V) (ϕ : V → V → Prop)
+        `{Proper _ ((≡) ==> (≡) ==> (impl)) ϕ} :
+  (forall (x : V), x ∈ a → { y | ϕ x y }) →
+  exists (b : V), (forall (x : V), x ∈ a → exists y, y ∈ b ∧ ϕ x y ).
+Proof.
+  intros Hϕ.
+  exists (coll a ϕ Hϕ). intros xx Hxx.
+  destruct a as [A f].
+  destruct Hxx as [x Hx]. simpl in *.
+  set (Hϕ':=Hϕ (f x) (ex_intro (λ y, f x ≡ f y) x (reflexivity _))).
+  exists (proj1_sig Hϕ'). split.
+  2: { rewrite Hx. apply (proj2_sig Hϕ'). }
+  exists x. cbn. reflexivity.
+Qed.