definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
coercion powerset_of_POW'.
-definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (POW' o1) (POW' o2).
+definition orelation_of_relation: ∀o1,o2:REL. o1 ⇒_\r1 o2 → (POW' o1) ⇒_\o2 (POW' o2).
intros;
constructor 1;
[ constructor 1;
qed.
lemma orelation_of_relation_preserves_equality:
- ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2.
+ ∀o1,o2:REL.∀t,t': o1 ⇒_\r1 o2.
t = t' → orelation_of_relation ?? t =_2 orelation_of_relation ?? t'.
intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
simplify; whd in o1 o2;
alias symbol "eq" = "setoid2 eq".
alias symbol "compose" = "category1 composition".
lemma orelation_of_relation_preserves_composition:
- ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
+ ∀o1,o2,o3:REL.∀F: o1 ⇒_\r1 o2.∀G: o2 ⇒_\r1 o3.
orelation_of_relation ?? (G ∘ F) =
comp2 OA ??? (orelation_of_relation ?? F) (orelation_of_relation ?? G).
intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros;
theorem POW_faithful:
∀S,T.∀f,g:arrows2 (category2_of_category1 REL) S T.
- map_arrows2 ?? POW ?? f = map_arrows2 ?? POW ?? g → f = g.
+ POW⎽⇒ f =_2 POW⎽⇒ g → f =_2 g.
intros; unfold POW in e; simplify in e; cases e;
unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4;
intros 2; cases (e3 {(x)});
intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
qed.
-(*
-interpretation "lifting singl" 'singl x =
- (fun11 ? (objs2 (POW ?)) (singleton ?) x).
-*)
-
-
-theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
+theorem POW_full: ∀S,T.∀f: (POW S) ⇒_\o2 (POW T) . exT22 ? (λg. POW⎽⇒ g = f).
intros; exists;
[ constructor 1; constructor 1;
[ apply (λx:carr S.λy:carr T. y ∈ f {(x)});