first [apply refl | assumption]]]
qed.
-(*
definition full_subset: ∀s:REL. Ω \sup s.
apply (λs.{x | True});
intros; simplify; split; intro; assumption.
qed.
coercion full_subset.
-*)
definition setoid1_of_REL: REL → setoid ≝ λS. S.
coercion setoid1_of_REL.
qed.
coercion Type_OF_setoid1_of_REL.
-(*
-definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
- intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
+ intros; simplify;
+ alias symbol "trans" = "trans1".
+ alias symbol "prop1" = "prop11".
+ apply (.= †e); apply refl1.
qed.
interpretation "subset comprehension" 'comprehension s p =
- (comprehension s (mk_unary_morphism __ p _)).
+ (comprehension s (mk_unary_morphism1 __ p _)).
definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
- apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
- [ intros; simplify; apply (.= (H‡#)); apply refl1
- | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
- [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
- | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?);
+ [ intros; simplify; apply (.= (e‡#)); apply refl1
+ | intros; simplify; split; intros; simplify;
+ [ change with (∀x. x ♮a b → x ♮a' b'); intros;
+ apply (. (#‡e1)); whd in e; apply (if ?? (e ??)); assumption
+ | change with (∀x. x ♮a' b' → x ♮a b); intros;
+ apply (. (#‡e1\sup -1)); whd in e; apply (fi ?? (e ??));assumption]]
qed.
-
+(*
definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
(* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
intros (X S r); constructor 1;