First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory