Would it be possible to derive transp natively from Path, Interval and typecase?

Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm aware it is internally defined by pattern-matching on types, as explained here. But I'm slightly confused by the notation of this paper (and the presence of ϕ : F, which isn't cited on Agda's docs). My question is: is my understanding right that, if we further extended Agda with typecase, we would be able to recover transp as a function rather than a primitive? In other words, could we write:

transp : (I -> Type) -> I -> P(i0) -> P(i1)
transp (\ i -> Set)          i0 f = ...
transp (\ i -> ((x: A) -> B) i0 f = ...
transp A                     i1 f = f


Directly? How would such a proof work, and, for illustration purposes, what it would look like in Agda pseudocode? Obviously, no need to cover all types, just Set, dependent functions and perhaps pairs.

Additionally: 1. It seems that typecase itself isn't quite enough since we have A : I -> Type, not A : Type, so do we also need some kind of lamcase? 2. How could we enforce the "A must be a constant when r=i1" requisite interally?

• For ϕ : F you should check the original cubical type theory paper: F is a type of conditions that can be imposed on interval elements. In Cubical Agda we simplified it to just r : I since you can express a lot with just the condition r = i1. – Saizan May 28 at 12:14
• The typecase looks very suspicuous. Couldn't you use it to define a map which distinguishes two types that are equivalent? For instance, a map f such that f Unit = Unit and f (Unit * Unit) = Empty. This would then contradict univalence, and very likley destroy whatever use one might have for Interval and Path. – Andrej Bauer May 28 at 16:32
• @AndrejBauer yes, I think you're right. Does that mean that there is absolutely no way to implement transp from simpler primitives? Also, does that mean types can't be erased when compiling cubical languages, and that the runtime must have a complex transp "interpreter" that operates on types? – MaiaVictor May 28 at 17:02
• This distinction is important, because in any reasonable model not every type will be definable as some code (something built out of $\mathsf{Nat}$, $\times$, $\to$, etc). But all of those types must come equipped with these operations as well! This means that if we build in something like typecase, quite apart from problems with univalence, the resulting theory will lack any "natural" mathematical models. – Daniel Gratzer Jun 1 at 13:16
• @MaiaVictor $\mathsf{transp}$ is really one of several operations which is required to make a type fibrant. Without these operations the path type would be useless: it might fail to be an equivalence relation and may not enjoy a substitutive property. They're certainly not "unnatural": they correspond to typical conditions in homotopy theory to ensure that a cubical set is "space-like". Some of them are doubtless complex and, while there have been various simplifications over the years, I suspect that there is a kernel of intrinsic complexity. – Daniel Gratzer Jun 1 at 21:58