docs: proof-reading the tutorial

[ulidtko]

Hi, Agda team!

Here's a small patch in the tutorial, doc/README*, with minor editorials: typos and the like.

I know it's always easier for (somebody else's) fresh set of eyeballs to do proof-reads. Thus, here goes.

Hoping for easy merge — there's no code change, just the docstrings.

[ulidtko]

BTW @andreasabel, thanks for reminding me!

This has been collecting dust for... turns out, exactly a year. I was initially meaning to go over all readme modules; alas, that hadn't happened. Uneasy times.

[JacquesCarette]

Wish I could do a 'request clarification' review. Basically this all looks good to me (but I'll want a second pair of eyes), except for the one thing that I comment on.

[Taneb]

Why was this paragraph removed?

[ulidtko]

@Taneb well, two reasons.

One: it seemed a bit misplaced... Just below, there's detailed exposition of Bundle re-exporting.

Two: it looks possibly outdated; talks about record Semigroup having a "repackaging function" semigroup which converts a Magma to a Semigroup — meanwhile, what's actually there in the definition, is the opposite: a function magma that projects the implied Magma out of the Semigroup.

Perhaps I misunderstood; please confirm. I can recover the paragraph easily, it just didn't read to me as correct neither helpful.

[jamesmckinna]

Actually, I think there's preferable solution to this problem, namely to rewrite the whole paragraph so as to explain (hopefully: better!) what's actually going on ... but for the unfortunate lack of distinction between a 'primitive'/'definitional' field and what elsewhere in PL would be called a 'manifest field', viz. the definitions made either explicitly (as with the magma example at hand), or by being brought into scope by an open declaration (as with isMagma on which it depends)

[jamesmckinna]

Suggest, therefore instead, as a drop-in replacement for the deleted paragraph (GitHub won't apparently let me add this as a suggestion, alas):

-- Note that the Semigroup record does not include a (primitive; definitional) Magma field, by contrast with the `IsSemigroup` structure which *does* include an `isMagma` field as primitive.
-- Instead, the Semigroup record includes an additional declaration (a 'manifest field' of the `record`) defining a `Magma` bundle, in terms of that exported `isMagma` field.
-- In this way, 'inheritance' is *automatic* for the `IsX` sub*structures* of a given bundle, while supporting the *optional* export of inherited sub*bundles*.

Now, I fully expect colleagues to object to my rephrasing... ;-) which is why I haven't tried to push such a commit to this PR without further discussion!

[jamesmckinna]

Thanks for offering this. I think it would be good to nail down the discussion with @Taneb before merging, though.

[jamesmckinna]

Comma seems worthwhile, but not sure about the increase in legibility/intelligibility arising from the change in/of preposition, maybe going all out and writing

Suggested change

	-- For example, in binary relations these are homogeneous and
	-- For example, in the case of binary relations these are homogeneous and

(possibly with knock-on consequences for the line-breaking/layout)

[jamesmckinna]

Suggest rewriting (rather than deleting) the paragraph in favour of (some version of) the suggestion below.
Either that, or reinstate the paragraph and we can have another go as a separate PR (but that seems 'wasteful', given that the one at hand already problematises the paragraph as needing fixing in some for or another...)

[jamesmckinna]

Actually, I think there's preferable solution to this problem, namely to rewrite the whole paragraph so as to explain (hopefully: better!) what's actually going on ... but for the unfortunate lack of distinction between a 'primitive'/'definitional' field and what elsewhere in PL would be called a 'manifest field', viz. the definitions made either explicitly (as with the magma example at hand), or by being brought into scope by an open declaration (as with isMagma on which it depends)

[jamesmckinna]

Suggest, therefore instead, as a drop-in replacement for the deleted paragraph (GitHub won't apparently let me add this as a suggestion, alas):

-- Note that the Semigroup record does not include a (primitive; definitional) Magma field, by contrast with the `IsSemigroup` structure which *does* include an `isMagma` field as primitive.
-- Instead, the Semigroup record includes an additional declaration (a 'manifest field' of the `record`) defining a `Magma` bundle, in terms of that exported `isMagma` field.
-- In this way, 'inheritance' is *automatic* for the `IsX` sub*structures* of a given bundle, while supporting the *optional* export of inherited sub*bundles*.

Now, I fully expect colleagues to object to my rephrasing... ;-) which is why I haven't tried to push such a commit to this PR without further discussion!