Errata

In Samuele Maschio. Numerical existence property and categories with an internal copy.  Logica Universalis, 14(3), 383-394 (2020) 

-Section 7 p.390 : in the first line DC[T] is a cartesian first-order theory with equality. The same holds for the statement of Proposition 7.1

-In definition 4.3: the requirement "S is mono" is not necessary since it always holds for free. Indeed, S has always a left inverse.

-At page 389 there are some inconsistencies in the definition: 

    A) in clause 1. notoccur(\underline{y},x} should be erased

    B) in clause 4.  der(y, sub(z,\underline{y},\underline{x})) should be

           der(sub(y,\underline{z},\underline{y}), sub(z,\underline{z},\underline{x})) 

   C) in clause 9. y should be equal to a pair in which the first component is the one shown here, but the second is x.

  D) in clause 10. upper case Lambdas are typographical mistakes and should be conjunctions, while p_1(x) should be equal to the same term but with \underline{z} substituded with var(x), that is a term representing the xth variable of the system. This is to avoid occurrences of \underline{z} in p_1(y) and at the same time for guaranteeing the use of a fresh variable.

-In proof of Theorem 7.4, it is tacitely assumed that formulas in objects and arrows can be taken in such a way that the variable z does not occur in them.

In Hajime Ishihara, Maria Emilia Maietti, Samuele Maschio, Thomas Streicher. Consistency of the intensional level of the Minimalist Foundation with Church's Thesis and Axiom of Choice, Archive for Mathematical Logic, 57(7-8), 873-888 (2018).

item 18:  should be  x/ε π(a, b) if and only if Fam(b, a)∧∃y (y ε a∧(¬{x}(y) ↓ ∨{x}(y)/ε {b}(y)))

In Maschio, S., Sabelli, P. (2022). On the Compatibility Between the Minimalist Foundation and Constructive Set Theory.

pag. 176.  In the fifth rule two premisses are missing, namely: A col and B col

In Samuele Maschio. (2015) On the distinction between sets and classes: a categorical perspective.  

In the proof of Theorem 10.5.1 in the definition of functor P' on objects is ambiguous. However one can choose a representative of the class {z|varphi} using a minimum argument exploiting the fact that variables of the theory are presented with an enumeration and thus we have a goedelian encoding of formulas, in such a way that the first variable x_0 does not appear in it. 

Another way-out consists in defining the category of definable classes in such a way that {x|varphi} is identified with {x|psi} if varphi and psi are provably equivalent in the theory.

In Samuele Maschio, Davide Trotta (2024) On categorical structures arising from implicative algebras: from topology to assemblies

in Example 5.44 one should add the hypothesis of "locally connected topological space".