This project contains a formalization of the Quillen equivalent model category structures on the category of topological spaces and on the category of simplicial sets.
The main definitions are referenced in this file: https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/Test.lean