From c8718cc46ab9aaca047366dfefe72bc7c9402e5a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 4 Mar 2012 19:23:00 +0000
Subject: [PATCH] - lambda_delta: "conversion" and "equivalence" components
 started - formal_topology: porting to lib started. cprop_connectives
 compiles!

---
 .../contribs/lambda_delta/Basic_2/Basic_1.txt |   3 +-
 .../lambda_delta/Basic_2/conversion/cpc.ma    |  37 +++
 .../Basic_2/conversion/cpc_cpc.ma             |  23 ++
 .../lambda_delta/Basic_2/equivalence/cpcs.ma  |  47 +++
 matita/matita/contribs/lambda_delta/Makefile  |  64 ++--
 matita/matita/lib/basics/pts.ma               |   1 +
 .../formal_topology/apply_functor.ma          |   4 +-
 .../formal_topology/basic_pairs.ma            |   4 +-
 .../basic_pairs_to_basic_topologies.ma        |   2 +-
 .../basic_pairs_to_o-basic_pairs.ma           |   0
 .../formal_topology/basic_topologies.ma       |   4 +-
 .../basic_topologies_to_o-basic_topologies.ma |   0
 .../formal_topology/categories.ma             | 291 +++++++++---------
 .../formal_topology/concrete_spaces.ma        |   4 +-
 .../concrete_spaces_to_o-concrete_spaces.ma   |   0
 .../formal_topology/cprop_connectives.ma      | 114 +++----
 .../formal_topology/formal_topologies.ma      |   0
 .../formal_topology/notation.ma               |   0
 .../formal_topology/o-algebra.ma              |   8 +-
 .../formal_topology/o-basic_pairs.ma          |   4 +-
 .../o-basic_pairs_to_o-basic_topologies.ma    |   0
 .../formal_topology/o-basic_topologies.ma     |   4 +-
 .../formal_topology/o-concrete_spaces.ma      |   4 +-
 .../formal_topology/o-formal_topologies.ma    |   0
 .../formal_topology/o-saturations.ma          |   4 +-
 .../formal_topology/r-o-basic_pairs.ma        |   2 +-
 .../formal_topology/relations.ma              |   2 +-
 .../formal_topology/relations_to_o-algebra.ma |   0
 matita/matita/lib/formal_topology/replace.sh  |  10 +
 .../formal_topology/saturations.ma            |   4 +-
 .../saturations_to_o-saturations.ma           |   0
 .../formal_topology/subsets.ma                |   6 +-
 matita/matita/predefined_virtuals.ml          |   2 +-
 33 files changed, 375 insertions(+), 273 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc.ma
 create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc_cpc.ma
 create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/equivalence/cpcs.ma
 rename matita/matita/{library => lib}/formal_topology/apply_functor.ma (98%)
 rename matita/matita/{library => lib}/formal_topology/basic_pairs.ma (98%)
 rename matita/matita/{library => lib}/formal_topology/basic_pairs_to_basic_topologies.ma (97%)
 rename matita/matita/{library => lib}/formal_topology/basic_pairs_to_o-basic_pairs.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/basic_topologies.ma (98%)
 rename matita/matita/{library => lib}/formal_topology/basic_topologies_to_o-basic_topologies.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/categories.ma (73%)
 rename matita/matita/{library => lib}/formal_topology/concrete_spaces.ma (98%)
 rename matita/matita/{library => lib}/formal_topology/concrete_spaces_to_o-concrete_spaces.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/cprop_connectives.ma (55%)
 rename matita/matita/{library => lib}/formal_topology/formal_topologies.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/notation.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/o-algebra.ma (99%)
 rename matita/matita/{library => lib}/formal_topology/o-basic_pairs.ma (98%)
 rename matita/matita/{library => lib}/formal_topology/o-basic_pairs_to_o-basic_topologies.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/o-basic_topologies.ma (98%)
 rename matita/matita/{library => lib}/formal_topology/o-concrete_spaces.ma (99%)
 rename matita/matita/{library => lib}/formal_topology/o-formal_topologies.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/o-saturations.ma (93%)
 rename matita/matita/{library => lib}/formal_topology/r-o-basic_pairs.ma (99%)
 rename matita/matita/{library => lib}/formal_topology/relations.ma (99%)
 rename matita/matita/{library => lib}/formal_topology/relations_to_o-algebra.ma (100%)
 create mode 100644 matita/matita/lib/formal_topology/replace.sh
 rename matita/matita/{library => lib}/formal_topology/saturations.ma (92%)
 rename matita/matita/{library => lib}/formal_topology/saturations_to_o-saturations.ma (100%)
 rename matita/matita/{library => lib}/formal_topology/subsets.ma (98%)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
index 5e2e3d961..54f20be57 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
@@ -184,6 +184,7 @@ pc1/props pc1_head_2
 pc1/props pc1_t
 pc1/props pc1_pr0_u2
 pc1/props pc1_head
+
 pc3/dec pc3_dec
 pc3/dec pc3_abst_dec
 pc3/fsubst0 pc3_pr2_fsubst0
@@ -205,13 +206,11 @@ pc3/left pc3_ind_left
 pc3/nf2 pc3_nf2
 pc3/nf2 pc3_nf2_unfold
 pc3/pc1 pc3_pc1
-pc3/props clear_pc3_trans
 pc3/props pc3_pr2_r
 pc3/props pc3_pr2_x
 pc3/props pc3_pr3_r
 pc3/props pc3_pr3_x
 pc3/props pc3_pr3_t
-pc3/props pc3_refl
 pc3/props pc3_s
 pc3/props pc3_thin_dx
 pc3/props pc3_head_1
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc.ma b/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc.ma
new file mode 100644
index 000000000..e3058349b
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc.ma
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************)
+
+definition cpc: lenv → relation term ≝
+   λL,T1,T2. L ⊢ T1 ➡ T2 ∨ L ⊢ T2 ➡ T1.
+
+interpretation
+   "context-sensitive parallel conversion (term)"
+   'PConv L T1 T2 = (cpc L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cpc_refl: ∀L,T. L ⊢ T ⬌ T.
+/2 width=1/ qed.
+
+lemma cpc_sym: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → L ⊢ T2 ⬌ T1.
+#L #T1 #T2 * /2 width=1/
+qed.
+
+lemma cpc_cpr: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T.
+#L #T1 #T2 * /2 width=3/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc_cpc.ma
new file mode 100644
index 000000000..b4920c35c
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc_cpc.ma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/conversion/cpc.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************)
+
+(* Main properties **********************************************************)
+
+theorem cpc_conf: ∀L,T0,T1,T2. L ⊢ T0 ⬌ T1 → L ⊢ T0 ⬌ T2 →
+                  ∃∃T. L ⊢ T1 ⬌ T & L ⊢ T2 ⬌ T.
+/3 width=3/ qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambda_delta/Basic_2/equivalence/cpcs.ma
new file mode 100644
index 000000000..6004ee539
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/equivalence/cpcs.ma
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/conversion/cpc.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+definition cpcs: lenv → relation term ≝
+                 λL. TC … (cpc L).
+
+interpretation "context-sensitive parallel equivalence (term)"
+   'PConvStar L T1 T2 = (cpcs L T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma cpcs_ind: ∀L,T1. ∀R:predicate term. R T1 →
+                (∀T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → R T → R T2) →
+                ∀T2. L ⊢ T1 ⬌* T2 → R T2.
+#L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: pc3_refl *)
+lemma cpcs_refl: ∀L,T. L ⊢ T ⬌* T.
+/2 width=1/ qed.
+
+lemma cpcs_strap1: ∀L,T1,T,T2.
+                   L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
+/2 width=3/ qed.
+
+lemma cpcs_strap2: ∀L,T1,T,T2.
+                   L ⊢ T1 ⬌ T → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
+/2 width=3/ qed.
+
+(* Basic_1: removed theorems 1: clear_pc3_trans *)
diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index 3ce097690..b90b52178 100644
--- a/matita/matita/contribs/lambda_delta/Makefile
+++ b/matita/matita/contribs/lambda_delta/Makefile
@@ -25,15 +25,6 @@ stats: $(PACKAGES:%=%.stats)
 
 %.stats: CHARS = $(shell cat $(MAS) | wc -c)
 
-%.stats: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l)
-%.stats: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l)
-%.stats: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l)
-%.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l)
-%.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l)
-%.stats: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l)
-
-%.stats: TBL = ld_$*_sum
-
 %.stats:
 	@printf '\x1B[1;40;37m'
 	@printf '%-15s %-42s' 'Statistics for:' $*	
