search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
397 stars 23 forks source link

Notation for constructors #113

Open UlrikBuchholtz opened 3 years ago

UlrikBuchholtz commented 3 years ago

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?

DanGrayson commented 3 years ago

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.

marcbezem commented 3 years ago

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.

DanGrayson commented 3 years ago

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.

bidundas commented 3 years ago

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.