- 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>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
<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
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
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
- 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.
functors, we also present algebraic versions of all the introduced
notions, as well as categorical embedding of the concrete categories in
functors, we also present algebraic versions of all the introduced
notions, as well as categorical embedding of the concrete categories in
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.
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.
existential and universal pre and post images of a relation.
</li>
<li>the large category of O-Basic Pairs, that algebraize Basic
existential and universal pre and post images of a relation.
</li>
<li>the large category of O-Basic Pairs, that algebraize Basic
<p>The formal system λδ is a typed λ-calculus that
pursues the unification of terms, types, environments and contexts
<p>The formal system λδ is a typed λ-calculus that
pursues the unification of terms, types, environments and contexts