CAT2

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations_to_o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 3317c0e64672b220864f8c975903cdfe61163286..a7041357af3a0cffd16f257a87008e4be21aac7f 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -157,3 +157,17 @@ lemma orelation_of_relation_preserves_composition:
   | whd; intros; apply f; exists; [ apply y] split; assumption;
   | cases f1; clear f1; cases x; clear x; apply (f w); assumption;]
 qed.
+
+definition SUBSETS': carr3 (arrows3 CAT2 (category2_of_category1 REL) OA).
+ constructor 1;
+  [ apply SUBSETS;
+  | intros; constructor 1;
+     [ apply (orelation_of_relation S T);
+     | intros; apply (orelation_of_relation_preserves_equality S T a a' e); ]
+  | apply orelation_of_relation_preserves_identity;
+  | simplify; intros;
+    apply (.= (orelation_of_relation_preserves_composition o1 o2 o4 f1 (f3∘f2)));
+    apply (#‡(orelation_of_relation_preserves_composition o2 o3 o4 f2 f3)); ]
+qed.
+    
+    
\ No newline at end of file