198 citations · 457 across the 25 of their papers we have counts for
27 papers
C-systems defined by universe categories: presheaves
Vladimir Voevodsky
The main result of this paper may be stated as a construction of "almost representations" for the canonical presheaves of object extensions of length n on the C-systems defined by…
The (Pi,lambda)-structures on the C-systems defined by universe categories
Vladimir Voevodsky
We define the notion of a (P,P-tilde)-structure on a universe p in a locally cartesian closed category category C with a binary product structure and construct a (Pi,lambda)-struct…
Products of families of types and (Pi,lambda)-structures on C-systems
Vladimir Voevodsky
In this paper we continue the study of the most important structures on C-systems, the structures that correspond, in the case of the syntactic C-systems, to the $(Pi,lambda,app,be…
Categorical structures for type theory in univalent foundations
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categori…
C-system of a module over a -relative monad
Vladimir Voevodsky
Let be the category with the set of objects and morphisms being the functions between the standard finite sets of the corresponding cardinalities. Let $Jf:F\rightarrow…
Lawvere theories and Jf-relative monads
Vladimir Voevodsky
In this paper we provide a detailed construction of an equivalence between the category of Lawvere theories and the category of relative monads on the obvious functor $Jf:F\rightar…