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"
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"
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"
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"
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"
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"
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"
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>
projects / helm.git / blobdiff
