@jcreed Take the following with a grain of salt, since I'm a homotopy theorist, not a homotopy type theorist. Classically, what you would get, if these were spaces, is that A₀ is weakly contractible: for any n, it is (n-1)-connected because A₀ = Σⁿ Aₙ. This much should also be true in HoTT, so πₙ(A₀) = 0 for all n.

Now, I gather that HoTT has models in every (∞,1)-topos. But not every (∞,1)-topos is hypercomplete. In a hypercomplete (∞,1)-topos an object like A₀ with all homotopy groups vanishing would have to be contractible, but not so in a non-hypercomplete (∞,1)-topos.

I think this probably means that in HoTT A₀ is not necessarily contractible —but it still has vanishing homotopy groups, so, for example, all it's truncations ‖A₀‖ₙ are contractible.