From 68bcb81d3d91255eacd5ae4c19c755d41e8440cf Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Oct 2009 09:30:11 +0000
Subject: [PATCH] fixed pictures

---
 .../matita/nlibrary/topology/cantor.ma        |   2 +
 .../nlibrary/topology/igft-CIC-universes.svg  | 157 +++----
 .../nlibrary/topology/igft-minimality-CIC.svg | 383 +++++++++++++-----
 .../software/matita/nlibrary/topology/igft.ma |  11 +-
 4 files changed, 371 insertions(+), 182 deletions(-)

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index b8f8a5543..6ae8d36ad 100644
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -28,6 +28,7 @@ interpretation "empty" 'empty = (emptyset ?).
 
 naxiom EM : ∀A:Ax.∀a:A.∀i_star.(a ∈ 𝐂 a i_star) ∨ ¬( a ∈ 𝐂 a i_star).
 
+alias symbol "covers" = "covers".
 ntheorem th2_3 :
   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
 #A; #a; #H; nelim H;
@@ -130,6 +131,7 @@ naxiom h : nat → nat.
 alias symbol "eq" = "leibnitz's equality".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "covers" = "covers".
+alias symbol "eq" = "leibnitz's equality".
 naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 
 nlemma replace_char:
diff --git a/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg b/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
index 49894fd46..524a15df8 100644
--- a/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
+++ b/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
@@ -49,9 +49,9 @@
      objecttolerance="10"
      inkscape:pageopacity="0.0"
      inkscape:pageshadow="2"
-     inkscape:zoom="0.96"
-     inkscape:cx="116.61148"
-     inkscape:cy="211.75616"
+     inkscape:zoom="1.26"
+     inkscape:cx="140.40282"
+     inkscape:cy="191.23857"
      inkscape:document-units="px"
      inkscape:current-layer="g3726"
      showgrid="false"
@@ -59,7 +59,9 @@
      inkscape:window-height="747"
      inkscape:window-x="0"
      inkscape:window-y="26"
-     units="cm" />
+     units="cm"
+     showguides="true"
+     inkscape:guide-bbox="true" />
   <metadata
      id="metadata5599">
     <rdf:RDF>
@@ -197,33 +199,33 @@
        id="path6753"
        sodipodi:nodetypes="cc" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1, 1;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2,2;stroke-dashoffset:0;stroke-opacity:1"
        d="M 531.54598,838.44703 L 531.54598,783.23841"
        id="path6755" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1, 1;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2,2;stroke-dashoffset:0;stroke-opacity:1"
        d="M 532.06404,748.82285 L 532.06404,693.61423"
        id="path6757" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1, 1;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2,2;stroke-dashoffset:0;stroke-opacity:1"
        d="M 276.66103,836.89285 L 276.66103,781.68423"
        id="path6759" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1.02127696, 1.02127696;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2.0425539,2.0425539;stroke-dashoffset:0;stroke-opacity:1"
        d="M 277.69711,747.25802 L 277.69711,689.51835"
        id="path6761" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1.02127696, 1.02127696;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2.0425539,2.0425539;stroke-dashoffset:0;stroke-opacity:1"
        d="M 319.87901,670.05275 L 469.31509,670.05275"
        id="path6765"
        sodipodi:nodetypes="cc" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1.02127696, 1.02127696;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2.0425539,2.0425539;stroke-dashoffset:0;stroke-opacity:1"
        d="M 320.13803,763.30334 L 469.57411,763.30334"
        id="path6767"
        sodipodi:nodetypes="cc" />
     <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1.02127696, 1.02127696;stroke-dashoffset:0;stroke-opacity:1"
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.02127695;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2.0425539,2.0425539;stroke-dashoffset:0;stroke-opacity:1"
        d="M 318.58386,856.03587 L 468.01994,856.03587"
        id="path6769"
        sodipodi:nodetypes="cc" />
@@ -247,76 +249,79 @@
     <g
        id="g3726"
        transform="translate(-196.38554,-21.460843)">
-      <path
-         id="path6777"
-         d="M 448.97379,1004.9376 L 504.18241,1004.9376"
-         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-opacity:1" />
-      <path
-         id="path6779"
-         d="M 448.9738,1026.178 L 504.18242,1026.178"
-         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:1, 1;stroke-dashoffset:0;stroke-opacity:1" />
-      <text
-         id="text6781"
-         y="1007.5103"
-         x="510.66592"
-         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-         xml:space="preserve"><tspan
+      <g
+         id="g3416">
+        <path
+           style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-opacity:1"
+           d="M 448.97379,1004.9376 L 504.18241,1004.9376"
+           id="path6777" />
+        <path
+           style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:2,2;stroke-dashoffset:0;stroke-opacity:1"
+           d="M 448.9738,1026.178 L 504.18242,1026.178"
+           id="path6779" />
+        <text
+           xml:space="preserve"
+           style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+           x="510.66592"
            y="1007.5103"
