- A : Type[0], B,C : powerclass A ⊢
- fun21 …
- (mk_binary_morphism1 …
- (λS,S'.S ∩ S')
- (prop21 … (intersect_ok' A))) B C
- ≡ intersect ? B C.
-
-ndefinition prop21_mem :
- ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) C.
- ∀a,a':setoid1_of_setoid A.
- ∀b,b':qpowerclass_setoid A.a = a' → b = b' → f a b = f a' b'.
-#A; #C; #f; #a; #a'; #b; #b'; #H1; #H2; napply prop21; nassumption;
-nqed.
-
-interpretation "prop21 mem" 'prop2 l r = (prop21_mem ??????? l r).
-
-nlemma intersect_ok'':
- ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
- #A; @ (intersect_ok A); nlapply (prop21 … (intersect_ok' A)); #H;
- #a; #a'; #b; #b'; #H1; #H2; napply H; nassumption;
+ A : Type[0], B,C : Ω^A;
+ R ≟ (mk_unary_morphism1 …
+ (λS. mk_unary_morphism1 … (λS'.S ∩ S') (prop11 … (intersect_is_morph A S)))
+ (prop11 … (intersect_is_morph A)))
+ ⊢
+ R B C ≡ intersect ? B C.
+
+interpretation "prop21 ext" 'prop2 l r =
+ (prop11 (ext_powerclass_setoid ?)
+ (unary_morphism1_setoid1 (ext_powerclass_setoid ?) ?) ? ?? l ?? r).
+
+nlemma intersect_is_ext_morph:
+ ∀A. unary_morphism1 (ext_powerclass_setoid A)
+ (unary_morphism1_setoid1 (ext_powerclass_setoid A) (ext_powerclass_setoid A)).
+ #A; napply (mk_binary_morphism1 … (intersect_is_ext …));
+ #a; #a'; #b; #b'; #Ha; #Hb; napply (prop11 … (intersect_is_morph A)); nassumption.