o-basic_pairs are indeed examples of o-basic_topologies!

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / categories.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 0ac3b518baaacaab25f1869c24a26e096236a0e9..e22402d9f52542745b29e226597fe74a14920622 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -55,6 +55,7 @@ definition setoid1_of_setoid: setoid → setoid1.
 qed.
 
 coercion setoid1_of_setoid.
+prefer coercion Type_OF_setoid.
 
 definition reflexive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x:A.R x x.
 definition symmetric2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λC:Type2.λlt:C→C→CProp2. ∀x,y:C.lt x y → lt y x.
@@ -85,6 +86,10 @@ definition setoid2_of_setoid1: setoid1 → setoid2.
 qed.
 
 coercion setoid2_of_setoid1.
+prefer coercion Type_OF_setoid2. 
+prefer coercion Type_OF_setoid. 
+prefer coercion Type_OF_setoid1. 
+(* we prefer 0 < 1 < 2 *)
 
 interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y).
 interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
@@ -264,11 +269,6 @@ definition setoid_of_SET: objs1 SET → setoid.
  intros; apply o; qed.
 coercion setoid_of_SET.
 
-definition setoid1_of_SET: SET → setoid1.
- intro; whd in t; apply setoid1_of_setoid; apply t.
-qed.
-coercion setoid1_of_SET.
-
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
 
@@ -320,11 +320,14 @@ qed.
 coercion Type1_OF_SET1.
 
 definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply setoid1_of_SET; apply U
+ [ apply rule U; 
  | intros; apply c;]
 qed.
 coercion Type_OF_setoid1_of_carr.
 
+definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
+coercion carr'. (* we prefer the lower carrier projection *)
+
 interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
 
 lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.