Continuing the example of why it's hard to compute with univalence?
You are correct, in the sense that the elusive computational nature of Univalence is not so elusive for "ordinary" type constructors.

In fact, you might want to glance at Tabareau, Tanter and Sozeau's paper Equivalences for Free!, which outlines what you have just written, along with many more types of, well, types.

Trouble starts (as usual!) with dependent types, particularly when equivalent types start appearing in indices. Take the following type:

IndexedList (A : Type) : List A -&gt; Type :=
   | INil : IndexedList A []
   | ICons : forall (a : A) (l : List A) (il : IndexedList A l), IndexedList A (a::l)


It's an interesting exercise to write down ap_IndexedList in this case, it's not trivial! But once this is done you then have to take into account types that depend on types that depend on $A$, etc. This is where things get pretty hairy.

Homotopy type theorists want to be able to describe this theory in full generality, since only this will capture the "ideal" of a constructive model of homotopy types.

But as Tabareau &amp; al mention, this is not really all that useful for programing applications, where "single index nesting" is really all that is necessary (for the most part, obviously then proving things about dependent types might require more). So as far as computer scientists are concerned, we're pretty much ready for univalence!