<p>Assume for a moment that we extended Agda with an <code>Interval</code> and a <code>Path</code> type, but <strong>not</strong> transp (which is a primitive currently). I'm aware it is internally defined by pattern-matching on types, as explained <a href="http://www.cse.chalmers.se/~simonhu/misc/hcomp.pdf" rel="nofollow noreferrer">here</a>. But I'm slightly confused by the notation of this paper (and the presence of <code>ϕ : F</code>, which isn't cited on Agda's docs). My question is: is my understanding right that, if we further extended Agda with <code>typecase</code>, we would be able to recover <code>transp</code> as a function rather than a primitive? In other words, could we write:</p>

<pre><code>transp : (I -&gt; Type) -&gt; I -&gt; P(i0) -&gt; P(i1)
transp (\ i -&gt; Set)          i0 f = ...
transp (\ i -&gt; ((x: A) -&gt; B) i0 f = ...
transp A                     i1 f = f
</code></pre>

<p>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.</p>

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

CC BY-SA 4.0
2020-05-28T12:14:56.353Z
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
CC BY-SA 4.0
2020-05-28T16:32:42.067Z
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
CC BY-SA 4.0
2020-05-28T17:02:41.740Z
@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
CC BY-SA 4.0
2020-05-29T06:06:57.007Z
Well, what counts as "simpler" is up for discussion, but certainly transport won't come out of nowhere. All formulations of intensional identity types and path types have primitives that allow you to get transport one way or another. I do not understand what it means to "compile cubical languages". Compile to what? To a non-dependent language? If you're asking about how to *implement* them, yes I think the implementations look at the types to tell how to perform transport.
Andrej Bauer
CC BY-SA 4.0
2020-05-29T06:08:29.000Z
If you're interested in this sort of thing, you could attend the online ["Every proof assistant"](http://math.andrej.com/category/every-proof-assistant/) seminar on Cubical Agda on July 2nd.
Andrej Bauer
CC BY-SA 4.0
2020-06-01T13:13:50.627Z
One remark: it's a little misleading to think of $\mathsf{transp}$ as being defined by pattern-matching. This may be the implementation in the actual Haskell code, but semantically one should think of every type as coming equipped with its own implementation of $\mathsf{transp}$ and $\mathsf{(h)comp}$. It's extra structure that each type is already equipped with. For say, non-dependent sums ($A  \times B$), these operations are defined in terms of the operations that $A$ and $B$ are equipped with already.
daniel gratzer
CC BY-SA 4.0
2020-06-01T13:16:03.160Z
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
CC BY-SA 4.0
2020-06-01T19:58:46.840Z
@DanielGratzer do you agree `transp` is quite complex and unnatural to implement compared to the rest of the language and that there should be some more elegant way to achieve the same results, or do you think there is an unavoidable implementation complexity on cubical languages?
MaiaVictor
CC BY-SA 4.0
2020-06-01T21:58:09.320Z
@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
CC BY-SA 4.0
2020-06-03T17:48:50.713Z
@DanielGratzer I see. In this case I'll take the complexity as granted and try to absorb the concepts one by one. Thank you for this comment, it was helpful. At least now I'm confident that my approach was unproductive (as there is clearly not an obvious non-complex way to capture those concepts). Will also be looking forward for future simplifications on the core theory; I hope researchers don't stop at it just because it is implemented in some languages.
MaiaVictor
<type-theory><lambda-calculus><dependent-type>
Would it be possible to derive `transp` natively from Path, Interval and typecase?
MaiaVictor
# Would it be possible to derive `transp` natively from Path, Interval and typecase?

(Asked by: username_0 on 2020-05-28)

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?

**Tags:** type-theory, lambda-calculus, dependent-type
> **Comments:**
> **username_1**: 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`.  
> **username_2**: 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`.  
> **username_0**: @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?  
> **username_2**: Well, what counts as "simpler" is up for discussion, but certainly transport won't come out of nowhere. All formulations of intensional identity types and path types have primitives that allow you to get transport one way or another. I do not understand what it means to "compile cubical languages". Compile to what? To a non-dependent language? If you're asking about how to *implement* them, yes I think the implementations look at the types to tell how to perform transport.  
> **username_2**: If you're interested in this sort of thing, you could attend the online ["Every proof assistant"](http://math.andrej.com/category/every-proof-assistant/) seminar on Cubical Agda on July 2nd.  
> **username_3**: One remark: it's a little misleading to think of $\mathsf{transp}$ as being defined by pattern-matching. This may be the implementation in the actual Haskell code, but semantically one should think of every type as coming equipped with its own implementation of $\mathsf{transp}$ and $\mathsf{(h)comp}$. It's extra structure that each type is already equipped with. For say, non-dependent sums ($A  \times B$), these operations are defined in terms of the operations that $A$ and $B$ are equipped with already.  
> **username_3**: 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.  
> **username_0**: @DanielGratzer do you agree `transp` is quite complex and unnatural to implement compared to the rest of the language and that there should be some more elegant way to achieve the same results, or do you think there is an unavoidable implementation complexity on cubical languages?  
> **username_3**: @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.  
> **username_0**: @DanielGratzer I see. In this case I'll take the complexity as granted and try to absorb the concepts one by one. Thank you for this comment, it was helpful. At least now I'm confident that my approach was unproductive (as there is clearly not an obvious non-complex way to capture those concepts). Will also be looking forward for future simplifications on the core theory; I hope researchers don't stop at it just because it is implemented in some languages.  

---

## 0 answers

