X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft-CIC-universes.svg;h=524a15df8ad608ce9272ffd70917464bfa77e3c4;hb=e7264f953fcf2cd2bef9057d83add08996d2ce75;hp=0140c6bd48227bbffc35358c21957bfcce06e5b0;hpb=8de75e1a28002270f98c13eb0933f1780c181eb5;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg b/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
index 0140c6bd4..524a15df8 100644
--- a/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
+++ b/helm/software/matita/nlibrary/topology/igft-CIC-universes.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="363.91672"
-   height="306.94781"
+   width="389.76376"
+   height="407.48032"
    id="svg5594"
    sodipodi:version="0.32"
    inkscape:version="0.46"
@@ -49,16 +49,19 @@
      objecttolerance="10"
      inkscape:pageopacity="0.0"
      inkscape:pageshadow="2"
-     inkscape:zoom="0.83572854"
-     inkscape:cx="484.72287"
-     inkscape:cy="293.62421"
+     inkscape:zoom="1.26"
+     inkscape:cx="140.40282"
+     inkscape:cy="191.23857"
      inkscape:document-units="px"
-     inkscape:current-layer="layer1"
+     inkscape:current-layer="g3726"
      showgrid="false"
      inkscape:window-width="1280"
      inkscape:window-height="747"
      inkscape:window-x="0"
-     inkscape:window-y="26" />
+     inkscape:window-y="26"
+     units="cm"
+     showguides="true"
+     inkscape:guide-bbox="true" />
   <metadata
      id="metadata5599">
     <rdf:RDF>
@@ -74,7 +77,7 @@
      inkscape:label="Layer 1"
      inkscape:groupmode="layer"
      id="layer1"
-     transform="translate(-188.07341,-633.27063)">
+     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"
@@ -129,12 +132,12 @@
     <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="256.27246"
+       x="252.05559"
        y="858.94543"
        id="text5703"><tspan
          sodipodi:role="line"
          id="tspan5705"
-         x="256.27246"
+         x="252.05559"
          y="858.94543">CProp[0]</tspan></text>
     <rect
        style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.29999995;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
@@ -146,12 +149,12 @@
     <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="257.01849"
+       x="251.5968"
        y="768.29889"
        id="text5709"><tspan
          sodipodi:role="line"
          id="tspan5711"
-         x="257.01849"
+         x="251.5968"
          y="768.29889">CProp[1]</tspan></text>
     <rect
        style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.29999995;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
@@ -163,12 +166,12 @@
     <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="256.27252"
+       x="250.85083"
        y="675.04108"
        id="text5715"><tspan
          sodipodi:role="line"
          id="tspan5717"
-         x="256.27252"
+         x="250.85083"
          y="675.04108">CProp[2]</tspan></text>
     <rect
        style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.29999995;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
@@ -196,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" />
@@ -233,33 +236,124 @@
        height="258.51135"
        x="188.57341"
        y="633.77063" />
+    <path
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.70000005;stroke-linecap:butt;stroke-linejoin:miter;marker-end:none;stroke-miterlimit:4;stroke-dasharray:1.7, 5.1;stroke-dashoffset:0;stroke-opacity:1"
+       d="M 277.24765,650.76688 L 277.24765,627.48597"
+       id="path2417"
+       sodipodi:nodetypes="cc" />
+    <path
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.70000005;stroke-linecap:butt;stroke-linejoin:miter;marker-end:none;stroke-miterlimit:4;stroke-dasharray:1.7, 5.1;stroke-dashoffset:0;stroke-opacity:1"
+       d="M 511.56739,651.25649 L 511.56739,627.97558"
+       id="path3710"
+       sodipodi:nodetypes="cc" />
+    <g
+       id="g3726"
+       transform="translate(-196.38554,-21.460843)">
+      <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"
+           y="1029.7869"
+           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"
+           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"
+           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"
-       d="M 276.08222,914.57615 L 331.29084,914.57615"
-       id="path6777" />
+       d="M 42.344378,282.75069 L 380.72289,281.54587"
+       id="path3741"
+       transform="translate(188.07341,626.63597)"
+       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"
-       d="M 276.08223,935.81657 L 331.29085,935.81657"
-       id="path6779" />
+       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 219.98181,645.12981 L 218.77699,891.84167"
+       id="path5034"
+       sodipodi:nodetypes="cc" />
     <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="337.77435"
-       y="917.1488"
-       id="text6781"><tspan
+       x="719.58075"
+       y="-205.23161"
+       id="text5036"
+       transform="matrix(0,1,-1,0,0,0)"><tspan
          sodipodi:role="line"
-         id="tspan6783"
-         x="337.77435"
-         y="917.1488">Has type</tspan></text>
+         id="tspan5038"
+         x="719.58075"
+         y="-205.23161">Impredicativity</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="337.77435"
-       y="939.42535"
-       id="text6785"><tspan
+       x="343.28174"
+       y="920.44342"
+       id="text5040"><tspan
          sodipodi:role="line"
-         x="337.77435"
-         y="939.42535"
-         id="tspan6789">Is included</tspan></text>
+         id="tspan5042"
+         x="343.28174"
+         y="920.44342">Axiom of Choice</tspan></text>
   </g>
 </svg>