<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
fragment of Matita based on the minimalist type theory
by Maietti and Sambin, where choice axioms are not valid.
</p>
fragment of Matita based on the minimalist type theory
by Maietti and Sambin, where choice axioms are not valid.
</p>
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