nLab9d ago

formal (infinity,1)-category theory

p
Formal -category theory is to -category theory what formal category theory is to 1-category theory, that is: a synthetic approach to -categories standing in relation to synthetic homotopy theory as -category theory stands to homotopy theory. Consequently, formal -category theory has also been called synthetic -category theory. There have been two main styles of approaches to formal -category theory: categorical, which are -categorical in nature; and type theoretic, which propose deductive...