The talk will give an overview of categorical semantics - a magical tool that puts our wanted loose ways of reasoning on solid ground. We’ll discuss how Grothendieck generic freeness lemma is “internally” a simple one-liner, in what secret sense Spec A is free, why intuitionistic mathematics is so natural, and maybe even how to approach algebraic geometry synthetically (i.e. with no set theory references).