Algebraic Monoidal Model Categories and Path Category Structures for Effective Kan Fibrations
Lingyuan Ye

Abstract:
In this document, we first develop a general framework to lift the pushout-product axioms in classical homotopy theory to the structured context of algebraic weak factorisation systems. The outcome is a notion of an algebraic monoidal model category. Within this framework, we are able to formulate and prove a structured analogue of Joyal-Tierney calculus, with the help of which we put an algebraic monoidal structure on effective Kan fibrations.
Effective Kan fibration is a new notion of fibration introduced in [63], in order to develop a constructive model of homotopy type theory on simplicial sets. In the second part of this document, we show there is a path category structure on the full subcategory of effective Kan fibrations over any object, using the algebraic monoidal structure constructed earlider. This brings us closer to showing the existence of a full model structure. Finally, we also identify a key semantic property, which we refer to as Moore equivalence extension. Based on the results in this document, we are able to show that if simplicial sets satisfy this property, then there exists a full algebraic monoidal model category structure for effective Kan fibrations.