Continuing the example of why it's hard to compute with univalence?

Question

In "Towards a cubical type theory without an interval" Altenkirch and Kaposi motivate why it is hard to compute with univalence. They say:

For example, we can define the equivalence (not ,...) between Bool and Bool and thus univ (not ,...) : Bool =_U Bool, and then using it, define a boolean b:

coe : (A =_U B) → A → B
coe (refl A) a :≡ a

b : Bool
b :≡ coe (univ (not, ...)) true

We know that b should be false as we coerce along not, but coe was only defined for the case refl so the term b does not compute further. One may think that it would be enought to add the equation coe (univ (f,...)) ≡ f but this is not sufficient as shown by the following example. Here we use the ap (apply path) function for a P : U → U :

ap_P : A =_U B → P A =_U P B
ap_P (refl A) ≡ refl (P A)

x : P Bool =_U P Bool
x :≡ ap_P (univ (not, ...))

To reduce this term we need to know how to transport an equivalence along an arbitrary type.

What I don't understand is the last sentence. Is the "arbitrary type" the result of applying P to Bool? I feel that for any given P : U → U we can write a corresponding ap_P. For example:

Maybe : U → U
Maybe A = () + A

Show : U → U
Show A = A → String

Endo : U → U
Endo A = A → A

ap_Maybe (univ (f, g, ...)) = univ (either id f, either id g, ...)
ap_Show (univ (f, g, ...)) = univ (\show -> show . g, \show -> show . f, ...)
ap_Endo (univ (f, g, ...)) = univ (\endo -> f . endo . g, \endo -> g . endo . f, ...)

Is this intuition already off? What would be a concrete P where this fails? Or is the problem that while we know how to transport an equivalence along any function P : U → U we don't know how to do it for all such functions?

Answer 1

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 -> 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 & 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!