+           id="text6781"><tspan
+             sodipodi:role="line"
+             id="tspan6783"
+             x="510.66592"
+             y="1007.5103">Has type</tspan></text>
+        <text
+           xml:space="preserve"
+           style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
            x="510.66592"
-           id="tspan6783"
-           sodipodi:role="line">Has type</tspan></text>
-      <text
-         id="text6785"
-         y="1029.7869"
-         x="510.66592"
-         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-         xml:space="preserve"><tspan
-           id="tspan6789"
            y="1029.7869"
-           x="510.66592"
-           sodipodi:role="line">Is included</tspan></text>
-      <rect
-         y="1000.0105"
-         x="634.06982"
-         height="28.993309"
-         width="102.58569"
-         id="rect3712"
-         style="opacity:1;fill:none;fill-opacity:1;stroke:#828282;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:6, 6;stroke-dashoffset:0;stroke-opacity:1" />
-      <text
-         id="text3714"
-         y="1016.7295"
-         x="650.32379"
-         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-         xml:space="preserve"><tspan
-           y="1016.7295"
+           id="text6785"><tspan
+             sodipodi:role="line"
+             x="510.66592"
+             y="1029.7869"
+             id="tspan6789">Is included</tspan></text>
+        <rect
+           style="opacity:1;fill:none;fill-opacity:1;stroke:#828282;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:6, 6;stroke-dashoffset:0;stroke-opacity:1"
+           id="rect3712"
+           width="102.58569"
+           height="28.993309"
+           x="634.06982"
+           y="1000.0105" />
+        <text
+           xml:space="preserve"
+           style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
            x="650.32379"
-           id="tspan3716"
-           sodipodi:role="line">Mirror</tspan></text>
-      <rect
-         y="969.02521"
-         x="426.02521"
-         height="19.277109"
-         width="328.91565"
-         id="rect3718"
-         style="opacity:0.26612902;fill:#a1a1a1;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
-      <rect
-         transform="translate(188.07341,626.63597)"
-         y="339.97961"
-         x="236.14458"
-         height="71.084351"
-         width="333.73495"
-         id="rect3720"
-         style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
-      <text
-         id="text3722"
-         y="982.2782"
-         x="430.2421"
-         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-         xml:space="preserve"><tspan
-           y="982.2782"
+           y="1016.7295"
+           id="text3714"><tspan
+             sodipodi:role="line"
+             id="tspan3716"
+             x="650.32379"
+             y="1016.7295">Mirror</tspan></text>
+        <rect
+           style="opacity:0.26612902;fill:#a1a1a1;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+           id="rect3718"
+           width="328.91565"
+           height="19.277109"
+           x="426.02521"
+           y="969.02521" />
+        <rect
+           style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+           id="rect3720"
+           width="333.73495"
+           height="71.084351"
+           x="236.14458"
+           y="339.97961"
+           transform="translate(188.07341,626.63597)" />
+        <text
+           xml:space="preserve"
+           style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
            x="430.2421"
-           id="tspan3724"
-           sodipodi:role="line">Legenda</tspan></text>
+           y="982.2782"
+           id="text3722"><tspan
+             sodipodi:role="line"
+             id="tspan3724"
+             x="430.2421"
+             y="982.2782">Legenda</tspan></text>
+      </g>
     </g>
     <path
        style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-opacity:1"
diff --git a/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg b/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg
index d18237dd9..d70c35e03 100644
--- a/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg
+++ b/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg
@@ -8,8 +8,8 @@
    xmlns="http://www.w3.org/2000/svg"
    xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
    xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
-   width="496.06299"
-   height="318.89764"
+   width="600"
+   height="445"
    id="svg2"
    sodipodi:version="0.32"
    inkscape:version="0.46"
@@ -18,6 +18,19 @@
    version="1.0">
   <defs
      id="defs4">
+    <marker
+       inkscape:stockid="Arrow2Lstart"
+       orient="auto"
+       refY="0"
+       refX="0"
+       id="Arrow2Lstart"
+       style="overflow:visible">
+      <path
+         id="path3296"
+         style="font-size:12px;fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round"
+         d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.97309,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z"
+         transform="matrix(1.1,0,0,1.1,1.1,0)" />
+    </marker>
     <marker
        inkscape:stockid="StopL"
        orient="auto"
