Splitting dictoses

In old work by Martin Hofmann (CSL 1994) he used Giraud's right adjoint
splitting for splitting locally cartesian closed categories in order to
make them ready for interpreting the syntax of MLTT. He observed that
there were problems with extending this work to impredicative universes
as in Ehrhard's dictoses (a notion of model for Calculus of
Constructions).

I will describe recent attempts based on different methods of splitting
models. I will try to pinpoint where they fail and will isolate the key
problem, namely that splitting small universes may make them big.