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
371 stars 22 forks source link

new notation for paths over #135

Open DanGrayson opened 2 years ago

DanGrayson commented 2 years ago

What should our new notation for paths over be?

Screen Shot 2022-01-13 at 4 20 40 PM
DanGrayson commented 2 years ago

Maybe this would work:

Screen Shot 2022-01-13 at 4 29 33 PM
marcbezem commented 2 years ago

The type family is not expressable in this notation.

And it has the disadvantage that it will always affect the vertical spacing of lines (the old notation only did this with complicated super- and subscripts, which could be solved by introducing abbreviations).

There could also be some confusing with the labelling of arrows in diagrams.

Maybe this would work:

<img width="588" alt="Screen Shot 2022-01-13 at 4 29 33 PM" src="https://user-images.githubusercontent.com/700228/149430491-00cb1714-b3cf-4a65-b482-ad0cffc57d5e.png">

DanGrayson commented 2 years ago

Another disadvantage is possible confusion with commutative diagrams:

Screen Shot 2022-01-14 at 8 39 20 AM
DanGrayson commented 2 years ago

The type family doesn't have to be part of the notation, since the endpoints are elements in members of the family, allowing the type family to be deduced.

DanGrayson commented 2 years ago

I don't see vertical spacing of the lines as an issue. Lots of math books have tall notations.

marcbezem commented 2 years ago

On 2022-01-14 17:40, Daniel R. Grayson wrote:

The type family doesn't have to be part of the notation, since the endpoints are elements in members of the family, allowing the type family to be deduced.

Is that always true? If p: a=a, then the type families P(,a) and P(a,) are hard to distinguish.

DanGrayson commented 2 years ago

Well, maybe it's not always true. But that's what prose exposition is for.