I am trying to read "Homotopy Type Theory: The Logic of Space" https://www.cambridge.org/core/books/abs/new-spaces-in-mathematics/homotopy-type-theory-the-logic-of-space/D13957048F50112B531698F6FB6269EB (which is about classifying category of HoTT: types are objects and terms and morphisms) and "Model category of diffeological spaces" https://arxiv.org/abs/1605.06794
The first article mentions that types can be interpreted as (diffeological) spaces and one can wonder what category such spaces form? Maybe classifying category of HoTT and category of diffeological spaces are the categories with exactly the sames properties and there exists some functor (what?) among them?