<div dir="ltr">Let me respond to some of your questions, although I am not an expert.<div><br></div><div>>But in this sentence, A is meant to be any expression, and it may contain r as a free variable.<br></div><div><br></div><div>I don't believe it is possible for A to contain r as a free variable. A has type A : I → Set ℓ. It is typical to use "r" to denote the input to a function whose domain is the interval; I think this is part of the confusion. But A should not be allowed to contain any reference to interval variables other than its bound input.</div><div><br></div><div>Thorston mentions that A can pattern match on "r" (here he is using r to refer to the input of A rather than the specific r passed to transport) but I don't believe this is correct (see section 3.1 of the Cubical Agda paper). One can only pattern match on an interval when creating "Partial" elements (see later in the doc). Someone correct me if I'm wrong.</div><div><br></div><div>>I still don't understand what's meant by A should be a constant function.<br></div><div><br></div><div>Since the type of A is I → Set ℓ it simply means that the value of A must not depend on its input (a member of the interval type). Of course there are some followup questions: How is this checked by the typechecker? And if A can't depend on its input why not just force it to have type Set ℓ?</div><div><br></div><div>I haven't looked at the code but I assume the check is a basic syntactic check that if A is of the form λ i → B then i cannot appear in B (so it may exclude functions which are not syntactically constant). However my understanding (again correct me if I'm wrong) is that this check only takes place when typechecking "transp A r" and r is not known to be i0. In the case r=i0 there is no constraint on A and A is allowed to be nonconstant. This happens in the definition of transport immediately below: "transport p a = transp (λ i → p i) i0 a". In this case A is not necessarily constant.</div><div><br></div><div>>At the end, doesn't transp A i always compute as the identity function? Isn't the point of transport to just verify that two types are equal so we can safely coerce?<br></div><div><br></div><div>No, transport takes a proof of the equality of two types as an input and then does the coercion. It need not be the identity function. For example, using the non-refl self-equivalence of Bool, transport should send true to false and vice-versa.</div><div><br></div><div>John</div></div>