Homotopy Type Theory is conjectured to be the internal language of (∞,1)-topoi. In particular, the category of contexts of HoTT is an (∞, 1)-category. This (∞, 1)-cateory can be presented as a category with weak equivalences, where weak equivalences are given by the now customary type theoretic equivalences. But we can add more structure: namely we can define what are fibrations and cofibrations in type theory, so that the category of contexts be a model category. This was done by Gambino and Garner [GG] and Lumsdaine [Lum] and we will start by presenting their work.

Next we will consider moving to a two level type system like the one considered by Thorsten Altenkirch, to formalize those notions internally. Indeed, a strict equality satisfying UIP allows to formalize what is a strict category and a model structure over it.

Last, we will see how the model structure justify some homotopy colimit calculations from strict colimits.

[Lum] Lumsdaine, P. L. (2011). Model structures from higher inductive types. http://peterlefanulumsdaine.com/research/Lumsdaine-Model-strux-from-HITs.pdf.

[GG] Gambino, N., & Garner, R. (2008). The identity type weak factorisation system. Theoretical Computer Science, 409(1), 94-109.