Syntactic Overhaul of Foundations about unimath HOT 10 CLOSED

(f : X -> Y) and { X Y : UU },
You suggest to not separate () with a space and separate {} with a space?

Perhaps introducing a new notation f ~ g for homotopies between functions.
Perhaps.

Then maybe also an infix for funcomp e.g. ( f circ g ), easily replaceable by unicode later.

The rest look good to me.

On Nov 5, 2014, at 5:20 PM, Alex Kavvos [email protected] wrote:

Following from recent lectures based on UniMath, I feel that a good part of Foundations, and especially uu0.v, could benefit from the following superficial changes in syntax:

Consistently replacing notations with the newly introduced set (@, =, !).
Perhaps introducing a new notation f ~ g for homotopies between functions.
Standardising the spacing in implicit and non-implicit arguments, e.g. (f : X -> Y) and { X Y : UU }, which may be slightly easier to read on a projector.
Word-wrapping at 95 or 100 characters per line.
Adhere to a stricter format of proofs, as exemplified in the example script in issue 33 [1].
[1] #33 #33
—
Reply to this email directly or view it on GitHub #47.

from unimath.

You suggest to not separate () with a space and separate {} with a space?

Yes. The choice was instinctive, although it probably derives from years of practice in imperative languages, where you would write things like

if (x == y) then { f(); return x; } else { g(); return y; }

But it is still up for debate.

The example code seems to stick with {X Y}; does Benedikt have any strong feelings about this?

from unimath.

There's probably not much reason to import C spacing conventions into Coq,
so it
might be good to treat () and {} identically.

On Wed, Nov 5, 2014 at 10:12 PM, Alex Kavvos [email protected]
wrote:

You suggest to not separate () with a space and separate {} with a space?

Yes. The choice was instinctive, although it probably derives from years
of practice in imperative languages, where you would write things like

if (x == y) then { f(); return x; } else { g(); return y; }

But it is still up for debate.

—
Reply to this email directly or view it on GitHub
#47 (comment).

from unimath.

I think you're right. I will stick to no spaces at all.

from unimath.

In my new code I am using ( X ) and { X }. V.

On Nov 5, 2014, at 10:12 PM, Alex Kavvos [email protected] wrote:

You suggest to not separate () with a space and separate {} with a space?

Yes. The choice was instinctive, although it probably derives from years of practice in imperative languages, where you would write things like

if (x == y) then { f(); return x; } else { g(); return y; }
But it is still up for debate.

—
Reply to this email directly or view it on GitHub #47 (comment).

from unimath.

For () and {} right? Because there is a reason to have spaces everywhere else since Coq considers are sequence of symbols without spaces (and probably () and {}) as a symbol and looks in the notation tables etc. trying to make sense of it.

V.

On Nov 6, 2014, at 12:08 AM, Alex Kavvos [email protected] wrote:

I think you're probably right. I will stick to no spaces at all.

—
Reply to this email directly or view it on GitHub #47 (comment).

from unimath.

Yes, exactly, for () and {} only.

As you will be using that convention, I will follow it too then.

from unimath.

It's hard to see how such superfluous spaces would ever be useful, at least
if
we resist the temptation to define new notations involving combinations like
(+ ... +), so I would not insert them.

On Thu, Nov 6, 2014 at 4:03 PM, Vladimir Voevodsky <[email protected]

wrote:

For () and {} right? Because there is a reason to have spaces everywhere
else since Coq considers are sequence of symbols without spaces (and
probably () and {}) as a symbol and looks in the notation tables etc.
trying to make sense of it.

V.

On Nov 6, 2014, at 12:08 AM, Alex Kavvos [email protected]
wrote:

I think you're probably right. I will stick to no spaces at all.

—
Reply to this email directly or view it on GitHub <
https://github.com/UniMath/UniMath/issues/47#issuecomment-61905839>.

—
Reply to this email directly or view it on GitHub
#47 (comment).

from unimath.

It seems to be slightly easier to read arguments like

( f : T1 -> T2 )

on screen -- only a little harder on paper or projector than without spaces. However,

phi : ( ( X -> Y ) -> Y ) -> Y

is harder to parse on any medium.

from unimath.

I just don’t think about it and insert a space between any two “words”. As long as it is not too terrible I think it is a
reasonable policy.

V.

On Nov 7, 2014, at 1:49 PM, Alex Kavvos [email protected] wrote:

It seems to be slightly easier to read arguments like

( f : T1 -> T2 )

on screen -- only a little harder on paper or projector than without spaces. However,

phi : ( ( X -> Y ) -> Y ) -> Y

is hard on any medium.

—
Reply to this email directly or view it on GitHub #47 (comment).

from unimath.