Model structure on the universe in a two level type theory
Model structure on the universe in a two level type theory
There is an ongoing connection between type theory and homotopy theory, based on the similarity between types and the notion of homotopy types for topological spaces. This idea has been made precise by exhibiting the category cSet of cubical sets as a model of homotopy type theory. It is natural …