What does `transp` do when the second argument is i1? about cubical HOT 5 CLOSED

Looking at your examples again, I think I see why this is necessary: the type of transp cannot depend on the value of the interval variable given. Recall the type of transp:

transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1

Thus if we want transp to be definitionally equal to a when r = i1, then we need to assert that A i0 is definitionally equal to A i1 (or equivalently, A is a constant function) in that case.

Yes, exactly.

I'm hoping someone who knows more about cubical type theory can also weigh in.

I don't have time to give a detailed answer, but the introduction of transp was motivated to be able to support HITs. This is discussed in:

https://arxiv.org/abs/1802.01170

Section 3.2 explains the typing rule and how to derive "squeeze" and "transFill" from it. These two operations are needed to explain how to compute comp in HITs. In CCHM (https://arxiv.org/abs/1611.02108) we had to define both squeeze and transport for propositional truncation (section 9.2) while with transp we only have to define one operation.

from cubical.

transport : ∀ {A B : Set} → A ≡ A → A → A
transport p a = transp (λ i → p i) i1 a

E:\TheoremProving\CubicalAgdaStuff\hello.agda:6,25-34
p i != A of type Set
when checking that the expression transp (λ i → p i) i1 a has type
A

I really did not expect this error.

transport : ∀ {A B : Set} → A ≡ A → A → A
transport p a = transp (λ i → p i0) i1 a

transport : ∀ {A B : Set} → A ≡ A → A → A
transport p a = transp (λ i → p i1) i1 a

These two on the other hand work.

I am confused as to what is going on here. Just what is transp doing and why was it designed like this?

from cubical.

From the agda docs:

There is an additional side condition to be satisfied for transp A r a to type-check, which is that A has to be constant on r. This means that A should be a constant function whenever the constraint r = i1 is satisfied. This side condition is vacuously true when r is i0, so there is nothing to check when writing transp A i0 a.

This explains why your middle two examples don't work. As for why this is what we want, I'm not sure – and I'm also curious about the answer! Perhaps it's so that transp always gives a path instead of a PathP?

from cubical.

Looking at your examples again, I think I see why this is necessary: the type of transp cannot depend on the value of the interval variable given. Recall the type of transp:

transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1

Thus if we want transp to be definitionally equal to a when r = i1, then we need to assert that A i0 is definitionally equal to A i1 (or equivalently, A is a constant function) in that case.

I'm hoping someone who knows more about cubical type theory can also weigh in.

from cubical.

Thank you for the replies. I had nearly forgotten that the docs existed. I think I understand transport well enough now after studying it for a while and debugging my mental errors. No doubt, I will have questions about other parts of Cubical Agda later.

from cubical.