[ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
| simplify; intros 3; split; intro; assumption
| simplify; intros 5; split; intro;
- [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
+ [ apply (fi ?? (f ??)) | apply (if ?? (f ??))] assumption
| simplify; intros 7; split; intro;
- [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
- [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
+ [ apply (if ?? (f1 ??)) | apply (fi ?? (f ??)) ]
+ [ apply (if ?? (f ??)) | apply (fi ?? (f1 ??)) ]
assumption]]
qed.
(* carr to avoid universe inconsistency *)
apply (λs1:carr A.λs3:carr C.∃s2:carr B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
| intros;
- split; intro; cases H (w H3); clear H; exists; [1,3: apply w ]
+ split; intro; cases e2 (w H3); clear e2; exists; [1,3: apply w ]
[ apply (. (e‡#)‡(#‡e1)); assumption
| apply (. ((e \sup -1)‡#)‡(#‡(e1 \sup -1))); assumption]]
| intros 8; split; intro H2; simplify in H2 ⊢ %;
split; assumption
|6,7: intros 5; unfold composition; simplify; split; intro;
unfold setoid1_of_setoid in x y; simplify in x y;
- [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+ [1,3: cases e (w H1); clear e; cases H1; clear H1; unfold;
[ apply (. (e ^ -1 : eq1 ? w x)‡#); assumption
| apply (. #‡(e : eq1 ? w y)); assumption]
|2,4: exists; try assumption; split;
apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
qed.
-(* the same as * for a basic pair *)
+(* the same as Rest for a basic pair *)
definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:carr V. x ♮r y → y ∈ S});
apply f; [ apply (if ?? (e ^ -1 ??)); | apply (if ?? (e ??)) ] assumption]
qed.
-(* the same as - for a basic pair *)
+(* the same as Ext for a basic pair *)
definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
intros; constructor 1;
[ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
*)
include "o-algebra.ma".
-
+axiom daemon: False.
definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → ORelation (SUBSETS o1) (SUBSETS o2).
intros;
constructor 1;
- [ constructor 1;
+ [ constructor 1;
[ apply (λU.image ?? t U);
| intros; apply (#‡e); ]
| constructor 1;