C-systems

Type theories are formal deduction systems similar in function to the system of predicate logic. They can be used to formalize reasoning about various aspects of the world. C-systems appear as the central class of objects in the mathematical study of type theories. They are essentially algebraic structures, i.e., algebraic structures where some operations are defined only for arguments that themselves satisfy equations on more basic operations. I will explain what C-systems are and how they arise from syntax on the one hand and from mathematical categories such as simplicial sets on the other.