@@ -67,22 +58,39 @@ stats: $(PACKAGES:%=%.stats)
 	@printf '   %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
 	@printf '   %-10s' ''
 	@printf '\x1B[0m\n'
-	@printf 'name "$(TBL)"\n\n'                      > $*/$(TBL).tbl
-	@printf 'table {\n'                             >> $*/$(TBL).tbl
-	@printf '   class "grey" [ "category"\n'        >> $*/$(TBL).tbl
-	@printf '      [ "objects" * ]\n'               >> $*/$(TBL).tbl
-	@printf '   ]\n'                                >> $*/$(TBL).tbl
-	@printf '   class "green" [ "propositions"\n'   >> $*/$(TBL).tbl
-	@printf '      [ "theorems" "$(P1)" * ]\n'      >> $*/$(TBL).tbl
-	@printf '      [ "lemmas"   "$(P2)" * ]\n'      >> $*/$(TBL).tbl
-	@printf '      [ "total"    "$(P3)" * ]\n'      >> $*/$(TBL).tbl
-	@printf '   ]\n'                                >> $*/$(TBL).tbl
-	@printf '   class "yellow" [ "concepts"\n'      >> $*/$(TBL).tbl
-	@printf '      [ "declared" "$(C1)" * ]\n'      >> $*/$(TBL).tbl
-	@printf '      [ "defined"  "$(C2)" * ]\n'      >> $*/$(TBL).tbl
-	@printf '      [ "total"    "$(C3)" * ]\n'      >> $*/$(TBL).tbl
-	@printf '   ]\n'                                >> $*/$(TBL).tbl
-	@printf '}\n\n'                                 >> $*/$(TBL).tbl
-	@printf 'class "component" { 0 }\n\n'           >> $*/$(TBL).tbl
-	@printf 'class "plane" { 1 } { 3 } { 5 } \n\n'  >> $*/$(TBL).tbl
-	@printf 'class "number" { 2 } { 4 } { 6 } \n\n' >> $*/$(TBL).tbl
+
+# sum ########################################################################
+
+tbls: $(PACKAGES:%=etc/ld_%_sum.tbl)
+
+etc/ld_%_sum.tbl: MAS = $(shell find $* -name "*.ma")
+
+%.tbl: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l)
+%.tbl: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l)
+%.tbl: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l)
+%.tbl: P1 = $(shell grep "theorem " $(MAS) | wc -l)
+%.tbl: P2 = $(shell grep "lemma " $(MAS) | wc -l)
+%.tbl: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l)
+
+etc/ld_%_sum.tbl: $(MAS)
+	@mkdir -p etc
+	@printf 'Summary for: $*\n'
+	@printf 'name "$(basename $(@F))"\n\n'         >  $@
+	@printf 'table {\n'                            >> $@
+	@printf '   class "grey" [ "category"\n'       >> $@
+	@printf '      [ "objects" * ]\n'              >> $@
+	@printf '   ]\n'                               >> $@
+	@printf '   class "green" [ "propositions"\n'  >> $@
+	@printf '      [ "theorems" "$(P1)" * ]\n'     >> $@
+	@printf '      [ "lemmas"   "$(P2)" * ]\n'     >> $@
+	@printf '      [ "total"    "$(P3)" * ]\n'     >> $@
+	@printf '   ]\n'                               >> $@
+	@printf '   class "yellow" [ "concepts"\n'     >> $@
+	@printf '      [ "declared" "$(C1)" * ]\n'     >> $@
+	@printf '      [ "defined"  "$(C2)" * ]\n'     >> $@
+	@printf '      [ "total"    "$(C3)" * ]\n'     >> $@
+	@printf '   ]\n'                               >> $@
+	@printf '}\n\n'                                >> $@
+	@printf 'class "component" { 0 }\n\n'          >> $@
+	@printf 'class "plane" { 1 } { 3 } { 5 }\n\n'  >> $@
+	@printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $@
diff --git a/matita/matita/lib/basics/pts.ma b/matita/matita/lib/basics/pts.ma
index 446305ecf..237c0c2b3 100644
--- a/matita/matita/lib/basics/pts.ma
+++ b/matita/matita/lib/basics/pts.ma
@@ -19,3 +19,4 @@ universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
 universe constraint Type[4] < Type[5].
+universe constraint Type[5] < Type[6].
diff --git a/matita/matita/library/formal_topology/apply_functor.ma b/matita/matita/lib/formal_topology/apply_functor.ma
similarity index 98%
rename from matita/matita/library/formal_topology/apply_functor.ma
rename to matita/matita/lib/formal_topology/apply_functor.ma
index 89f3400a2..41e242caa 100644
--- a/matita/matita/library/formal_topology/apply_functor.ma
+++ b/matita/matita/lib/formal_topology/apply_functor.ma
@@ -15,7 +15,7 @@
 include "formal_topology/categories.ma".
 include "formal_topology/notation.ma".
 
