-
11B-Systems and C-Systems Are EquivalentJournal of Symbolic Logic 1-9. forthcoming.C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.
-
8A characterisation of elementary fibrationsAnnals of Pure and Applied Logic 173 (6): 103103. 2022.
-
33Exact completion and constructive theories of setsJournal of Symbolic Logic 85 (2): 563-584. 2020.In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects. Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study t…Read more
Genoa, Italy