On syntax and free objectsLast updated Feb 3, 2024Tags: Type theory, Categorical Logic (Shulman, 2016)