The independence of premise principle says roughly that if a hypothesis P implies the existence of some object satisfying a property Q, and if P itself carries no computational content beyond its truth, then one can extract the witnessing object without committing to P first. The recent resolution of this principle for intuitionistic Zermelo-Fraenkel set theory used specific proof-theoretic and realizability techniques tailored to that system. The open question is whether these techniques can be lifted uniformly to dependent type theories equipped with a hierarchy of universes, which are the foundations underlying modern proof assistants like Coq and Agda. Such systems have a richer universe structure that interacts in subtle ways with logical principles and creates new obstacles for realizability arguments.