-definition singleton: ∀A:setoid. A → Ω \sup A.
- apply (λA:setoid.λa:A.{b | a=b});
- intros; simplify;
- split; intro;
- apply (.= H1);
- [ apply H | apply (H \sup -1) ]
+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]