...

diff --git a/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg b/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
new file mode 100644 (file)
index 0000000..0140c6b
--- /dev/null
+++ b/helm/software/matita/nlibrary/topology/igft-CIC-universes.svg
@@ -0,0 +1,265 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+   xmlns:dc="http://purl.org/dc/elements/1.1/"
+   xmlns:cc="http://creativecommons.org/ns#"
+   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+   xmlns:svg="http://www.w3.org/2000/svg"
+   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"
+   id="svg5594"
+   sodipodi:version="0.32"
+   inkscape:version="0.46"
+   sodipodi:docname="igft-CIC-universes.svg"
+   inkscape:output_extension="org.inkscape.output.svg.inkscape"
+   version="1.0">
+  <defs
+     id="defs5596">
+    <marker
+       inkscape:stockid="Arrow2Lend"
+       orient="auto"
+       refY="0"
+       refX="0"
+       id="Arrow2Lend"
+       style="overflow:visible">
+      <path
+         id="path3231"
+         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>
+    <inkscape:perspective
+       sodipodi:type="inkscape:persp3d"
+       inkscape:vp_x="0 : 526.18109 : 1"
+       inkscape:vp_y="0 : 1000 : 0"
+       inkscape:vp_z="744.09448 : 526.18109 : 1"
+       inkscape:persp3d-origin="372.04724 : 350.78739 : 1"
+       id="perspective5602" />
+  </defs>
+  <sodipodi:namedview
+     id="base"
+     pagecolor="#ffffff"
+     bordercolor="#666666"
+     borderopacity="1.0"
+     gridtolerance="10000"
+     guidetolerance="10"
+     objecttolerance="10"
+     inkscape:pageopacity="0.0"
+     inkscape:pageshadow="2"
+     inkscape:zoom="0.83572854"
+     inkscape:cx="484.72287"
+     inkscape:cy="293.62421"
+     inkscape:document-units="px"
+     inkscape:current-layer="layer1"
+     showgrid="false"
+     inkscape:window-width="1280"
+     inkscape:window-height="747"
+     inkscape:window-x="0"
+     inkscape:window-y="26" />
+  <metadata
+     id="metadata5599">
+    <rdf:RDF>
+      <cc:Work
+         rdf:about="">
+        <dc:format>image/svg+xml</dc:format>
+        <dc:type
+           rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+      </cc:Work>
+    </rdf:RDF>
+  </metadata>
+  <g
+     inkscape:label="Layer 1"
+     inkscape:groupmode="layer"
+     id="layer1"
+     transform="translate(-188.07341,-633.27063)">
+    <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="488.6709"
+       y="860.62408"
+       id="text5679"><tspan
+         sodipodi:role="line"
+         id="tspan5681"
+         x="488.6709"
+         y="860.62408">Type[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"
+       id="rect5683"
+       width="80.574745"
+       height="33.572811"
+       x="470.01935"
+       y="839.73438" />
+    <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="489.41693"
+       y="769.97754"
+       id="text5685"><tspan
+         sodipodi:role="line"
+         id="tspan5687"
+         x="489.41693"
+         y="769.97754">Type[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"
+       id="rect5689"
+       width="80.574745"
+       height="33.572811"
+       x="470.76538"
+       y="749.08783" />
+    <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="488.67093"
+       y="676.71973"
+       id="text5697"><tspan
+         sodipodi:role="line"
+         id="tspan5699"
+         x="488.67093"
+         y="676.71973">Type[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"
+       id="rect5701"
+       width="80.574745"
+       height="33.572811"
+       x="470.01938"
+       y="655.83002" />
+    <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"
+       y="858.94543"
+       id="text5703"><tspan
+         sodipodi:role="line"
+         id="tspan5705"
+         x="256.27246"
+         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"
+       id="rect5707"
+       width="80.574745"
+       height="33.572811"
+       x="237.6209"
+       y="838.05573" />
+    <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"
+       y="768.29889"
+       id="text5709"><tspan
+         sodipodi:role="line"
+         id="tspan5711"
+         x="257.01849"
+         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"
+       id="rect5713"
+       width="80.574745"
+       height="33.572811"
+       x="238.36693"
+       y="747.40918" />
+    <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"
+       y="675.04108"
+       id="text5715"><tspan
+         sodipodi:role="line"
+         id="tspan5717"
+         x="256.27252"
+         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"
+       id="rect5719"
+       width="80.574745"
+       height="33.572811"
+       x="237.62096"
+       y="654.15137" />
+    <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 508.81459,838.98832 L 508.81459,783.7797"
+       id="path5721" />
+    <path
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.01706386px;stroke-linecap:butt;stroke-linejoin:miter;marker-end:url(#Arrow2Lend);stroke-opacity:1"
+       d="M 508.93607,748.8504 L 508.93607,691.61697"
+       id="path6749" />
+    <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 318.64978,855.99465 L 469.92296,768.14832"
+       id="path6751"
+       sodipodi:nodetypes="cc" />
+    <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 318.80446,763.26458 L 470.07764,675.41825"
+       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"
+       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"
+       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"
+       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"
+       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"
+       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"
+       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"
+       d="M 318.58386,856.03587 L 468.01994,856.03587"
+       id="path6769"
+       sodipodi:nodetypes="cc" />
+    <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="rect6771"
+       width="183.91089"
+       height="258.51135"
+       x="188.57341"
+       y="633.77063" />
+    <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" />
+    <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" />
+    <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
+         sodipodi:role="line"
+         id="tspan6783"
+         x="337.77435"
+         y="917.1488">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="337.77435"
+       y="939.42535"
+       id="text6785"><tspan
+         sodipodi:role="line"
+         x="337.77435"
+         y="939.42535"
+         id="tspan6789">Is included</tspan></text>
+  </g>
+</svg>

diff --git a/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg b/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg
new file mode 100644 (file)
index 0000000..3cf9b46
--- /dev/null
+++ b/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg
@@ -0,0 +1,207 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+   xmlns:dc="http://purl.org/dc/elements/1.1/"
+   xmlns:cc="http://creativecommons.org/ns#"
+   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+   xmlns:svg="http://www.w3.org/2000/svg"
+   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="371.16943"
+   height="210.00404"
+   id="svg2"
+   sodipodi:version="0.32"
+   inkscape:version="0.46"
+   sodipodi:docname="igft-minimality-CIC.svg"
+   inkscape:output_extension="org.inkscape.output.svg.inkscape"
+   version="1.0">
+  <defs
+     id="defs4">
+    <marker
+       inkscape:stockid="Arrow2Lend"
+       orient="auto"
+       refY="0"
+       refX="0"
+       id="Arrow2Lend"
+       style="overflow:visible">
+      <path
+         id="path3231"
+         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="Arrow1Mend"
+       orient="auto"
+       refY="0"
+       refX="0"
+       id="Arrow1Mend"
+       style="overflow:visible">
+      <path
+         id="path3219"
+         d="M 0,0 L 5,-5 L -12.5,0 L 5,5 L 0,0 z"
+         style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;marker-start:none"
+         transform="matrix(-0.4,0,0,-0.4,-4,0)" />
+    </marker>
+    <inkscape:perspective
+       sodipodi:type="inkscape:persp3d"
+       inkscape:vp_x="0 : 526.18109 : 1"
+       inkscape:vp_y="0 : 1000 : 0"
+       inkscape:vp_z="744.09448 : 526.18109 : 1"
+       inkscape:persp3d-origin="372.04724 : 350.78739 : 1"
+       id="perspective10" />
+  </defs>
+  <sodipodi:namedview
+     id="base"
+     pagecolor="#ffffff"
+     bordercolor="#666666"
+     borderopacity="1.0"
+     gridtolerance="10000"
+     guidetolerance="10"
+     objecttolerance="10"
+     inkscape:pageopacity="0.0"
+     inkscape:pageshadow="2"
+     inkscape:zoom="1.9884615"
+     inkscape:cx="297.14286"
+     inkscape:cy="89.723635"
+     inkscape:document-units="px"
+     inkscape:current-layer="layer1"
+     showgrid="false"
+     inkscape:window-width="1280"
+     inkscape:window-height="747"
+     inkscape:window-x="0"
+     inkscape:window-y="26" />
+  <metadata
+     id="metadata7">
+    <rdf:RDF>
+      <cc:Work
+         rdf:about="">
+        <dc:format>image/svg+xml</dc:format>
+        <dc:type
+           rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+      </cc:Work>
+    </rdf:RDF>
+  </metadata>
+  <g
+     inkscape:label="Layer 1"
+     inkscape:groupmode="layer"
+     id="layer1"
+     transform="translate(-100.2483,-683.58839)">
+    <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="215.35783"
+       y="839.26465"
+       id="text2383"><tspan
+         sodipodi:role="line"
+         x="215.35783"
+         y="839.26465"
+         id="tspan5562"
+         style="font-size:12px">     Matita's CIC</tspan><tspan
+         sodipodi:role="line"
+         x="215.35783"
+         y="854.26465"
+         style="font-size:12px"
+         id="tspan2408" /><tspan
+         sodipodi:role="line"
+         x="215.35783"
+         y="867.27118"
+         id="tspan5564"
+         style="font-size:10px">CProp,Type predicative</tspan><tspan
+         sodipodi:role="line"
+         x="215.35783"
+         y="879.77118"
+         style="font-size:10px"
+         id="tspan5572">No elim CProp toward Type</tspan><tspan
+         sodipodi:role="line"
+         x="215.35783"
+         y="892.27118"
+         id="tspan5566" /></text>
+    <rect
+       style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:2.03334594;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
+       id="rect2399"
+       width="145.10805"
+       height="70.175743"
+       x="206.55623"
+       y="822.40002" />
+    <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="351.02515"
+       y="779.28674"
+       id="text3171"><tspan
+         sodipodi:role="line"
+         id="tspan3173"
+         x="351.02515"
+         y="779.28674">EM for CProp</tspan><tspan
+         sodipodi:role="line"
+         x="351.02515"
+         y="794.28674"
+         id="tspan3179">CProp impredicative</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="99.574471"
+       y="778.28094"
+       id="text3181"><tspan
+         sodipodi:role="line"
+         id="tspan3183"
+         x="99.574471"
+         y="778.28094">CProp[i] = Type[i]</tspan><tspan
+         sodipodi:role="line"
+         x="99.574471"
+         y="793.28094"
+         id="tspan3185">Exists = Sigma</tspan></text>
+    <rect
+       style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.3872999;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
+       id="rect3187"
+       width="121.11192"
+       height="39.139008"
+       x="312.59683"
+       y="684.78491" />
+    <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="318.33655"
+       y="699.32544"
+       id="text3189"><tspan
+         sodipodi:role="line"
+         id="tspan3191"
+         x="318.33655"
+         y="699.32544">Reuse theorems in</tspan><tspan
+         sodipodi:role="line"
+         x="318.33655"
+         y="714.32544"
+         id="tspan3193">a classical setting</tspan></text>
+    <rect
+       style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:1.3872999;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
+       id="rect3195"
+       width="121.11192"
+       height="39.139008"
+       x="128.03204"
+       y="684.28204" />
+    <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="139.30368"
+       y="700.83417"
+       id="text3197"><tspan
+         sodipodi:role="line"
+         x="139.30368"
+         y="700.83417"
+         id="tspan3201">Martin Löf</tspan><tspan
+         sodipodi:role="line"
+         x="139.30368"
+         y="715.83417"
+         id="tspan3205">Axiom of Choice</tspan></text>
+    <path
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="M 257.48549,821.53046 L 194.62282,722.9618"
+       id="path5558" />
+    <path
+       style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="M 305.51258,822.03336 L 368.37525,723.4647"
+       id="path5560" />
+  </g>
+</svg>

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 39497ac7be003b12f12e36925b323a986e0b0a77..075828b60e477b367d5757558d57b0088daacb0e 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -125,11 +125,7 @@ computation).
 Since we are going to formalize constructive and predicative mathematics
 in an intensional type theory like CIC, we try to establish some terminology. 
 Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
-not quotiented set). We will avoid using `Id` (Leibniz equality), 
-thus we will explicitly equip a set with an equivalence relation when needed.
-We will call this structure a _setoid_. Note that we will
-attach the infix `=` symbol only to the equality of a setoid,
-not to Id.
+not quotiented set). 
 
 We write `Type[i]` to mention a Type in the predicative hierarchy 
 of types. To ease the comprehension we will use `Type[0]` for sets, 
@@ -138,12 +134,39 @@ universes are declared by the user. The standard library defines
 
 > Type[0] < Type[1] < Type[2]
 
+<object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
+
 For every `Type[i]` there is a corresponding level of predicative
-propositions `CProp[i]`. A predicative proposition cannot be eliminated toward
-`Type[j]` unless it holds no computational content (i.e. it is an inductive type
+propositions `CProp[i]` (the C initial is due to historical reasons, and
+stands for constructive, `PProp` would be more appropriate). 
+A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
 with 0 or 1 constructors with propositional arguments, like `Id` and `And` 
 but not like `Or`). 
 
+The distintion between predicative propositions and predicative data types
+is a peculirity of Matita (for example in CIC as implemented by Coq they are the
+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"/>
+
+Theorems proved in this setting can be reused in a classical framwork (forcing
+Matita to collapse the hierarchy of constructive propositions). Alternatively,
+one can decide to collapse predicative propositions and datatypes recovering the
+Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to
+provide a witness for a Σ).
+
+Formalization choices
+---------------------
+
+We will avoid using `Id` (Leibniz equality), 
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,
+not to Id.
+
+
 
 The standard library and the `include` command
 ----------------------------------------------

diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml
index 3e76da66b33c4c803ee137f5590bd9e4040fc69c..45bc7da389eb00090da980f65ed938068504eb58 100644 (file)
--- a/helm/software/matita/nlibrary/topology/preamble.xml
+++ b/helm/software/matita/nlibrary/topology/preamble.xml
@@ -25,7 +25,7 @@ pre {
        margin-left: 2em; 
 }
 
-img { 
+img, .img { 
        margin-left: auto; 
        margin-right: auto; 
        display: block;