UniMath
Notation for constructors
Currently, many constructors, inl, inr, refl, are written with the argument as a subscript, but we also type them as functions. Perhaps it would be better to just use function application notation?
Perhaps we could do it this way: use the notation foo_x only for families of elements in a family of types, and use the notation foo(x) only for function application. Section 2.2, where families are introduced. We could easily edit that to adhere to such a standard, and that would remove some notation ambiguity that will be irksome for the student.
As we discussed, this could become problematic if the subscript is a complicated expression, or is itself a family of elements. Sometimes, computations will happen in the subscript. I'm in favour of allowing both in all cases, dependent and non-dependent. For example, a sequence in R could be denoted as a function s : N -> R and also as a family of elements s_n for any n:N. In any particular case one can then make the best choice. In some cases the choices can be equally good.
Yes, it can be a matter of taste whether you use a family or a function. Similarly, it can be a matter of taste whether you want subscripts or function applications.
Agree. We don't need to be totally consistent at just this point.
Bjorn
On 1 Jul 2021, at 19:22, Daniel R. Grayson @.***> wrote:
Yes, it can be a matter of taste whether you use a family or a function. Similarly, it can be a matter of taste whether you want subscripts or function applications.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.
