- R ≟ (mk_binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A)
- (λS,S':carr1 (ext_powerclass_setoid A).
- mk_ext_powerclass A (S∩S') (ext_prop A (intersect_is_ext ? S S')))
- (prop21 … (intersect_is_ext_morph A))) ,
+ R ≟ (mk_unary_morphism1 …
+ (λS:ext_powerclass_setoid A.
+ mk_unary_morphism1 ??
+ (λS':ext_powerclass_setoid A.
+ mk_ext_powerclass A (S∩S') (ext_prop A (intersect_is_ext ? S S')))
+ (prop11 … (intersect_is_ext_morph A S)))
+ (prop11 … (intersect_is_ext_morph A))) ,