Maietti suggested to replace a paragraph about the development on the

Basic Picture

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 9874142c96d59067111f30163cc1e4ca4dfddfb8..626cdaba1858e559c5657deb5aacc8a0e4d0e1d7 100644 (file)
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -71,8 +71,9 @@
            adjunction between topological spaces and locales</li>
       </ul>
       <p>
-      All the results are presented constructively and in the predicative
-      fragment of Matita, without any reference to choice axioms.
+      All the results are presented constructively and in the predicative 
+      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
       functors, we also present algebraic versions of all the introduced