UniMath/Foundations/Generalities/uuu.v: references to dependent sum as record about unimath HOT 6 CLOSED

I just now saw that these comments are mentioned in issue #111 too. Apologies for reporting a known issue!

from unimath.

Thanks for your comment! I updated the comment in #125 .

On 08/02/2015 10:43 AM, N. Raghavendra wrote:

There are comments in uuu.v saying:

"It contains some new notations for constructions defined in Coq.Init
library as well as the definition of dependent sum as a record."

"One could use "Inductive" instead of "Record" here but using
"Record" which is equivalent to "Structure" allows us later to use
the mechanism of canonical structures with total2."

They give the impression that dependent sums will be defined as
records. However the current definition of total2 uses Inductive, not
Record. Perhaps these comments can be removed or corrected.

from unimath.

Thank you for the correction.

There's still one comment in line 3 which says that the file defines dependent sums as records:

"It contains some new notations for constructions defined in Coq.Init library as well as the definition of dependent sum as a record."

from unimath.

Right, thanks. I updated #125.

On 08/02/2015 12:29 PM, N. Raghavendra wrote:

Thank you for the correction.

There's still one comment in line 3 which says that the file defines
dependent sums as records:

"It contains some new notations for constructions defined in Coq.Init
library as well as the definition of dependent sum as a record."

from unimath.

Thanks for reminding us about this inconsistency anyway. I suggest that we remove the comment.

On Aug 2, 2015, at 3:43 PM, N. Raghavendra [email protected] wrote:

There are comments in uuu.v saying:

"It contains some new notations for constructions defined in Coq.Init library as well as the definition of dependent sum as a record."

"One could use "Inductive" instead of "Record" here but using "Record" which is equivalent to "Structure" allows us later to use the mechanism of canonical structures with total2."

They give the impression that dependent sums will be defined as records. However the current definition of total2 uses Inductive, not Record. Perhaps these comments can be removed or corrected.

—
Reply to this email directly or view it on GitHub #124.

from unimath.

Fixed with PR #125 .

from unimath.