2014/10/20 by Voevodsky, Vladimir · 1 citation
#03B15 #03B22 #03F50 #03G25 #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.1410.5389
B-systems are algebras (models) of an essentially algebraic theory that is expected to be constructively equivalent to the essentially algebraic theory of C-systems which is, in turn, constructively equivalent to the theory of contextual categories. The theory of B-systems is closer in its form to the structures directly modeled by contexts and typing judgements of (dependent) type theories and further away from categories than contextual categories and C-systems.