-
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.