UniMath
new notation for paths over
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:
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.
I don't see vertical spacing of the lines as an issue. Lots of math books have tall notations.
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.
Well, maybe it's not always true. But that's what prose exposition is for.