Formalizing colimits in Cat

Mario Carneiro, Emily Riehl

Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite $\infty$-category theory has not been formalized. To s…