From 3da73646d19595dbbf6930c58971d6a1fde2bc57 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 12 Jun 2019 14:09:12 +0200
Subject: [PATCH] add big_union

---
 czf.v | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/czf.v b/czf.v
index 4d303d5..c0fa463 100644
--- a/czf.v
+++ b/czf.v
@@ -230,7 +230,28 @@ Proof.
 Qed.
 
 (** Union *)
-(* TODO: need big union operation *)
+Definition big_union (a : V) : V.
+Proof.
+  destruct a as [A f].
+  refine (sup { x : A & ind (f x) } _).
+  intros [x y]. apply (branch (f x) y).
+Defined.
+
+Theorem CZF_union (a : V) :
+  forall (x : V), x ∈ big_union a
+     ↔ exists (z : V), (x ∈ z ∧ z ∈ a).
+Proof.
+  intros x. split.
+  - destruct a as [A f].
+    intros [[a b] Hx]. simpl in *.
+    exists (f a). split.
+    + rewrite Hx. exists b. reflexivity.
+    + exists a. reflexivity.
+  - intros [z [[β Hx] [α Hz]]].
+    destruct a as [A f]. simpl in *.
+    assert ({x0 : A & ind (f x0)}).
+    exists α.
+Abort.
 
 (** Empty set *)
 Theorem CZF_empty :
@@ -263,7 +284,7 @@ Qed.
 Definition sep (a : V) (ϕ : V → Prop) : V.
 Proof.
   destruct a as [A f].
-  refine (sup (sigT (λ (x:A), ϕ (f x))) _).
+  refine (sup (sig (λ (x:A), ϕ (f x))) _).
   intros [x ?]. exact (f x).
 Defined.
 
@@ -276,7 +297,7 @@ Proof.
     rewrite Hx. split; [exists x|]; eauto.
   - intros [[x Hx] Hϕ]. simpl in *.
     rewrite Hx in Hϕ.
-    exists (existT x Hϕ). assumption.
+    exists (exist _ x Hϕ). assumption.
 Qed.
 
 (** Collection *)
@@ -327,3 +348,6 @@ Proof.
   set (Hϕ':=Hϕ (f y) (ex_intro (λ z, f y ≡ f z) y (reflexivity _))).
   apply (proj2_sig Hϕ').
 Qed.
+
+(** Subset collection *)
+(* ... *)