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 ,...)
betweenBool
andBool
and thusuniv (not ,...) : Bool =_U Bool
, and then using it, define a booleanb
: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 alongnot
, butcoe
was only defined for the caserefl
so the termb
does not compute further. One may think that it would be enought to add the equationcoe (univ (f,...)) ≡ f
but this is not sufficient as shown by the following example. Here we use theap
(apply path) function for aP : 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?