(* *)
(**************************************************************************)
-include "logic/connectives.ma".
+include "logic/equality.ma".
nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
-(* This is a projection! *)
-ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f].
interpretation "powerset" 'powerset A = (powerset A).
ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
-interpretation "overlaps" 'overlaps U V = (fun1 ??? (overlaps ?) U V).
-
-definition intersects:
- ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
- intros;
- constructor 1;
- [ apply (λU,V. {x | x ∈ U ∧ x ∈ V });
- intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1;
- | intros;
- split; intros 2; simplify in f ⊢ %;
- [ apply (. (#‡H)‡(#‡H1)); assumption
- | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
-qed.
-
-interpretation "intersects" 'intersects U V = (fun1 ??? (intersects ?) U V).
-
-definition union:
- ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
- intros;
- constructor 1;
- [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
- intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1
- | intros;
- split; intros 2; simplify in f ⊢ %;
- [ apply (. (#‡H)‡(#‡H1)); assumption
- | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
-qed.
-
-interpretation "union" 'union U V = (fun1 ??? (union ?) U V).
-
-definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
- intros; constructor 1;
- [ apply (λA:setoid.λa:A.{b | a=b});
- intros; simplify;
- split; intro;
- apply (.= H1);
- [ apply H | apply (H \sup -1) ]
- | intros; split; intros 2; simplify in f ⊢ %; apply trans;
- [ apply a |4: apply a'] try assumption; apply sym; assumption]
-qed.
-
-interpretation "singleton" 'singl a = (fun_1 ?? (singleton ?) a).
\ No newline at end of file
+interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
+
+ndefinition intersects ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∧ x ∈ V }.
+
+interpretation "intersects" 'intersects U V = (intersects ? U V).
+
+ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }.
+
+interpretation "union" 'union U V = (union ? U V).
+
+ndefinition singleton ≝ λA.λa:A.{b | a=b}.
+
+interpretation "singleton" 'singl a = (singleton ? a).