-record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type2 ≝ {
+record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type[2] ≝ {
   F2: C2;
   F1: C1;
   FP: map_objs2 ?? F F1 =_\ID F2
@@ -36,7 +36,7 @@ intros 5; cases X; cases Y; clear X Y;
 cases H; cases H1; intros; assumption;
 qed.           
 
-record Fm_c (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) (X,Y:Fo ?? F) : Type2 ≝ {
+record Fm_c (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) (X,Y:Fo ?? F) : Type[2] ≝ {
   Fm2: arrows2 C2 (F2 ??? X) (F2 ??? Y);
   Fm1: arrows2 C1 (F1 ??? X) (F1 ??? Y);
   FmP: REW ?? F X Y (map_arrows2 ?? F ?? Fm1) = Fm2
diff --git a/matita/matita/library/formal_topology/basic_pairs.ma b/matita/matita/lib/formal_topology/basic_pairs.ma
similarity index 98%
rename from matita/matita/library/formal_topology/basic_pairs.ma
rename to matita/matita/lib/formal_topology/basic_pairs.ma
index ecf27345d..ff4085554 100644
--- a/matita/matita/library/formal_topology/basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/basic_pairs.ma
@@ -15,14 +15,14 @@
 include "formal_topology/relations.ma".
 include "formal_topology/notation.ma".
 
-record basic_pair: Type1 ≝ { 
+record basic_pair: Type[1] ≝ { 
    concr: REL; form: REL; rel: concr ⇒_\r1 form
 }.
 
 interpretation "basic pair relation" 'Vdash2 x y c = (fun21 ??? (rel c) x y).
 interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
 
-record relation_pair (BP1,BP2: basic_pair): Type1 ≝ { 
+record relation_pair (BP1,BP2: basic_pair): Type[1] ≝ { 
    concr_rel: (concr BP1) ⇒_\r1 (concr BP2); form_rel: (form BP1) ⇒_\r1 (form BP2);
    commute: comp1 REL ??? concr_rel (rel ?) =_1 form_rel ∘ ⊩
  }.
diff --git a/matita/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma b/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma
similarity index 97%
rename from matita/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
rename to matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma
index fb8891613..c236dc6a8 100644
--- a/matita/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma
@@ -42,7 +42,7 @@ qed.
 
 alias symbol "compose" (instance 3) = "category1 composition".
 alias symbol "compose" (instance 3) = "category1 composition".
-record functor1 (C1: category1) (C2: category1) : Type2 ≝
+record functor1 (C1: category1) (C2: category1) : Type[2] ≝
  { map_objs1:1> C1 → C2;
    map_arrows1: ∀S,T. unary_morphism1 (arrows1 ? S T) (arrows1 ? (map_objs1 S) (map_objs1 T));
    respects_id1: ∀o:C1. map_arrows1 ?? (id1 ? o) =_1 id1 ? (map_objs1 o);
diff --git a/matita/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma b/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma
similarity index 100%
rename from matita/matita/library/formal_topology/basic_pairs_to_o-basic_pairs.ma
rename to matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma
diff --git a/matita/matita/library/formal_topology/basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies.ma
similarity index 98%
rename from matita/matita/library/formal_topology/basic_topologies.ma
rename to matita/matita/lib/formal_topology/basic_topologies.ma
index 0177afb63..3b1e2e577 100644
--- a/matita/matita/library/formal_topology/basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_topologies.ma
@@ -15,7 +15,7 @@
 include "formal_topology/relations.ma".
 include "formal_topology/saturations.ma".
 
-record basic_topology: Type1 ≝
+record basic_topology: Type[1] ≝
  { carrbt:> REL;
    A: Ω^carrbt ⇒_1 Ω^carrbt;
    J: Ω^carrbt ⇒_1 Ω^carrbt;
@@ -24,7 +24,7 @@ record basic_topology: Type1 ≝
    compatibility: ∀U,V. (A U ≬ J V) =_1 (U ≬ J V)
  }.
 
-record continuous_relation (S,T: basic_topology) : Type1 ≝
+record continuous_relation (S,T: basic_topology) : Type[1] ≝
  { cont_rel:> S ⇒_\r1 T;
    reduced: ∀U. U =_1 J ? U → image_coercion ?? cont_rel U =_1 J ? (image_coercion ?? cont_rel U);
    saturated: ∀U. U =_1 A ? U → (cont_rel)⎻* U = _1A ? ((cont_rel)⎻* U)
diff --git a/matita/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
similarity index 100%
rename from matita/matita/library/formal_topology/basic_topologies_to_o-basic_topologies.ma
rename to matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
diff --git a/matita/matita/library/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma
similarity index 73%
rename from matita/matita/library/formal_topology/categories.ma
rename to matita/matita/lib/formal_topology/categories.ma
index 015e245f3..f5437449a 100644
--- a/matita/matita/library/formal_topology/categories.ma
+++ b/matita/matita/lib/formal_topology/categories.ma
@@ -14,92 +14,97 @@
 
 include "formal_topology/cprop_connectives.ma".
 
+inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝
+    refl: eq A x x.
+
 notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
 for @{ 'eqID $a $b }.
 
 notation > "hvbox(a break =_\ID b)" non associative with precedence 45
-for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
+for @{ 'eqID ? $a $b }.
 
-interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
+interpretation "ID eq" 'eqID x y = (eq ? x y).
 
-record equivalence_relation (A:Type0) : Type1 ≝
- { eq_rel:2> A → A → CProp0;
+record equivalence_relation (A:Type[0]) : Type[1] ≝
+ { eq_rel:2> A → A → CProp[0];
    refl: reflexive ? eq_rel;
    sym: symmetric ? eq_rel;
    trans: transitive ? eq_rel
  }.
 
-record setoid : Type1 ≝
- { carr:> Type0;
+record setoid : Type[1] ≝
+ { carr:> Type[0];
    eq: equivalence_relation carr
  }.
 
-record equivalence_relation1 (A:Type1) : Type2 ≝
- { eq_rel1:2> A → A → CProp1;
+record equivalence_relation1 (A:Type[1]) : Type[2] ≝
+ { eq_rel1:2> A → A → CProp[1];
    refl1: reflexive1 ? eq_rel1;
    sym1: symmetric1 ? eq_rel1;
    trans1: transitive1 ? eq_rel1
  }.
 
-record setoid1: Type2 ≝
- { carr1:> Type1;
+record setoid1: Type[2] ≝
+ { carr1:> Type[1];
    eq1: equivalence_relation1 carr1
  }.
 
 definition setoid1_of_setoid: setoid → setoid1.
- intro;
- constructor 1;
-  [ apply (carr s)
-  | constructor 1;
-    [ apply (eq_rel s);
-      apply (eq s)
-    | apply (refl s)
-    | apply (sym s)
-    | apply (trans s)]]
+ #s
+  @mk_setoid1
+  [ @(carr s)
+  | @mk_equivalence_relation1
+    [ @(eq_rel s)
+      @(eq s)
+    | @(refl s)
+    | @(sym s)
+    | @(trans s)]]
 qed.
 
 coercion setoid1_of_setoid.
+(*
 prefer coercion Type_OF_setoid.
-
-record equivalence_relation2 (A:Type2) : Type3 ≝
- { eq_rel2:2> A → A → CProp2;
+*)
+record equivalence_relation2 (A:Type[2]) : Type[3] ≝
+ { eq_rel2:2> A → A → CProp[2];
    refl2: reflexive2 ? eq_rel2;
    sym2: symmetric2 ? eq_rel2;
    trans2: transitive2 ? eq_rel2
  }.
 
-record setoid2: Type3 ≝
- { carr2:> Type2;
+record setoid2: Type[3] ≝
+ { carr2:> Type[2];
    eq2: equivalence_relation2 carr2
  }.
 
 definition setoid2_of_setoid1: setoid1 → setoid2.
- intro;
- constructor 1;
-  [ apply (carr1 s)
-  | constructor 1;
-    [ apply (eq_rel1 s);
-      apply (eq1 s)
-    | apply (refl1 s)
-    | apply (sym1 s)
-    | apply (trans1 s)]]
+ #s
+  @mk_setoid2
+  [ @(carr1 s)
+  | @mk_equivalence_relation2
+    [ @(eq_rel1 s)
+      @(eq1 s)
+    | @(refl1 s)
+    | @(sym1 s)
+    | @(trans1 s)]]
 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 *)
-
-record equivalence_relation3 (A:Type3) : Type4 ≝
- { eq_rel3:2> A → A → CProp3;
+*)
+record equivalence_relation3 (A:Type[3]) : Type[4] ≝
+ { eq_rel3:2> A → A → CProp[3];
    refl3: reflexive3 ? eq_rel3;
    sym3: symmetric3 ? eq_rel3;
    trans3: transitive3 ? eq_rel3
  }.
 
-record setoid3: Type4 ≝
- { carr3:> Type3;
+record setoid3: Type[4] ≝
+ { carr3:> Type[3];
    eq3: equivalence_relation3 carr3
  }.
 
@@ -129,42 +134,42 @@ interpretation "trans2" 'trans r = (trans2 ????? r).
 interpretation "trans1" 'trans r = (trans1 ????? r).
 interpretation "trans" 'trans r = (trans ????? r).
 
-record unary_morphism (A,B: setoid) : Type0 ≝
- { fun1:1> A → B;
+record unary_morphism (A,B: setoid) : Type[0] ≝
+ { fun1:(*1>*) A → B;
    prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
  }.
 
-record unary_morphism1 (A,B: setoid1) : Type1 ≝
+record unary_morphism1 (A,B: setoid1) : Type[1] ≝
  { fun11:1> A → B;
    prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
  }.
 
-record unary_morphism2 (A,B: setoid2) : Type2 ≝
+record unary_morphism2 (A,B: setoid2) : Type[2] ≝
  { fun12:1> A → B;
    prop12: ∀a,a'. eq2 ? a a' → eq2 ? (fun12 a) (fun12 a')
  }.
 
-record unary_morphism3 (A,B: setoid3) : Type3 ≝
+record unary_morphism3 (A,B: setoid3) : Type[3] ≝
  { fun13:1> A → B;
    prop13: ∀a,a'. eq3 ? a a' → eq3 ? (fun13 a) (fun13 a')
  }.
 
-record binary_morphism (A,B,C:setoid) : Type0 ≝
+record binary_morphism (A,B,C:setoid) : Type[0] ≝
  { fun2:2> A → B → C;
    prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
  }.
 
-record binary_morphism1 (A,B,C:setoid1) : Type1 ≝
+record binary_morphism1 (A,B,C:setoid1) : Type[1] ≝
  { fun21:2> A → B → C;
    prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b')
  }.
 
-record binary_morphism2 (A,B,C:setoid2) : Type2 ≝
+record binary_morphism2 (A,B,C:setoid2) : Type[2] ≝
  { fun22:2> A → B → C;
    prop22: ∀a,a',b,b'. eq2 ? a a' → eq2 ? b b' → eq2 ? (fun22 a b) (fun22 a' b')
  }.
 
-record binary_morphism3 (A,B,C:setoid3) : Type3 ≝
+record binary_morphism3 (A,B,C:setoid3) : Type[3] ≝
  { fun23:2> A → B → C;
    prop23: ∀a,a',b,b'. eq3 ? a a' → eq3 ? b b' → eq3 ? (fun23 a b) (fun23 a' b')
  }.
@@ -215,29 +220,29 @@ interpretation "'arrows1_SETlow" 'arrows1_SETlow A B = (unary_morphism1 A B).
 
 definition unary_morphism2_of_unary_morphism1: 
   ∀S,T:setoid1.unary_morphism1 S T → unary_morphism2 (setoid2_of_setoid1 S) T.
- intros;
- constructor 1;
-  [ apply (fun11 ?? u);
-  | apply (prop11 ?? u); ]
+ #S #T #u
+ @mk_unary_morphism2
+  [ @(fun11 ?? u)
+  | @(prop11 ?? u) ]
 qed.
 
 definition CPROP: setoid1.
- constructor 1;
-  [ apply CProp0
-  | constructor 1;
-     [ apply Iff
-     | intros 1; split; intro; assumption
-     | intros 3; cases i; split; assumption
-     | intros 5; cases i; cases i1; split; intro;
-        [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]]
+ @mk_setoid1
+  [ @CProp[0]
+  | @mk_equivalence_relation1
+     [ @Iff
+     | #H1 @mk_Iff #H3 #H5 assumption
+     | #H7 #H8 #i cases i #H14 #H15 @mk_Iff assumption
+     | #H17 #H18 #H19 #i1 #i cases i cases i1 #f #f1 #f2 #f3 @mk_Iff
+       [ #x1 @(f2 (f x1)) | #z1 @(f1 (f3 z1))]]]
 qed.
 
-definition CProp0_of_CPROP: carr1 CPROP → CProp0 ≝ λx.x.
+definition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
 coercion CProp0_of_CPROP.
 
 alias symbol "eq" = "setoid1 eq".
 definition fi': ∀A,B:CPROP. A = B → B → A.
- intros; apply (fi ?? e); assumption.
+ intros; @(fi ?? e); assumption.
 qed.
 
 notation ". r" with precedence 50 for @{'fi $r}.
@@ -245,39 +250,39 @@ interpretation "fi" 'fi r = (fi' ?? r).
 
 definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
  constructor 1;
-  [ apply And
+  [ @And
   | intros; split; intro; cases a1; split;
-     [ apply (if ?? e a2)
-     | apply (if ?? e1 b1)
-     | apply (fi ?? e a2)
-     | apply (fi ?? e1 b1)]]
+     [ @(if ?? e a2)
+     | @(if ?? e1 b1)
+     | @(fi ?? e a2)
+     | @(fi ?? e1 b1)]]
 qed.
 
 interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).
 
 definition or_morphism: binary_morphism1 CPROP CPROP CPROP.
  constructor 1;
-  [ apply Or
+  [ @Or
   | intros; split; intro; cases o; [1,3:left |2,4: right]
-     [ apply (if ?? e a1)
-     | apply (fi ?? e a1)
-     | apply (if ?? e1 b1)
-     | apply (fi ?? e1 b1)]]
+     [ @(if ?? e a1)
+     | @(fi ?? e a1)
+     | @(if ?? e1 b1)
+     | @(fi ?? e1 b1)]]
 qed.
 
 interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).
 
 definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
  constructor 1;
-  [ apply (λA,B. A → B)
+  [ @(λA,B. A → B)
   | intros; split; intros;
-     [ apply (if ?? e1); apply f; apply (fi ?? e); assumption
-     | apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
+     [ @(if ?? e1); @f; @(fi ?? e); assumption
+     | @(fi ?? e1); @f; @(if ?? e); assumption]]
 qed.
 
 notation > "hvbox(a break ∘ b)" left associative with precedence 55 for @{ comp ??? $a $b }.
-record category : Type1 ≝ { 
-   objs:> Type0;
+record category : Type[1] ≝ { 
+   objs:> Type[0];
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
    comp: ∀o1,o2,o3. (arrows o1 o2) × (arrows o2 o3) ⇒ (arrows o1 o3);
@@ -288,8 +293,8 @@ record category : Type1 ≝ {
 }.
 notation "hvbox(a break ∘ b)" left associative with precedence 55 for @{ 'compose $a $b }.
 
-record category1 : Type2 ≝
- { objs1:> Type1;
+record category1 : Type[2] ≝
+ { objs1:> Type[1];
    arrows1: objs1 → objs1 → setoid1;
    id1: ∀o:objs1. arrows1 o o;
    comp1: ∀o1,o2,o3. binary_morphism1 (arrows1 o1 o2) (arrows1 o2 o3) (arrows1 o1 o3);
@@ -299,8 +304,8 @@ record category1 : Type2 ≝
    id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) =_1 a
  }.
 
-record category2 : Type3 ≝
- { objs2:> Type2;
+record category2 : Type[3] ≝
+ { objs2:> Type[2];
    arrows2: objs2 → objs2 → setoid2;
    id2: ∀o:objs2. arrows2 o o;
    comp2: ∀o1,o2,o3. binary_morphism2 (arrows2 o1 o2) (arrows2 o2 o3) (arrows2 o1 o3);
@@ -310,8 +315,8 @@ record category2 : Type3 ≝
    id_neutral_left2: ∀o1,o2. ∀a: arrows2 o1 o2. comp2 ??? a (id2 o2) =_2 a
  }.
 
-record category3 : Type4 ≝
- { objs3:> Type3;
+record category3 : Type[4] ≝
+ { objs3:> Type[3];
    arrows3: objs3 → objs3 → setoid3;
    id3: ∀o:objs3. arrows3 o o;
    comp3: ∀o1,o2,o3. binary_morphism3 (arrows3 o1 o2) (arrows3 o2 o3) (arrows3 o1 o3);
@@ -333,21 +338,21 @@ interpretation "category assoc" 'assoc = (comp_assoc ????????).
 definition category2_of_category1: category1 → category2.
  intro;
  constructor 1;
-  [ apply (objs1 c);
-  | intros; apply (setoid2_of_setoid1 (arrows1 c o o1));
-  | apply (id1 c);
+  [ @(objs1 c);
+  | intros; @(setoid2_of_setoid1 (arrows1 c o o1));
+  | @(id1 c);
   | intros;
     constructor 1;
-     [ intros; apply (comp1 c o1 o2 o3 c1 c2);
+     [ intros; @(comp1 c o1 o2 o3 c1 c2);
      | intros; unfold setoid2_of_setoid1 in e e1 a a' b b'; simplify in e e1 a a' b b'; 
-       change with ((b∘a) =_1 (b'∘a')); apply (e‡e1); ]
-  | intros; simplify; whd in a12 a23 a34; whd; apply rule (ASSOC);
-  | intros; simplify; whd in a; whd; apply id_neutral_right1;
-  | intros; simplify; whd in a; whd; apply id_neutral_left1; ]
+       change with ((b∘a) =_1 (b'∘a')); @(e‡e1); ]
+  | intros; simplify; whd in a12 a23 a34; whd; @rule (ASSOC);
+  | intros; simplify; whd in a; whd; @id_neutral_right1;
+  | intros; simplify; whd in a; whd; @id_neutral_left1; ]
 qed.
 (*coercion category2_of_category1.*)
 
-record functor2 (C1: category2) (C2: category2) : Type3 ≝
+record functor2 (C1: category2) (C2: category2) : Type[3] ≝
  { map_objs2:1> C1 → C2;
    map_arrows2: ∀S,T. unary_morphism2 (arrows2 ? S T) (arrows2 ? (map_objs2 S) (map_objs2 T));
    respects_id2: ∀o:C1. map_arrows2 ?? (id2 ? o) = id2 ? (map_objs2 o);
@@ -362,14 +367,14 @@ interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??)
 definition functor2_setoid: category2 → category2 → setoid3.
  intros (C1 C2);
  constructor 1;
-  [ apply (functor2 C1 C2);
+  [ @(functor2 C1 C2);
   | constructor 1;
      [ intros (f g);
-       apply (∀c:C1. cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? (f c) (g c));
-     | simplify; intros; apply cic:/matita/logic/equality/eq.ind#xpointer(1/1/1);
-     | simplify; intros; apply cic:/matita/logic/equality/sym_eq.con; apply H;
-     | simplify; intros; apply cic:/matita/logic/equality/trans_eq.con;
-        [2: apply H; | skip | apply H1;]]]
+       @(∀c:C1. cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? (f c) (g c));
+     | simplify; intros; @cic:/matita/logic/equality/eq.ind#xpointer(1/1/1);
+     | simplify; intros; @cic:/matita/logic/equality/sym_eq.con; @H;
+     | simplify; intros; @cic:/matita/logic/equality/trans_eq.con;
+        [2: @H; | skip | @H1;]]]
 qed.
 
 definition functor2_of_functor2_setoid: ∀S,T. functor2_setoid S T → functor2 S T ≝ λS,T,x.x.
@@ -377,30 +382,30 @@ coercion functor2_of_functor2_setoid.
 
 definition CAT2: category3.
  constructor 1;
-  [ apply category2;
-  | apply functor2_setoid;
+  [ @category2;
+  | @functor2_setoid;
   | intros; constructor 1;
-     [ apply (λx.x);
+     [ @(λx.x);
      | intros; constructor 1;
-        [ apply (λx.x);
+        [ @(λx.x);
         | intros; assumption;]
-     | intros; apply rule #;
-     | intros; apply rule #; ]
+     | intros; @rule #;
+     | intros; @rule #; ]
   | intros; constructor 1;
      [ intros; constructor 1;
-        [ intros; apply (c1 (c o));
+        [ intros; @(c1 (c o));
         | intros; constructor 1;
-           [ intro; apply (map_arrows2 ?? c1 ?? (map_arrows2 ?? c ?? c2));
-           | intros; apply (††e); ]
+           [ intro; @(map_arrows2 ?? c1 ?? (map_arrows2 ?? c ?? c2));
+           | intros; @(††e); ]
         | intros; simplify;
-          apply (.= †(respects_id2 : ?));
-          apply (respects_id2 : ?);
+          @(.= †(respects_id2 : ?));
+          @(respects_id2 : ?);
         | intros; simplify;
-          apply (.= †(respects_comp2 : ?));
-          apply (respects_comp2 : ?); ]
+          @(.= †(respects_comp2 : ?));
+          @(respects_comp2 : ?); ]
         | intros; intro; simplify;
-          apply (cic:/matita/logic/equality/eq_ind.con ????? (e ?));
-          apply (cic:/matita/logic/equality/eq_ind.con ????? (e1 ?));
+          @(cic:/matita/logic/equality/eq_ind.con ????? (e ?));
+          @(cic:/matita/logic/equality/eq_ind.con ????? (e1 ?));
           constructor 1; ]
         | intros; intro; simplify; constructor 1;
         | intros; intro; simplify; constructor 1;
@@ -420,27 +425,27 @@ interpretation "'arrows3_CAT" 'arrows3_CAT A B = (arrows3 CAT2 A B).
 definition unary_morphism_setoid: setoid → setoid → setoid.
  intros;
  constructor 1;
-  [ apply (unary_morphism s s1);
+  [ @(unary_morphism s s1);
   | constructor 1;
-     [ intros (f g); apply (∀a:s. eq ? (f a) (g a));
-     | intros 1; simplify; intros; apply refl;
-     | simplify; intros; apply sym; apply f;
-     | simplify; intros; apply trans; [2: apply f; | skip | apply f1]]]
+     [ intros (f g); @(∀a:s. eq ? (f a) (g a));
+     | intros 1; simplify; intros; @refl;
+     | simplify; intros; @sym; @f;
+     | simplify; intros; @trans; [2: @f; | skip | @f1]]]
 qed.
 
 definition SET: category1.
  constructor 1;
-  [ apply setoid;
-  | apply rule (λS,T:setoid.setoid1_of_setoid (unary_morphism_setoid S T));
-  | intros; constructor 1; [ apply (λx:carr o.x); | intros; assumption ]
-  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
-     apply († (†e));]
+  [ @setoid;
+  | @rule (λS,T:setoid.setoid1_of_setoid (unary_morphism_setoid S T));
+  | intros; constructor 1; [ @(λx:carr o.x); | intros; assumption ]
+  | intros; constructor 1; [ intros; constructor 1; [ @(λx. c1 (c x)); | intros;
+     @(† (†e));]
   | intros; whd; intros; simplify; whd in H1; whd in H;
-    apply trans; [ apply (b (a' a1)); | lapply (prop1 ?? b (a a1) (a' a1));
-     [ apply Hletin | apply (e a1); ]  | apply e1; ]]
-  | intros; whd; intros; simplify; apply refl;
-  | intros; simplify; whd; intros; simplify; apply refl;
-  | intros; simplify; whd; intros; simplify; apply refl;
+    @trans; [ @(b (a' a1)); | l@(prop1 ?? b (a a1) (a' a1));
+     [ @Hletin | @(e a1); ]  | @e1; ]]
+  | intros; whd; intros; simplify; @refl;
+  | intros; simplify; whd; intros; simplify; @refl;
+  | intros; simplify; whd; intros; simplify; @refl;
   ]
 qed.
 
@@ -456,14 +461,14 @@ interpretation "'arrows1_SET" 'arrows1_SET A B = (arrows1 SET A B).
 definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
  intros;
  constructor 1;
-  [ apply (unary_morphism1 s s1);
+  [ @(unary_morphism1 s s1);
   | constructor 1;
      [ intros (f g);
        alias symbol "eq" = "setoid1 eq".
-       apply (∀a: carr1 s. f a = g a);
-     | intros 1; simplify; intros; apply refl1;
-     | simplify; intros; apply sym1; apply f;
-     | simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]]
+       @(∀a: carr1 s. f a = g a);
+     | intros 1; simplify; intros; @refl1;
+     | simplify; intros; @sym1; @f;
+     | simplify; intros; @trans1; [2: @f; | skip | @f1]]]
 qed.
 
 definition unary_morphism1_of_unary_morphism1_setoid1 : 
@@ -472,17 +477,17 @@ coercion unary_morphism1_of_unary_morphism1_setoid1.
 
 definition SET1: objs3 CAT2.
  constructor 1;
-  [ apply setoid1;
-  | apply rule (λS,T.setoid2_of_setoid1 (unary_morphism1_setoid1 S T));
-  | intros; constructor 1; [ apply (λx.x); | intros; assumption ]
-  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
-     apply († (†e));]
+  [ @setoid1;
+  | @rule (λS,T.setoid2_of_setoid1 (unary_morphism1_setoid1 S T));
+  | intros; constructor 1; [ @(λx.x); | intros; assumption ]
+  | intros; constructor 1; [ intros; constructor 1; [ @(λx. c1 (c x)); | intros;
+     @(† (†e));]
   | intros; whd; intros; simplify; whd in H1; whd in H;
-    apply trans1; [ apply (b (a' a1)); | lapply (prop11 ?? b (a a1) (a' a1));
-     [ apply Hletin | apply (e a1); ]  | apply e1; ]]
-  | intros; whd; intros; simplify; apply refl1;
-  | intros; simplify; whd; intros; simplify; apply refl1;
-  | intros; simplify; whd; intros; simplify; apply refl1;
+    @trans1; [ @(b (a' a1)); | l@(prop11 ?? b (a a1) (a' a1));
+     [ @Hletin | @(e a1); ]  | @e1; ]]
+  | intros; whd; intros; simplify; @refl1;
+  | intros; simplify; whd; intros; simplify; @refl1;
+  | intros; simplify; whd; intros; simplify; @refl1;
   ]
 qed.
 
@@ -501,7 +506,7 @@ coercion objs2_of_category1.
 prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
 prefer coercion Type_OF_objs1.
 
-alias symbol "exists" (instance 1) = "CProp2 exists".
+alias symbol "exists" (instance 1) = "CProp[2] exists".
 definition full2 ≝  
   λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
     ∀o1,o2:A.∀f.∃g:arrows2 A o1 o2.F⎽⇒ g =_2 f.
diff --git a/matita/matita/library/formal_topology/concrete_spaces.ma b/matita/matita/lib/formal_topology/concrete_spaces.ma
similarity index 98%
rename from matita/matita/library/formal_topology/concrete_spaces.ma
rename to matita/matita/lib/formal_topology/concrete_spaces.ma
index 69ff6f134..f9f715dc6 100644
--- a/matita/matita/library/formal_topology/concrete_spaces.ma
+++ b/matita/matita/lib/formal_topology/concrete_spaces.ma
@@ -16,13 +16,13 @@ include "formal_topology/basic_pairs.ma".
 
 (* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
    (confondendola con la coercion per gli oggetti di SET
-record concrete_space : Type1 ≝
+record concrete_space : Type[1] ≝
  { bp:> BP;
    converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
    all_covered: ∀x: carr1 (concr bp). x ⊩ form bp
  }.
 
-record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type[1] ≝
  { rp:> arrows1 ? CS1 CS2;
    respects_converges:
     ∀b,c.
diff --git a/matita/matita/library/formal_topology/concrete_spaces_to_o-concrete_spaces.ma b/matita/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma
similarity index 100%
rename from matita/matita/library/formal_topology/concrete_spaces_to_o-concrete_spaces.ma
rename to matita/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma
diff --git a/matita/matita/library/formal_topology/cprop_connectives.ma b/matita/matita/lib/formal_topology/cprop_connectives.ma
similarity index 55%
rename from matita/matita/library/formal_topology/cprop_connectives.ma
rename to matita/matita/lib/formal_topology/cprop_connectives.ma
index a1faba399..af183d0f6 100644
--- a/matita/matita/library/formal_topology/cprop_connectives.ma
+++ b/matita/matita/lib/formal_topology/cprop_connectives.ma
@@ -12,45 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
-
-definition Type4 : Type := Type.
-definition Type3 : Type4 := Type.
-definition Type2 : Type3 := Type.
-definition Type1 : Type2 := Type.
-definition Type0 : Type1 := Type.
-
-definition Type_of_Type0: Type0 → Type := λx.x.
-definition Type_of_Type1: Type1 → Type := λx.x.
-definition Type_of_Type2: Type2 → Type := λx.x.
-definition Type_of_Type3: Type3 → Type := λx.x.
-definition Type_of_Type4: Type4 → Type := λx.x.
-coercion Type_of_Type0.
-coercion Type_of_Type1.
-coercion Type_of_Type2.
-coercion Type_of_Type3.
-coercion Type_of_Type4.
-
-definition CProp0 : Type1 := Type0.
-definition CProp1 : Type2 := Type1.
-definition CProp2 : Type3 := Type2.
-definition CProp3 : Type4 := Type3.
-definition CProp_of_CProp0: CProp0 → CProp ≝ λx.x.
-definition CProp_of_CProp1: CProp1 → CProp ≝ λx.x.
-definition CProp_of_CProp2: CProp2 → CProp ≝ λx.x.
-definition CProp_of_CProp3: CProp3 → CProp ≝ λx.x.
-coercion CProp_of_CProp0.
-coercion CProp_of_CProp1.
-coercion CProp_of_CProp2.
-coercion CProp_of_CProp3.
-
-inductive Or (A,B:CProp0) : CProp0 ≝
+include "basics/pts.ma".
+
+inductive False: CProp[0] ≝.
+
+inductive Or (A,B:CProp[0]) : CProp[0] ≝
  | Left : A → Or A B
  | Right : B → Or A B.
 
 interpretation "constructive or" 'or x y = (Or x y).
 
-inductive Or3 (A,B,C:CProp0) : CProp0 ≝
+inductive Or3 (A,B,C:CProp[0]) : CProp[0] ≝
  | Left3 : A → Or3 A B C
  | Middle3 : B → Or3 A B C
  | Right3 : C → Or3 A B C.
@@ -59,7 +31,7 @@ interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z).
 
 notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}.
 
-inductive Or4 (A,B,C,D:CProp0) : CProp0 ≝
+inductive Or4 (A,B,C,D:CProp[0]) : CProp[0] ≝
  | Left3 : A → Or4 A B C D
  | Middle3 : B → Or4 A B C D
  | Right3 : C → Or4 A B C D
@@ -69,31 +41,31 @@ interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t).
 
 notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}.
 
-inductive And (A,B:CProp0) : CProp0 ≝
+inductive And (A,B:CProp[0]) : CProp[0] ≝
  | Conj : A → B → And A B.
  
 interpretation "constructive and" 'and x y = (And x y).
 
-inductive And3 (A,B,C:CProp0) : CProp0 ≝
+inductive And3 (A,B,C:CProp[0]) : CProp[0] ≝
  | Conj3 : A → B → C → And3 A B C.
 
 notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}.
  
 interpretation "constructive ternary and" 'and3 x y z = (And3 x y z).
 
-inductive And42 (A,B,C,D:CProp2) : CProp2 ≝
+inductive And42 (A,B,C,D:CProp[2]) : CProp[2] ≝
  | Conj42 : A → B → C → D → And42 A B C D.
 
 notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}.
  
 interpretation "constructive quaternary and2" 'and4 x y z t = (And42 x y z t).
 
-record Iff (A,B:CProp0) : CProp0 ≝
+record Iff (A,B:CProp[0]) : CProp[0] ≝
  { if: A → B;
    fi: B → A
  }.
  
-record Iff1 (A,B:CProp1) : CProp1 ≝
+record Iff1 (A,B:CProp[1]) : CProp[1] ≝
  { if1: A → B;
    fi1: B → A
  }.
@@ -102,11 +74,11 @@ notation "hvbox(a break ⇔ b)" right associative with precedence 25 for @{'iff1
 interpretation "logical iff" 'iff x y = (Iff x y).
 interpretation "logical iff type1" 'iff1 x y = (Iff1 x y).
 
-inductive exT22 (A:Type2) (P:A→CProp2) : CProp2 ≝
+inductive exT22 (A:Type[2]) (P:A→CProp[2]) : CProp[2] ≝
   ex_introT22: ∀w:A. P w → exT22 A P.
   
-interpretation "CProp2 exists" 'exists \eta.x = (exT22 ? x).
-
+interpretation "CProp[2] exists" 'exists \eta.x = (exT22 ? x).
+(*
 definition pi1exT22 ≝ λA,P.λx:exT22 A P.match x with [ex_introT22 x _ ⇒ x].
 definition pi2exT22 ≝ 
   λA,P.λx:exT22 A P.match x return λx.P (pi1exT22 ?? x) with [ex_introT22 _ p ⇒ p].
@@ -117,8 +89,8 @@ interpretation "exT22 \fst a" 'pi1a x = (pi1exT22 ? ? x).
 interpretation "exT22 \snd a" 'pi2a x = (pi2exT22 ? ? x).
 interpretation "exT22 \fst b" 'pi1b x y = (pi1exT22 ? ? x y).
 interpretation "exT22 \snd b" 'pi2b x y = (pi2exT22 ? ? x y).
-
-inductive exT (A:Type0) (P:A→CProp0) : CProp0 ≝
+*)
+inductive exT (A:Type[0]) (P:A→CProp[0]) : CProp[0] ≝
   ex_introT: ∀w:A. P w → exT A P.
 
 interpretation "CProp exists" 'exists \eta.x = (exT ? x).
@@ -128,7 +100,7 @@ with precedence 90 for @{'dependent_pair $a $b}.
 interpretation "dependent pair" 'dependent_pair a b = 
   (ex_introT ? ? a b).
 
-
+(*
 definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
 definition pi2exT ≝ 
   λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
@@ -139,10 +111,10 @@ interpretation "exT \fst b" 'pi1b x y = (pi1exT ? ? x y).
 interpretation "exT \snd" 'pi2 = (pi2exT ? ?).
 interpretation "exT \snd a" 'pi2a x = (pi2exT ? ? x).
 interpretation "exT \snd b" 'pi2b x y = (pi2exT ? ? x y).
-
-inductive exT23 (A:Type0) (P:A→CProp0) (Q:A→CProp0) (R:A→A→CProp0) : CProp0 ≝
+*)
+inductive exT23 (A:Type[0]) (P:A→CProp[0]) (Q:A→CProp[0]) (R:A→A→CProp[0]) : CProp[0] ≝
   ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
-
+(*
 definition pi1exT23 ≝
   λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
 definition pi2exT23 ≝
@@ -154,39 +126,39 @@ interpretation "exT2 \fst a" 'pi1a x = (pi1exT23 ? ? ? ? x).
 interpretation "exT2 \snd a" 'pi2a x = (pi2exT23 ? ? ? ? x).
 interpretation "exT2 \fst b" 'pi1b x y = (pi1exT23 ? ? ? ? x y).
 interpretation "exT2 \snd b" 'pi2b x y = (pi2exT23 ? ? ? ? x y).
-
-inductive exT2 (A:Type0) (P,Q:A→CProp0) : CProp0 ≝
+*)
+inductive exT2 (A:Type[0]) (P,Q:A→CProp[0]) : CProp[0] ≝
   ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
 
 
-definition Not : CProp0 → Prop ≝ λx:CProp.x → False.
+definition Not : CProp[0] → CProp[0] ≝ λx:CProp[0].x → False.
 
 interpretation "constructive not" 'not x = (Not x).
   
-definition cotransitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝
- λC:Type0.λlt:C→C→CProp0.∀x,y,z:C. lt x y → lt x z ∨ lt z y. 
+definition cotransitive: ∀C:Type[0]. ∀lt:C→C→CProp[0].CProp[0] ≝
+ λC:Type[0].λlt:C→C→CProp[0].∀x,y,z:C. lt x y → lt x z ∨ lt z y. 
 
-definition coreflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝
- λC:Type0.λlt:C→C→CProp0. ∀x:C. ¬ (lt x x).
+definition coreflexive: ∀C:Type[0]. ∀lt:C→C→CProp[0].CProp[0] ≝
+ λC:Type[0].λlt:C→C→CProp[0]. ∀x:C. ¬ (lt x x).
 
-definition symmetric: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝
- λC:Type0.λlt:C→C→CProp0. ∀x,y:C.lt x y → lt y x.
+definition symmetric: ∀C:Type[0]. ∀lt:C→C→CProp[0].CProp[0] ≝
+ λC:Type[0].λlt:C→C→CProp[0]. ∀x,y:C.lt x y → lt y x.
 
-definition antisymmetric: ∀A:Type0. ∀R:A→A→CProp0. ∀eq:A→A→Prop.CProp0 ≝
- λA:Type0.λR:A→A→CProp0.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
+definition antisymmetric: ∀A:Type[0]. ∀R:A→A→CProp[0]. ∀eq:A→A→Prop.CProp[0] ≝
+ λA:Type[0].λR:A→A→CProp[0].λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
 
-definition reflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x:A.R x x.
+definition reflexive: ∀C:Type[0]. ∀lt:C→C→CProp[0].CProp[0] ≝ λA:Type[0].λR:A→A→CProp[0].∀x:A.R x x.
 
-definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
+definition transitive: ∀C:Type[0]. ∀lt:C→C→CProp[0].CProp[0] ≝ λA:Type[0].λR:A→A→CProp[0].∀x,y,z:A.R x y → R y z → R x z.
 
-definition reflexive1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λA:Type1.λR:A→A→CProp1.∀x:A.R x x.
-definition symmetric1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λC:Type1.λlt:C→C→CProp1. ∀x,y:C.lt x y → lt y x.
-definition transitive1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λA:Type1.λR:A→A→CProp1.∀x,y,z:A.R x y → R y z → R x z.
+definition reflexive1: ∀A:Type[1].∀R:A→A→CProp[1].CProp[1] ≝ λA:Type[1].λR:A→A→CProp[1].∀x:A.R x x.
+definition symmetric1: ∀A:Type[1].∀R:A→A→CProp[1].CProp[1] ≝ λC:Type[1].λlt:C→C→CProp[1]. ∀x,y:C.lt x y → lt y x.
+definition transitive1: ∀A:Type[1].∀R:A→A→CProp[1].CProp[1] ≝ λA:Type[1].λR:A→A→CProp[1].∀x,y,z:A.R x y → R y z → R x z.
 
-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.
-definition transitive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x,y,z:A.R x y → R y z → R x z.
+definition reflexive2: ∀A:Type[2].∀R:A→A→CProp[2].CProp[2] ≝ λA:Type[2].λR:A→A→CProp[2].∀x:A.R x x.
+definition symmetric2: ∀A:Type[2].∀R:A→A→CProp[2].CProp[2] ≝ λC:Type[2].λlt:C→C→CProp[2]. ∀x,y:C.lt x y → lt y x.
+definition transitive2: ∀A:Type[2].∀R:A→A→CProp[2].CProp[2] ≝ λA:Type[2].λR:A→A→CProp[2].∀x,y,z:A.R x y → R y z → R x z.
 
-definition reflexive3: ∀A:Type3.∀R:A→A→CProp3.CProp3 ≝ λA:Type3.λR:A→A→CProp3.∀x:A.R x x.
-definition symmetric3: ∀A:Type3.∀R:A→A→CProp3.CProp3 ≝ λC:Type3.λlt:C→C→CProp3. ∀x,y:C.lt x y → lt y x.
-definition transitive3: ∀A:Type3.∀R:A→A→CProp3.CProp3 ≝ λA:Type3.λR:A→A→CProp3.∀x,y,z:A.R x y → R y z → R x z.
+definition reflexive3: ∀A:Type[3].∀R:A→A→CProp[3].CProp[3] ≝ λA:Type[3].λR:A→A→CProp[3].∀x:A.R x x.
+definition symmetric3: ∀A:Type[3].∀R:A→A→CProp[3].CProp[3] ≝ λC:Type[3].λlt:C→C→CProp[3]. ∀x,y:C.lt x y → lt y x.
+definition transitive3: ∀A:Type[3].∀R:A→A→CProp[3].CProp[3] ≝ λA:Type[3].λR:A→A→CProp[3].∀x,y,z:A.R x y → R y z → R x z.
diff --git a/matita/matita/library/formal_topology/formal_topologies.ma b/matita/matita/lib/formal_topology/formal_topologies.ma
similarity index 100%
rename from matita/matita/library/formal_topology/formal_topologies.ma
rename to matita/matita/lib/formal_topology/formal_topologies.ma
diff --git a/matita/matita/library/formal_topology/notation.ma b/matita/matita/lib/formal_topology/notation.ma
similarity index 100%
rename from matita/matita/library/formal_topology/notation.ma
rename to matita/matita/lib/formal_topology/notation.ma
diff --git a/matita/matita/library/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma
similarity index 99%
rename from matita/matita/library/formal_topology/o-algebra.ma
rename to matita/matita/lib/formal_topology/o-algebra.ma
index fb508aa92..f84249343 100644
--- a/matita/matita/library/formal_topology/o-algebra.ma
+++ b/matita/matita/lib/formal_topology/o-algebra.ma
@@ -14,7 +14,7 @@
 
 include "formal_topology/categories.ma".
 
-inductive bool : Type0 := true : bool | false : bool.
+inductive bool : Type[0] := true : bool | false : bool.
 
 lemma BOOL : objs1 SET.
 constructor 1; [apply bool] constructor 1;
@@ -63,7 +63,7 @@ notation > "⋁ p" non associative with precedence 45 for @{oa_join ? $p}.
 notation > "⋀ p" non associative with precedence 45 for @{oa_meet ? $p}.
 notation > "𝟙" non associative with precedence 90 for @{oa_one}. 
 notation > "𝟘" non associative with precedence 90 for @{oa_zero}. 
-record OAlgebra : Type2 := {
+record OAlgebra : Type[2] := {
   oa_P :> SET1;
   oa_leq : oa_P × oa_P ⇒_1 CPROP;
   oa_overlap: oa_P × oa_P ⇒_1 CPROP;
@@ -137,7 +137,7 @@ qed.
 interpretation "o-algebra binary meet" 'and a b = 
   (fun21 ??? (binary_meet ?) a b).
 
-prefer coercion Type1_OF_OAlgebra.
+prefer coercion Type[1]_OF_OAlgebra.
 
 definition binary_join : ∀O:OAlgebra. O × O ⇒_1 O.
 intros; split;
@@ -176,7 +176,7 @@ interpretation "o-algebra join" 'oa_join f =
 interpretation "o-algebra join with explicit function" 'oa_join_mk f = 
   (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
 
-record ORelation (P,Q : OAlgebra) : Type2 ≝ {
+record ORelation (P,Q : OAlgebra) : Type[2] ≝ {
   or_f_ : P ⇒_2 Q;
   or_f_minus_star_ : P ⇒_2 Q;
   or_f_star_ : Q ⇒_2 P;
diff --git a/matita/matita/library/formal_topology/o-basic_pairs.ma b/matita/matita/lib/formal_topology/o-basic_pairs.ma
similarity index 98%
rename from matita/matita/library/formal_topology/o-basic_pairs.ma
rename to matita/matita/lib/formal_topology/o-basic_pairs.ma
index e4bf8e5c7..02ef2143a 100644
--- a/matita/matita/library/formal_topology/o-basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/o-basic_pairs.ma
@@ -15,7 +15,7 @@
 include "formal_topology/o-algebra.ma".
 include "formal_topology/notation.ma".
 
-record Obasic_pair: Type2 ≝ { 
+record Obasic_pair: Type[2] ≝ { 
    Oconcr: OA; Oform: OA; Orel: arrows2 ? Oconcr Oform
 }.
 
@@ -23,7 +23,7 @@ record Obasic_pair: Type2 ≝ {
 interpretation "o-basic pair relation indexed" 'Vdash2 x y c = (Orel c x y).
 interpretation "o-basic pair relation (non applied)" 'Vdash c = (Orel c).
 
-record Orelation_pair (BP1,BP2: Obasic_pair): Type2 ≝ { 
+record Orelation_pair (BP1,BP2: Obasic_pair): Type[2] ≝ { 
    Oconcr_rel: (Oconcr BP1) ⇒_\o2 (Oconcr BP2); Oform_rel: (Oform BP1) ⇒_\o2 (Oform BP2);
    Ocommute: ⊩ ∘ Oconcr_rel =_2 Oform_rel ∘ ⊩
 }.
diff --git a/matita/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
similarity index 100%
rename from matita/matita/library/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
rename to matita/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma
diff --git a/matita/matita/library/formal_topology/o-basic_topologies.ma b/matita/matita/lib/formal_topology/o-basic_topologies.ma
similarity index 98%
rename from matita/matita/library/formal_topology/o-basic_topologies.ma
rename to matita/matita/lib/formal_topology/o-basic_topologies.ma
index 4228e6450..0e9d8604f 100644
--- a/matita/matita/library/formal_topology/o-basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/o-basic_topologies.ma
@@ -15,14 +15,14 @@
 include "formal_topology/o-algebra.ma".
 include "formal_topology/o-saturations.ma".
 
-record Obasic_topology: Type2 ≝ { 
+record Obasic_topology: Type[2] ≝ { 
    Ocarrbt:> OA;
    oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
    oA_is_saturation: is_o_saturation ? oA; oJ_is_reduction: is_o_reduction ? oJ;
    Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
  }.
 
-record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ { 
+record Ocontinuous_relation (S,T: Obasic_topology) : Type[2] ≝ { 
    Ocont_rel:> arrows2 OA S T;
    Oreduced: ∀U:S. U = oJ ? U → Ocont_rel U =_1 oJ ? (Ocont_rel U);
    Osaturated: ∀U:S. U = oA ? U → Ocont_rel⎻* U =_1 oA ? (Ocont_rel⎻* U)
diff --git a/matita/matita/library/formal_topology/o-concrete_spaces.ma b/matita/matita/lib/formal_topology/o-concrete_spaces.ma
similarity index 99%
rename from matita/matita/library/formal_topology/o-concrete_spaces.ma
rename to matita/matita/lib/formal_topology/o-concrete_spaces.ma
index 2ff03c8f7..d808b0085 100644
--- a/matita/matita/library/formal_topology/o-concrete_spaces.ma
+++ b/matita/matita/lib/formal_topology/o-concrete_spaces.ma
@@ -25,7 +25,7 @@ lemma down_p : ∀S:SET1.∀I:SET.∀u:S ⇒_1 S.∀c:arrows2 SET1 I S.∀a:I.
 intros; apply (†(†e));
 qed.
 
-record Oconcrete_space : Type2 ≝
+record Oconcrete_space : Type[2] ≝
  { Obp:> OBP;
    (*distr : is_distributive (form bp);*)
    Odownarrow: unary_morphism1 (Oform Obp) (Oform Obp);
@@ -54,7 +54,7 @@ qed.
 
 interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 ? ? ? (Obinary_downarrow ?) a b).
 
-record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type2 ≝
+record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type[2] ≝
  { Orp:> arrows2 ? CS1 CS2;
    Orespects_converges:
     ∀b,c. eq1 ? (Orp\sub\c⎻ (Ext⎽CS2 (b ↓ c))) (Ext⎽CS1 (Orp\sub\f⎻ b ↓ Orp\sub\f⎻ c));
diff --git a/matita/matita/library/formal_topology/o-formal_topologies.ma b/matita/matita/lib/formal_topology/o-formal_topologies.ma
similarity index 100%
rename from matita/matita/library/formal_topology/o-formal_topologies.ma
rename to matita/matita/lib/formal_topology/o-formal_topologies.ma
diff --git a/matita/matita/library/formal_topology/o-saturations.ma b/matita/matita/lib/formal_topology/o-saturations.ma
similarity index 93%
rename from matita/matita/library/formal_topology/o-saturations.ma
rename to matita/matita/lib/formal_topology/o-saturations.ma
index b8d5e9ca1..20db479a3 100644
--- a/matita/matita/library/formal_topology/o-saturations.ma
+++ b/matita/matita/lib/formal_topology/o-saturations.ma
@@ -14,10 +14,10 @@
 
 include "formal_topology/o-algebra.ma".
 
-definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp1 ≝
+definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp[1] ≝
  λC:OA.λA:C ⇒_1 C.∀U,V. (U ≤ A V) =_1 (A U ≤ A V).
 
-definition is_o_reduction: ∀C:OA. C ⇒_1 C → CProp1 ≝
+definition is_o_reduction: ∀C:OA. C ⇒_1 C → CProp[1] ≝
  λC:OA.λJ:C ⇒_1 C.∀U,V. (J U ≤ V) =_1 (J U ≤ J V).
 
 theorem o_saturation_expansive: ∀C,A. is_o_saturation C A → ∀U. U ≤ A U.
diff --git a/matita/matita/library/formal_topology/r-o-basic_pairs.ma b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma
similarity index 99%
rename from matita/matita/library/formal_topology/r-o-basic_pairs.ma
rename to matita/matita/lib/formal_topology/r-o-basic_pairs.ma
index 45593605e..76d077cfa 100644
--- a/matita/matita/library/formal_topology/r-o-basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma
@@ -96,7 +96,7 @@ qed.
 notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
 interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
 
-definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp1.
+definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp[1].
 intros (S T f); apply (∀X:Ω \sup S. (f X) =_1 ?);
 constructor 1; constructor 1;
 [ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
diff --git a/matita/matita/library/formal_topology/relations.ma b/matita/matita/lib/formal_topology/relations.ma
similarity index 99%
rename from matita/matita/library/formal_topology/relations.ma
rename to matita/matita/lib/formal_topology/relations.ma
index 789f312cf..2ad35655e 100644
--- a/matita/matita/library/formal_topology/relations.ma
+++ b/matita/matita/lib/formal_topology/relations.ma
@@ -14,7 +14,7 @@
 
 include "formal_topology/subsets.ma".
 
-record binary_relation (A,B: SET) : Type1 ≝
+record binary_relation (A,B: SET) : Type[1] ≝
  { satisfy:> binary_morphism1 A B CPROP }.
 
 notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)"  with precedence 45 for @{'satisfy $r $x $y}.
diff --git a/matita/matita/library/formal_topology/relations_to_o-algebra.ma b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma
similarity index 100%
rename from matita/matita/library/formal_topology/relations_to_o-algebra.ma
rename to matita/matita/lib/formal_topology/relations_to_o-algebra.ma
diff --git a/matita/matita/lib/formal_topology/replace.sh b/matita/matita/lib/formal_topology/replace.sh
new file mode 100644
index 000000000..5e281b251
--- /dev/null
+++ b/matita/matita/lib/formal_topology/replace.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+for MA in `find -name "*.ma"`; do
+   echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new
+   if diff ${MA} ${MA}.new > /dev/null; 
+      then rm -f ${MA}.new; 
+      else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA};
+   fi
+done
+
+unset MA
diff --git a/matita/matita/library/formal_topology/saturations.ma b/matita/matita/lib/formal_topology/saturations.ma
similarity index 92%
rename from matita/matita/library/formal_topology/saturations.ma
rename to matita/matita/lib/formal_topology/saturations.ma
index b02a9c053..02030e7cd 100644
--- a/matita/matita/library/formal_topology/saturations.ma
+++ b/matita/matita/lib/formal_topology/saturations.ma
@@ -14,10 +14,10 @@
 
 include "formal_topology/relations.ma".
 
-definition is_saturation: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝
+definition is_saturation: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp[1] ≝
  λC:REL.λA:Ω^C ⇒_1 Ω^C. ∀U,V. (U ⊆ A V) =_1 (A U ⊆ A V).
 
-definition is_reduction: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝
+definition is_reduction: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp[1] ≝
  λC:REL.λJ: Ω^C ⇒_1 Ω^C. ∀U,V. (J U ⊆ V) =_1 (J U ⊆ J V).
 
 theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U.
diff --git a/matita/matita/library/formal_topology/saturations_to_o-saturations.ma b/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma
similarity index 100%
rename from matita/matita/library/formal_topology/saturations_to_o-saturations.ma
rename to matita/matita/lib/formal_topology/saturations_to_o-saturations.ma
diff --git a/matita/matita/library/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma
similarity index 98%
rename from matita/matita/library/formal_topology/subsets.ma
rename to matita/matita/lib/formal_topology/subsets.ma
index 254f924dd..15bfb98d3 100644
--- a/matita/matita/library/formal_topology/subsets.ma
+++ b/matita/matita/lib/formal_topology/subsets.ma
@@ -14,12 +14,12 @@
 
 include "formal_topology/categories.ma".
 
-record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: A ⇒_1 CPROP }.
+record powerset_carrier (A: objs1 SET) : Type[1] ≝ { mem_operator: A ⇒_1 CPROP }.
 interpretation "powerset low" 'powerset A = (powerset_carrier A).
 notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
 interpretation "memlow" 'mem_low a S = (fun11 ?? (mem_operator ? S) a).
 
-definition subseteq_operator: ∀A: objs1 SET. Ω^A → Ω^A → CProp0 ≝
+definition subseteq_operator: ∀A: objs1 SET. Ω^A → Ω^A → CProp[0] ≝
  λA:objs1 SET.λU,V.∀a:A. a ∈. U → a ∈. V.
 
 theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
@@ -87,7 +87,7 @@ qed.
 definition overlaps: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
  intros;
  constructor 1;
-  [ apply (λA:objs1 SET.λU,V:Ω^A.(exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V) : CProp0))
+  [ apply (λA:objs1 SET.λU,V:Ω^A.(exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V) : CProp[0]))
   | intros;
     constructor 1; intro; cases e2; exists; [1,4: apply w]
      [ apply (. #‡e^-1); assumption
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index a94fbd552..98e9f1e61 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1509,7 +1509,7 @@ let predefined_classes = [
  ["⇒"; "➾"; "⇨"; "➡"; "⇉"; "⥤"; "⥰"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
  ["⇓"; "⇩"; "⬇"; ] ;
- ["⇔"; "⬄"; "⬌"; ] ; 
+ ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
  ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
-- 
2.39.2