include "categories.ma".
-record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
+record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: A ⇒_1 CPROP }.
+interpretation "powerset low" 'powerset A = (powerset_carrier A).
+notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
+interpretation "memlow" 'mem_low a S = (mem_operator ? S a).
-definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp0 ≝
- λA:objs1 SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
+definition subseteq_operator: ∀A: objs1 SET. Ω^A → Ω^A → CProp0 ≝
+ λA:objs1 SET.λU,V.∀a:A. a ∈. U → a ∈. V.
theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
intros 6; intros 2;
interpretation "subset construction" 'subset \eta.x =
(mk_powerset_carrier ? (mk_unary_morphism1 ? CPROP x ?)).
-definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
+definition mem: ∀A. A × Ω^A ⇒_1 CPROP.
intros;
constructor 1;
[ apply (λx,S. mem_operator ? S x)
interpretation "mem" 'mem a S = (fun21 ??? (mem ?) a S).
-definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+definition subseteq: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
intros;
constructor 1;
[ apply (λU,V. subseteq_operator ? U V)
interpretation "subseteq" 'subseteq U V = (fun21 ??? (subseteq ?) U V).
-
-
-theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
+theorem subseteq_refl: ∀A.∀S:Ω^A.S ⊆ S.
intros 4; assumption.
qed.
-theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
+theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω^A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
intros; apply transitive_subseteq_operator; [apply S2] assumption.
qed.
-definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+definition overlaps: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
intros;
constructor 1;
- (* Se metto x al posto di ? ottengo una universe inconsistency *)
- [ apply (λA:objs1 SET.λU,V:Ω \sup A.(exT2 ? (λx:A.?(*x*) ∈ U) (λx:A.?(*x*) ∈ V) : CProp0))
+ [ apply (λA:objs1 SET.λU,V:Ω^A.(exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V) : CProp0))
| intros;
constructor 1; intro; cases e2; exists; [1,4: apply w]
[ apply (. #‡e^-1); assumption
interpretation "overlaps" 'overlaps U V = (fun21 ??? (overlaps ?) U V).
-definition intersects:
- ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
+definition intersects: ∀A. Ω^A × Ω^A ⇒_1 Ω^A.
intros;
constructor 1;
[ apply rule (λU,V. {x | x ∈ U ∧ x ∈ V });
interpretation "intersects" 'intersects U V = (fun21 ??? (intersects ?) U V).
-definition union:
- ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
+definition union: ∀A. Ω^A × Ω^A ⇒_1 Ω^A.
intros;
constructor 1;
[ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
interpretation "union" 'union U V = (fun21 ??? (union ?) U V).
(* qua non riesco a mettere set *)
-definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
+definition singleton: ∀A:setoid. A ⇒_1 Ω^A.
intros; constructor 1;
[ apply (λa:A.{b | a =_0 b}); unfold setoid1_of_setoid; simplify;
intros; simplify;
qed.
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.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup 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});
| apply (. (#‡e i)); apply f]]
qed.
-definition big_union:
- ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+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 });