A couple of years ago I have shown that the usual Kan-Quillen model structure on simplicial sets can be shown to exists constructively. But one of the main interest of constructive mathematics is that it can be interpreted in other categories than the category of sets, for example in toposes. So, in a more recent joint work with Gambino, Sattler and Szumilo we have studied this interpretation, which give rise to what we call the "effective model structure" on the category of simplicial object sE of a countably lextensive category E.
In this talk I will give an informal/high level overview of what goes in the proof of this constructive Kan-Quillen model structure and how it give rise to this "effective" model structure on simplicial objects. If time permits I will also talk about some results we proved about the homotopy theory of the effective model structure, and how it relates to equivariant homotopy theory and infinity categorical exact completion.