Aiming to give a synthetic account of ∞-category theory, Riehl and Shulman introduced simplicial homotopy type theory (sHoTT) allowing one to reason about (complete) Segal spaces in type theory. I will explain how one can develop a fair amount of fibered category theory in that context a lot of which resembles Riehl and Verity's ∞-cosmos theory. Some of these results have also been formalized in the proof assistant Rzk. Afterwards, I will present recent constructions in a modal extension of sHoTT including the (∞,1)-category of ∞-groupoids and the Yoneda embedding together with some applications e.g. to the theory of Kan extensions. The talk is based on joint work with Daniel Gratzer & Ulrik Buchholtz as well as Nikolai Kudasov & Emily Riehl.