Andrew Swan: Introduction to Lifschitz realizability

Abstract: I will give an introduction to Lifschitz realizability from a synthetic point of view using higher modalities in homotopy type theory. I will briefly mention some new applications in the construction of models of type theory without propositional truncation.