A Type Theory for Synthetic ∞-Categories