The model independence of (∞,1)-category theory has never been in doubt, but it was unclear whether the model-independence of (∞,1)-category could be proven systematically, or whether "experts" would have to be relied on to provide ad hoc translations between models. Compounding this issue is the inevitable subtlety in understanding which statements about (∞,1)-categories are model-independent. For instance, the completeness axiom for Segal spaces has no clear analogue in the other models.
In past work, we have shown that a large part of the theory of (∞,1)-categories can be developed formally in the virtual equipment of modules, and moreover that the virtual equipments associated to the common models of (∞,1)-categories are all "biequivalent" in a suitable sense. In this talk we adapt Makkai's First Order Logic with Dependent Sorts to define a formal language for writing statements about (∞,1)-categories, and prove that the validity of every formula written in that language is invariant under change of model.
This is joint work with Dominic Verity.