(* qua non riesco a mettere set *)
definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
intros; constructor 1;
- [ apply (λa:A.{b | eq ? a b}); unfold setoid1_of_setoid; simplify;
+ [ apply (λa:A.{b | a =_0 b}); unfold setoid1_of_setoid; simplify;
intros; simplify;
split; intro;
apply (.= e1);
∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
intros; constructor 1;
[ intro; whd; whd in I;
- apply ({x | ∀i:I. x ∈ t 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;
∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
intros; constructor 1;
[ intro; whd; whd in A; whd in I;
- apply ({x | ∃i:I. x ∈ t 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;