From: Enrico Tassi Date: Wed, 21 Oct 2009 09:30:11 +0000 (+0000) Subject: fixed pictures X-Git-Tag: make_still_working~3271 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68bcb81d3d91255eacd5ae4c19c755d41e8440cf;p=helm.git fixed pictures --- 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" /> @@ -197,33 +199,33 @@ id="path6753" sodipodi:nodetypes="cc" /> @@ -247,76 +249,79 @@ - - - + + + Has type + Has type - Is included - - Is included + + Mirror - - - Mirror + + + Legenda + y="982.2782" + id="text3722">Legenda + + + + + transform="translate(-48.720708,-561.57164)"> Coq's CIC (work in CProp)(work in Type)Excluded Middle - - - - - - - - - - - Axiom of Choice - CProp Impredicative + + + + + + - Girard's paradoxCProp Impredicative + + 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">Girard's paradox + - ?????????????? + + Bishop + + + + + + Topos + + + + + + ZFC + + + + + + + + + + + + + becomes + + + Legenda + + good to formalise X + X + + + + + + + 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: - + 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". *)