Jacopo Emmenegger: A weak factorization system between type theory and homotopy theory

We will briefly outline the construction of a category from the rules of Martin-Löf type, in order to present a result due to Gambino and Garner which endows such category with a weak factorization system. We will then present four categorical properties, reminiscent of the rules of Martin-Löf type theory, which allow us to prove a generalization of Gambino and Garner's result. Those properties are also satisfied by the category of topological spaces, and the weak factorization system obtained in this case is that one generated by Hurewicz fibrations.