@@ -108,11 +121,11 @@
      objecttolerance="10"
      inkscape:pageopacity="0.0"
      inkscape:pageshadow="2"
-     inkscape:zoom="3.108143"
-     inkscape:cx="247.38483"
-     inkscape:cy="88.336977"
+     inkscape:zoom="0.9"
+     inkscape:cx="319.47326"
+     inkscape:cy="206.79135"
      inkscape:document-units="px"
-     inkscape:current-layer="g6154"
+     inkscape:current-layer="g4115"
      showgrid="false"
      inkscape:window-width="1280"
      inkscape:window-height="747"
@@ -135,7 +148,7 @@
      inkscape:label="Layer 1"
      inkscape:groupmode="layer"
      id="layer1"
-     transform="translate(-52.527322,-573.92589)">
+     transform="translate(-48.720708,-561.57164)">
     <text
        xml:space="preserve"
        style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
@@ -294,7 +307,7 @@
            x="489.87271"
            sodipodi:role="line">Coq's CIC <tspan
    style="font-size:10px"
-   id="tspan6150">(work in CProp)</tspan></tspan><tspan
+   id="tspan6150">(work in Type)</tspan></tspan><tspan
            id="tspan3212"
            style="font-size:12px"
            y="805.32825"
@@ -387,58 +400,6 @@
          x="440.85757"
          y="668.56934"
          id="tspan6207">Excluded Middle</tspan></text>
