Last paragraph of 2.16
Closed this issue · 9 comments
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.
Good idea. I think it's not worth the trouble using P \equiv Q for propositions, when we could use P <=> Q instead.
We should also introduce a macro "\equivto", which is an arrow with the equiv symbol on top.
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.
Yes, but that idea is a new one, and certainly our students have run into "if and only if" before.
I'd vote in favor of a double two-way arrow. ( <=> )
It's completely standard notation in mathematics.
Resolved!