Clarify extra condition on transp #4914
Conversation
|
@mortberg Thanks, this improved my patch! Updated and rebased. |
|
|
||
| * If ``r`` is ``i0`` then ``A`` can be anything, since this side | ||
| condition is vacuously true. | ||
|
|
||
| * If ``r`` is ``i1`` then ``A`` must be a constant function. | ||
|
|
||
| * If ``r`` is some in-scope variable ``i`` then ``A`` only needs to be | ||
| * If ``r`` is some in-scope variable ``i`` on which ``A`` depends as well, then ``A`` only needs to be | ||
| a constant function when substituting ``i1`` for ``i``. |
There was a problem hiding this comment.
the condition is still relevant even if A does not mention i, e.g. suppose we are in a context with variables, A : I -> Set, i : I, and x : A i0 then transp A i x will not typecheck. Or did you mean something else by this edit?
There was a problem hiding this comment.
@Saizan I thought that this case is covered in the previous bullet points, but I'm probably wrong then. How about "on which A may depend as well"?
There was a problem hiding this comment.
The previous bullet points do not cover the case where "r" is a variable in scope like "i".
Also, was the use of "convertible" rather than "equal" intentional? I'm not sure if "convertibility" is defined in the documentation anywhere.
There was a problem hiding this comment.
Ok, but would my new formulation be good?
Also, was the use of "convertible" rather than "equal" intentional? I'm not sure if "convertibility" is defined in the documentation anywhere.
Thanks for asking. Yes, "convertible" is presumably more precise because "equal" can mean so many things (starting with definitially vs. propositionally), and the whole point here is to make it more precise. But to be honest I don't know what "convertible" means or where it is defined. @mortberg do you have a hint?
There was a problem hiding this comment.
Maybe "definitionally/judgmentally equal" is better than "convertible". I don't know what is used elsewhere in the documentation for this equality
There was a problem hiding this comment.
Your new formulation would be good. Whether "A" depends or not on "i" is not strictly relevant to the condition, but I guess for transp A i to typecheck either A is always a constant function or it will mention i.
I imagine other readers would also not know about convertibility, I would rather use definitionally equal which is more descriptive at least.
andreasabel
added
cubical
See recent discussion: https://lists.chalmers.se/pipermail/agda/2020/012224.html