-    <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-start:none;marker-end:url(#Arrow2Lend);stroke-opacity:1"
-       d="M 362.82027,701.03266 C 362.82027,701.03266 294.27781,653.29395 204.66307,701.28945"
-       id="path6209"
-       sodipodi:nodetypes="cc" />
-    <path
-       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-start:none;marker-mid:none;marker-end:url(#Arrow2Lend);stroke-opacity:1"
-       d="M 203.66203,750.29609 L 361.81923,750.55288"
-       id="path6211"
-       sodipodi:nodetypes="cc" />
-    <g
-       id="g8379"
-       transform="translate(134.31734,94.095941)">
-      <path
-         transform="translate(51.420312,579.09195)"
-         id="path8375"
-         d="M 80.442804,87.328345 L 102.58303,67.033143"
-         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
-      <path
-         transform="translate(51.420312,579.09195)"
-         id="path8377"
-         d="M 80.073801,66.295135 L 103.32103,88.066353"
-         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
-    </g>
-    <g
-       id="g8383"
-       transform="translate(141.88192,23.200325)">
-      <path
-         transform="translate(51.420312,579.09195)"
-         id="path8385"
-         d="M 80.442804,87.328345 L 102.58303,67.033143"
-         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
-      <path
-         transform="translate(51.420312,579.09195)"
-         id="path8387"
-         d="M 80.073801,66.295135 L 103.32103,88.066353"
-         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
-    </g>
-    <text
-       xml:space="preserve"
-       style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-       x="236.74605"
-       y="698.91022"
-       id="text8389"><tspan
-         sodipodi:role="line"
-         x="236.74605"
-         y="698.91022"
-         id="tspan8391">Axiom of Choice</tspan><tspan
-         sodipodi:role="line"
-         x="236.74605"
-         y="713.91022"
-         id="tspan8393" /></text>
     <text
        xml:space="preserve"
        style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
@@ -453,34 +414,56 @@
          x="206.57732"
          y="618.78223"
          id="tspan8399" /></text>
-    <text
-       xml:space="preserve"
-       style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-       x="221.84404"
-       y="771.26294"
-       id="text8401"><tspan
-         sodipodi:role="line"
-         x="221.84404"
-         y="771.26294"
-         id="tspan8407">CProp Impredicative</tspan><tspan
-         sodipodi:role="line"
+    <g
+       id="g4089">
+      <path
+         sodipodi:nodetypes="cc"
+         id="path6211"
+         d="M 203.66203,726.64316 L 361.81923,726.89995"
+         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-start:url(#Arrow2Lstart);marker-mid:none;marker-end:url(#Arrow2Lend);stroke-opacity:1" />
+      <g
+         transform="translate(134.31734,70.443009)"
+         id="g8379">
+        <path
+           style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+           d="M 80.442804,87.328345 L 102.58303,67.033143"
+           id="path8375"
+           transform="translate(51.420312,579.09195)" />
+        <path
+           style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+           d="M 80.073801,66.295135 L 103.32103,88.066353"
+           id="path8377"
+           transform="translate(51.420312,579.09195)" />
+      </g>
+      <text
+         id="text8401"
+         y="747.60999"
          x="221.84404"
-         y="786.26294"
-         id="tspan8405" /></text>
-    <text
-       xml:space="preserve"
-       style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-       x="228.09178"
-       y="736.88953"
-       id="text8411"><tspan
-         sodipodi:role="line"
-         x="228.09178"
-         y="736.88953"
-         id="tspan8413">Girard's paradox</tspan><tspan
-         sodipodi:role="line"
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"><tspan
+           id="tspan8407"
+           y="747.60999"
+           x="221.84404"
+           sodipodi:role="line">CProp Impredicative</tspan><tspan
+           id="tspan8405"
+           y="762.60999"
+           x="221.84404"
+           sodipodi:role="line" /></text>
+      <text
+         id="text8411"
+         y="713.23657"
          x="228.09178"
-         y="751.88953"
-         id="tspan8415" /></text>
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"><tspan
+           id="tspan8413"
+           y="713.23657"
+           x="228.09178"
+           sodipodi:role="line">Girard's paradox</tspan><tspan
+           id="tspan8415"
+           y="728.23657"
+           x="228.09178"
+           sodipodi:role="line" /></text>
+    </g>
     <path
        style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-start:none;marker-end:url(#Arrow2Lend);stroke-opacity:1"
        d="M 359.90647,612.92159 C 359.90647,612.92159 212.45038,602.47727 189.20314,691.03816"
@@ -514,15 +497,223 @@
          x="240.21919"
          y="656.33929"
          id="tspan8439" /></text>
-    <text
-       xml:space="preserve"
-       style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
-       x="239.63129"
-       y="665.09381"
-       id="text8441"><tspan
-         sodipodi:role="line"
-         x="239.63129"
-         y="665.09381"
-         id="tspan8445">??????????????</tspan></text>
+    <g
+       id="g4109"
+       transform="translate(2.9566177,-24.392087)">
+      <text
+         id="text4101"
+         y="670.33813"
+         x="58.440556"
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"><tspan
+           y="670.33813"
+           x="58.440556"
+           id="tspan4103"
+           sodipodi:role="line">Bishop</tspan></text>
+      <rect
+         ry="10.717734"
+         transform="translate(52.527322,573.92589)"
+         y="81.629173"
+         x="2.2174623"
+         height="21.435469"
+         width="52.479942"
+         id="rect4105"
+         style="opacity:1;fill:none;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+      <rect
+         ry="10.717734"
+         y="652.59845"
+         x="46.61409"
+         height="26.609549"
+         width="66.523872"
+         id="rect4107"
+         style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+    </g>
+    <g
+       id="g4115"
+       transform="translate(25.870392,-51.74079)">
+      <g
+         id="g4125"
+         transform="translate(504.84226,78.35034)">
+        <text
+           xml:space="preserve"
+           style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+           x="62.136326"
+           y="670.33813"
+           id="text4117"><tspan
+             sodipodi:role="line"
+             id="tspan4119"
+             x="62.136326"
+             y="670.33813">Topos</tspan></text>
+        <rect
+           style="opacity:1;fill:none;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+           id="rect4121"
+           width="52.479942"
+           height="21.435469"
+           x="2.2174623"
+           y="81.629173"
+           transform="translate(52.527322,573.92589)"
+           ry="10.717734" />
+        <rect
+           style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+           id="rect4123"
+           width="66.523872"
+           height="26.609549"
+           x="46.61409"
+           y="652.59845"
+           ry="10.717734" />
+      </g>
+      <g
+         id="g4022"
+         transform="translate(-94.60221,-17.73018)">
+        <g
+           transform="translate(589.84498,-16.261391)"
+           id="g4131">
+          <text
+             id="text4133"
+             y="670.33813"
+             x="65.8321"
+             style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+             xml:space="preserve"><tspan
+               y="670.33813"
+               x="65.8321"
+               id="tspan4135"
+               sodipodi:role="line">ZFC</tspan></text>
+          <rect
+             ry="10.717734"
+             transform="translate(52.527322,573.92589)"
+             y="81.629173"
+             x="2.2174623"
+             height="21.435469"
+             width="52.479942"
+             id="rect4137"
+             style="opacity:1;fill:none;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+          <rect
+             ry="10.717734"
+             y="652.59845"
+             x="46.61409"
+             height="26.609549"
+             width="66.523872"
+             id="rect4139"
+             style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+        </g>
+      </g>
+    </g>
+    <g
+       transform="translate(-285.87827,-56.11513)"
+       id="g3416">
+      <path
+         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:3, 3;stroke-dashoffset:0;stroke-opacity:1"
+         d="M 381.23522,752.34128 L 372.13743,713.90527"
+         id="path4016"
+         sodipodi:nodetypes="cc" />
+      <path
+         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:3, 3;stroke-dashoffset:0;stroke-opacity:1"
+         d="M 801.07477,775.99422 L 862.93578,756.03706"
+         id="path4018"
+         sodipodi:nodetypes="cc" />
+      <path
+         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:3, 3;stroke-dashoffset:0;stroke-opacity:1"
+         d="M 798.11816,659.94701 L 852.58763,642.94646"
+         id="path4020"
+         sodipodi:nodetypes="cc" />
+    </g>
+    <g
+       id="g4046"
+       transform="translate(48.888889,-4.4444444)">
+      <path
+         id="path6777"
+         d="M 448.97379,1004.9376 L 504.18241,1004.9376"
+         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-opacity:1"
+         transform="translate(-285.87827,-56.11513)" />
+      <text
+         id="text6781"
+         y="1008.9886"
+         x="595.66864"
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"
+         transform="translate(-285.87827,-56.11513)"><tspan
+           y="1008.9886"
+           x="595.66864"
+           id="tspan6783"
+           sodipodi:role="line">becomes</tspan></text>
+      <rect
+         y="969.02521"
+         x="426.02521"
+         height="19.277109"
+         width="328.91565"
+         id="rect3718"
+         style="opacity:0.26612902;fill:#a1a1a1;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+         transform="translate(-285.87827,-56.11513)" />
+      <rect
+         transform="translate(-97.804862,570.52084)"
+         y="339.97961"
+         x="236.14458"
+         height="91.780663"
+         width="333.73492"
+         id="rect3720"
+         style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+      <text
+         id="text3722"
+         y="982.2782"
+         x="430.2421"
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"
+         transform="translate(-285.87827,-56.11513)"><tspan
+           y="982.2782"
+           x="430.2421"
+           id="tspan3724"
+           sodipodi:role="line">Legenda</tspan></text>
+      <path
+         id="path3455"
+         d="M 447.01995,1036.9156 L 502.22857,1036.9156"
+         style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-miterlimit:4;stroke-dasharray:3, 3;stroke-dashoffset:0;stroke-opacity:1"
+         transform="translate(-285.87827,-56.11513)" />
+      <text
+         id="text4008"
+         y="1039.1542"
+         x="594.7403"
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"
+         transform="translate(-285.87827,-56.11513)"><tspan
+           y="1039.1542"
+           x="594.7403"
+           id="tspan4010"
+           sodipodi:role="line">good to formalise X</tspan></text>
+      <text
+         id="text4012"
+         y="1039.8546"
+         x="531.95312"
+         style="font-size:12px;font-style:normal;font-weight:normal;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;font-family:Bitstream Vera Sans"
+         xml:space="preserve"
+         transform="translate(-285.87827,-56.11513)"><tspan
+           y="1039.8546"
+           x="531.95312"
+           id="tspan4014"
+           sodipodi:role="line">X</tspan></text>
+      <g
+         id="g4029">
+        <g
+           id="g3445"
+           transform="translate(171.37292,313.40134)">
+          <rect
+             ry="10.717734"
+             transform="translate(52.527322,573.92589)"
+             y="81.629173"
+             x="2.2174623"
+             height="21.435469"
+             width="52.479942"
+             id="rect3451"
+             style="opacity:1;fill:none;fill-opacity:1;stroke:none;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+          <rect
+             ry="10.717734"
+             y="652.59845"
+             x="46.61409"
+             height="26.609549"
+             width="66.523872"
+             id="rect3453"
+             style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.70000005;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+        </g>
+      </g>
+    </g>
   </g>
 </svg>
diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 3c0ba7090..e5859f03a 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -153,7 +153,7 @@ is a peculiarity of Matita (for example in CIC as implemented by Coq they are th
 same). The additional restriction of not allowing the elimination of a CProp
 toward a Type makes the theory of Matita minimal in the following sense: 
 
-<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="600px"/>
 
 Theorems proved in CIC as implemented in Matita can be reused in a classical 
 and impredicative framework (i.e. forcing Matita to collapse the hierarchy of 
@@ -1168,15 +1168,6 @@ We now proceed with the proof of the infinity rule.
 
 D*)
 
-
-alias symbol "exists" (instance 1) = "exists".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
 ntheorem new_coverage_infinity:
   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)  
-- 
2.39.2