Idea An Infinity-topoi (or similar ∞-category) equipped with a univalent universe interpreting dependent types.