\lam about book

[favonia]

I can't parse the lambda at https://github.com/HoTT/book/blob/master/ua-fe.tex#L47 (Hmm... maybe the author should use other symbols?)

[mikeshulman]

The \lambda on that line is the name of a function, whose definition
appears on the following line: it takes a function to its eta-expansion.

On Fri, Mar 29, 2013 at 4:06 PM, 西風 [email protected] wrote:

I can't parse the lambda at
https://github.com/HoTT/book/blob/master/ua-fe.tex#L47

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/44#issuecomment-15658219
.

[guillaumebrunerie]

Don't we have definitional eta? I thought we decided that last time.
On Mar 29, 2013 4:09 PM, "Mike Shulman" [email protected] wrote:

The \lambda on that line is the name of a function, whose definition
appears on the following line: it takes a function to its eta-expansion.

On Fri, Mar 29, 2013 at 4:06 PM, 西風 [email protected] wrote:

I can't parse the lambda at
https://github.com/HoTT/book/blob/master/ua-fe.tex#L47

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/44#issuecomment-15658219>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/44#issuecomment-15658319
.

[mikeshulman]

Yes, we do. So that part should also be rewritten.

On Fri, Mar 29, 2013 at 4:11 PM, Guillaume Brunerie <
[email protected]> wrote:

Don't we have definitional eta? I thought we decided that last time.
On Mar 29, 2013 4:09 PM, "Mike Shulman" [email protected] wrote:

The \lambda on that line is the name of a function, whose definition
appears on the following line: it takes a function to its eta-expansion.

On Fri, Mar 29, 2013 at 4:06 PM, 西風 [email protected] wrote:

I can't parse the lambda at
https://github.com/HoTT/book/blob/master/ua-fe.tex#L47

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/44#issuecomment-15658219>
.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/44#issuecomment-15658319>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/44#issuecomment-15658429
.

[favonia]

@mikeshulman I figured that out, but still feel authors should use other symbols if possible.

[mikeshulman]

I agree, it is confusing to use \lambda to mean the eta-expansion. Why don't you change it?

[favonia]

I'd be happy to but let me ask something first. Are we going to use uatofe.tex and drop ua-fe.tex?

Other than this, the conversion is done.

[mikeshulman]

That's probably a question for Peter Aczel.

On Fri, Mar 29, 2013 at 4:39 PM, 西風 [email protected] wrote:

I'd be happy to but let me ask something first. Are we going to use
uatofe.tex and drop ua-fe.tex?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/44#issuecomment-15659607
.

[favonia]

I'll ask him. Closing the Issue.