Dear all,

Readers of this list may be interested in the following series of papers:

[1] S. Henry, Weak model categories in classical and constructive mathematics, 

[2] S. Henry, A constructive account of the Kan-Quillen model structure and of Kan's Ex∞ functor, 

  https://arxiv.org/abs/1905.06160

[3] N. Gambino, C. Sattler, K. Szumiło, The constructive Kan-Quillen model structure: two new proofs

[4] N. Gambino, S. Henry, Towards a constructive simplicial model of Univalent Foundations

Apologies for cross-posting.

With best regards,

Nicola