mortberg
commented
2 years ago I think it's inspired by the type categories of section 6.3 in: https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf
I think whoever formalized that file was inspired by https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/ALV1/TypeCat.v
I did not look or think very closely about the definition that has been formalized in Cubical Agda, so maybe there's some mistake?
The module
Cubical.Categories.TypesOfCategories.TypeCategoryis not based on any notion of model of dependent type theory that I've encountered, and does not seem equivalent to any of those either. It starts as though it's going to become a CwF, but then instead of pairing a substitution with a term, it has functoriality of context extension. All in all, I think there is currently no way to use a term to create a substitution.