<h2>Scripts<a name="scripts"></a></h2>
<p>
- The <a href="library/">scripts</a> used to generate the knowledge base of
- Matita can be <a href="library/">browsed on line</a>.
+ The <a href="nlibrary/">scripts</a> used to generate the knowledge base of
+ Matita can be <a href="nlibrary/">browsed on line</a>.
</p>
<p>
- The experimental <a href="nlibrary/">scripts</a> for the next major version of Matita can also be <a href="nlibrary/">browsed on line</a>.
+ (Old <a href="library/">scripts</a> used in the previous releases of
+ Matita are <a href="library/">still available</a>.)
</p>
<br/>
<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
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
+ 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
here</a>.
</p>
- <h2>The Formal System λδ (lambda-delta)<a name="lambda-delta"></a></h2>
+ <h2>The Formal System λδ (lambda_delta)<a name="lambda_delta"></a></h2>
<p>The formal system λδ is a typed λ-calculus that
pursues the unification of terms, types, environments and contexts
</p>
<p>
- See the <a href="http://helm.cs.unibo.it/lambda-delta/">λδ home page</a>
+ See the <a href="http://lambda-delta.info/">λδ home page</a>
for more information.
</p>