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).