X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=c42fa673bd0fd87dcab5afe1841e23771fdbab47;hb=0c8cad22457218f78c30de239e49187968251613;hp=626cdaba1858e559c5657deb5aacc8a0e4d0e1d7;hpb=337862338098a2e01a8d59dab6e36663d9679067;p=helm.git

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 626cdaba1..c42fa673b 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -52,7 +52,7 @@
       <p>The formalization has been the result of a three years long
        collaboration between mathematicians from the University of Padova
        and computer scientists from the University of
-       Bologna, sponsored by the University of Padova. In particular,
+       Bologna, funded by the University of Padova. In particular,
        the groups that collaborated are headed respectively by Prof. Sambin
        in Padua (formal topology and constructive type theory)
        and by Prof. Asperti in Bologna (constructive type theory and interactive
@@ -75,18 +75,19 @@
       fragment of Matita based on the minimalist type theory
       by Maietti and Sambin, where choice axioms are not valid.
       </p>
-      In order to reason conformtably on the previous concrete categories and
+      In order to reason comfortably on the previous concrete categories and
       functors, we also present algebraic versions of all the introduced
       notions, as well as categorical embedding of the concrete categories in
-      the algebraized ones. In particular we formalized:
+      the algebrized ones. In particular we formalized:
       </p>
       <ul>
-       <li>the large category of Overlap Algebras, that extend locales with an
+       <li>the large category of Overlap Algebras, that extends locales with an
            axiomatized (= algebraized) overlap binary predicate. The
            concrete overlap predicate states positively 
            (i.e. without using negation) the existence (in the intuitionistic
            sense) of a point in the intersection of two sets.
-           The natural morphism over Overlap Algebras are functions for the
+           Morphisms of Overlap Algebras algebrize concrete relations between
+           sets by means of four functions that capture the
            existential and universal pre and post images of a relation.
            </li>
        <li>the large category of O-Basic Pairs, that algebraize Basic
@@ -142,7 +143,7 @@
          here</a>.
       </p>
 
-      <h2>The Formal System &lambda;&delta; (lambda-delta)<a name="lambda-delta"></a></h2>
+      <h2>The Formal System &lambda;&delta; (lambda_delta)<a name="lambda_delta"></a></h2>
       
       <p>The formal system &lambda;&delta; is a typed &lambda;-calculus that
          pursues the unification of terms, types, environments and contexts
@@ -165,7 +166,7 @@
       </p>
       
       <p>
-       See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>
+       See the <a href="http://lambda-delta.info/">&lambda;&delta; home page</a>
        for more information.
       </p>