Reflective property in computational category theory In Rydeheard-Burstall's book on computational category theory they articulate several models for computing with categories.  For a computational category theory based on types they refer to one built by Dyckhoff from 1985 which is based on a Martin-Lof dependent type theory.  The authors point out that this model still falls short in that it does not handle the reflective aspect of categories.  That is, the use of a hierarchy $\mathfrak{U}_0$, $\mathfrak{U}_1,\ldots$ of universes makes for the category of categories to be limited to the category of categories of types in universe $\mathfrak{U}_a$ but not actually all types at once (page 231).  (If I understand them correctly.)  They point out that Coquand found inconsistency when you try to glue it all together into a single universe (page 218).
Has any typed model of categories emerged since that does have an honest category of categories?  Perhaps more broadly would an intuitionistic view of categories have a category ${\sf Cat}$ at all?
 A: There are no particular challenges about defining categories in an intuitionistic logic/type theory. Some results are not constructively valid and thus don't hold, or they motivate some modifications to allow them to hold. One major one is the characterization of equivalence of categories as a full, faithful, and essentially surjective functor. To show that this is equivalent to the definition in terms of a unit and counit requires the Axiom of Choice and so isn't constructively valid. One solution is instead of talking about functors, you can talk about anafunctors. There are reasons to do this even in classical mathematics. That said, in my experience, constructive definitions of categories don't usually use anafunctors, and they just don't particularly care about full, faithful, and essentially surjective functors.
To your main question, I think what Rydeheard and Burstall mean is simply that you'd like to define a notion of product-in-a-category, say, and then be able to apply it to a category of categories to get the notion of a product category. The problem is a definition of product in a $\mathcal U_1$-category won't apply to the category of $\mathcal U_1$-categories which is a $\mathcal U_2$-category.
Forming a "true" "category of all categories" seems like it will lead to inconsistency pretty quickly. In a traditional set theory, you could define a class of all categories and give it some categorical structure via class functions, but it would be a different thing than the sets it classifies. It's also somewhat awkward to formulate definitions entirely as predicates. Regardless, the upshot is that you end up with two (or more) definitions of concepts: one for "class-level" notions and one for set-level notions. This is more or less the problem Rydeheard and Burstall wanted to avoid.
The typical solution for this in set theory is to assume the existence of Grothendieck universes, which do produce this stratification, but then you can at least parameterize definitions by universes. For type theory, the solution is the same. Type theoretic universes serve much the same purpose as Grothendieck universes, and the way to resolve Rydeheard and Burstall's issue is to support universe polymorphism which modern implementations of intuitionistic type theory, such as Agda, do. It's still possible to run into situations where you need superuniverses, but this won't come up for the vast majority of what people want to do with categories. (One place it can come up is when you try to formalize certain $\infty$-categories.)
