+interpretation "singleton" 'singl a = (fun11 ?? (singleton ?) a).
+notation > "{ term 19 a : S }" with precedence 90 for @{fun11 ?? (singleton $S) $a}.
+
+definition big_intersects: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
+ intros; constructor 1;
+ [ intro; whd; whd in I;
+ apply ({x | ∀i:I. x ∈ c i});
+ simplify; intros; split; intros; [ apply (. (e^-1‡#)); | apply (. e‡#); ]
+ apply f;
+ | intros; split; intros 2; simplify in f ⊢ %; intro;
+ [ apply (. (#‡(e i)^-1)); apply f;
+ | apply (. (#‡e i)); apply f]]
+qed.
+
+definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
+ intros; constructor 1;
+ [ intro; whd; whd in A; whd in I;
+ apply ({x | ∃i:I. x ∈ c i });
+ simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
+ [ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
+ apply x;
+ | intros; split; intros 2; simplify in f ⊢ %; cases f; clear f; exists; [1,3:apply w]
+ [ apply (. (#‡(e w)^-1)); apply x;
+ | apply (. (#‡e w)); apply x]]
+qed.
+
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (\emsp) term 90 p)"
+non associative with precedence 50 for @{ 'bigcup $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (ident i ∈ I) break term 90 p)"
+non associative with precedence 50 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋃ f)" non associative with precedence 60 for @{ 'bigcup $f }.
+
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (\emsp) term 90 p)"
+non associative with precedence 50 for @{ 'bigcap $p }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (ident i ∈ I) break term 90 p)"
+non associative with precedence 50 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋂ f)" non associative with precedence 60 for @{ 'bigcap $f }.
+
+interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f).
+interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).
+interpretation "bigcup mk" 'bigcup_mk f = (fun12 ?? (big_union ??) (mk_unary_morphism2 ?? f ?)).
+interpretation "bigcap mk" 'bigcap_mk f = (fun12 ?? (big_intersects ??) (mk_unary_morphism2 ?? f ?)).