Effective Kan fibrations for simplicial groupoids, semisimplicial sets and Ex∞
Storm Diephuis

Abstract:
Homotopy type theory has a model inside the category of simplicial sets which is based on Kan fibrations, but the proof of this fact can demonstrably not be made constructive. Effective Kan fibrations were introduced as an alternative to Kan fibrations in hopes of acquiring a constructive model. We contribute various results to the theory of effective Kan fibrations. Firstly, three constructions of Kan fibrations based on simplicial groupoids are redone for effective Kan fibrations. Secondly, we show that all the information about degeneracy maps is stored in the lifting structure of an effective Kan complex, but argue that this has no practical application. Finally, we prove that the Ex∞ functor does not automatically produce an effective Kan complex, and argue that it is most likely not usable for fibrant replacement in the context of effective Kan fibrations. The positive results encourage a continued study of effective Kan fibrations, while the negative results teach us about its possible obstacles.