search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
371 stars 22 forks source link

Last paragraph of 2.16 #167

Closed marcbezem closed 10 months ago

marcbezem commented 1 year ago

The last paragraph of 2.16 defines being equivalent as the truncation of the type of equivalences. I think we decided not to do this, neither for equality, not for equivalence. Hence I propose to remove this paragraph.

Instead, we could certainly keep using P \equiv Q for propositions P and Q, compatible with the use of = between elements of a set. For general types X and Y, I think we decided to avoid saying that they are equivalent without further indication of the equivalence one has in mind. To avoid awkward sentences we could perhaps be a bit lenient here. Rudimentary suggestion of the equivalence could be sufficient, such as "canonically equivalent", "by univalence, X\eqto Y and X\equiv Y are equivalent", "by function extensionality, f\eqto g and ... are equivalent", "we have an equivalence from X to Y" without giving it a name, etc.

DanGrayson commented 1 year ago

Good idea. I think it's not worth the trouble using P \equiv Q for propositions, when we could use P <=> Q instead.

DanGrayson commented 1 year ago

We should also introduce a macro "\equivto", which is an arrow with the equiv symbol on top.

marcbezem commented 1 year ago

We have \equivto already, and it is actively used. As a logician I like your proposal if it can be \leftrightarrow (not double). However, it deviates from the idea behind the \eq and \eqto, \equiv and \equivto, etc.

DanGrayson commented 1 year ago

Yes, but that idea is a new one, and certainly our students have run into "if and only if" before.

bidundas commented 1 year ago

I’d vote against a arrow with tips in both ends.

Bjorn

On Dec 14, 2022, at 18:04, Daniel R. Grayson @.***> wrote:

Yes, but that idea is a new one, and certainly our students have run into "if and only if" before.

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.

DanGrayson commented 1 year ago

I'd vote in favor of a double two-way arrow. ( <=> )

bidundas commented 1 year ago

Correction: I’d vote against aNY arrow with tips in both ends.

Like double-edged swords they are prone to hurt the handler.

Bjorn

On Dec 14, 2022, at 18:57, Daniel R. Grayson @.***> wrote:

I'd vote in favor of a double two-way arrow. ( <=> )

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.

DanGrayson commented 1 year ago

It's completely standard notation in mathematics.

UlrikBuchholtz commented 10 months ago

Resolved!