X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;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 @@
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.
- 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:The formal system λδ is a typed λ-calculus that pursues the unification of terms, types, environments and contexts @@ -165,7 +166,7 @@
- See the λδ home page + See the λδ home page for more information.