Subtyping is a popular addition to dependent type theories to improve flexibility and modularity. We can already see it at work in established proof assistants and programming languages with cumulativity in Coq or refinement types in F*. However, the metatheory of such addition to actual frameworks has yet to be formally worked out, especially if we wish to implement more advanced subtyping features, {\em e.g.} relying on monotonicity. Using a syntactic model approach, we build prototype models for a type theory with refinement types and subtyping in the formal setting of a proof assistant. This allow us to explore the design space while rigorously establishing metatheoretical results.