On syntax and free objectsLast updated Oct 4, 2022Tags: Type theory, Categorical Logic (Shulman, 2016)