What are some interesting applications of homotopical algebra in theoretical computer science? I am an homotopy theorist, interested in computer science.

I would like to ask what are some interesting applications of homotopical algebra (model categories, infinity categories, simplicial categories, etc) in theoretical computer science?
Two big applications of homotopy theory in theoretical computer science are


Homotopy Type Theory revealed a completely unexpected connection between the theory of the typed lambda calculus and homotopy theory. As a quick intuition, think of it as either a (vast) generalization of the connection between intuitionistic logic and topological spaces, or a language for doing "synthetic homotopy theory".
The directed version of algebraic topology and homotopy theory (ie, where paths are not reversible) has been developed precisely with applications to computer science in mind. The intuition is that the possible evaluations of a concurrent program correspond to a space, program executions correspond to paths in that space, and synchronization primitives correspond to obstructions. By considering the geometric properties of these spaces/programs, it becomes possible to develop tools for reasoning about their behaviour.