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
: 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?