UniMath
= versus \equiv
Dan, Peter, and Marc have been discussing when to use = and when to use \equiv between types. Here is our temporary conclusion:
For any types A and B, if an element of A=B can be constructed (sic) without UA, then use A=B, otherwise use A \equiv B.
The reason is that we would like to avoid unnecessary use of UA, in particular as the last and only step in the construction (sic) of an element of type A=B.
I’m not really involved in the book (yet), but I think this issue is worth an in-person discussion — especially after Dan’s talk today, which reminded us again of how alien this idea is to “normal” mathematicians. at the risk of re-opening this can of worms, perhaps we should have an open discussion of this issue when the “new generation” of CAS'ers arrives next week?
Steve
On Mar 28, 2019, at 6:58 PM, Marc Bezem [email protected] wrote:
Dan, Peter, and Marc have been discussing when to use = and when to use \equiv between types. Here is our temporary conclusion:
For any types A and B, if an element of A=B can be constructed (sic) without UA, then use A=B, otherwise use A \equiv B.
The reason is that we would like to avoid unnecessary use of UA, in particular as the last and only step in the construction (sic) of an element of type A=B.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/UniMath/SymmetryBook/issues/27, or mute the thread https://github.com/notifications/unsubscribe-auth/AAqtSIa5_uZuiXeR82H_xSiZvxC2eRCHks5vbQKsgaJpZM4cQx_g.
Excellent idea. The discussion could also touch upon phrasings like "the construction (sic) of an element of type A=B", where I wrote "(sic)" as a small provocation, as compared to "proving A=B".
Marc PS github has the advantage that the CAS'ers who leave can still participate.
It's hard to speak completely in a proof relevant way. For example, try never to say that "equality is transitive".
I'm probably the offender here, but most of my travesties came after we had had some discussions on this. While we don't want to convey a false impression (and obviously some of the things are plainly false as they are written and in need of revisions - that also goes for things of a totally different nature) the sentiment when I asked "how ingrained in the text should ua be" was that we wanted to pass rather freely back and forth.
From my categorical perspective; if p : A = B and f : B -> C, being refused to write f p : A -> C and forced to write some complicated thing like f fst idtoequiv p risks alienating the reader.
We should have clear and transparent conventions on this rather than the text looking like a source file (\smileyface: exaggeration for effect only).
The above example is 99% fine with me, the missing 1% is the use of the new notational convention proposed by Steve, and supported by these macros:
\newcommand{\etop}[1]{\bar {#1}} \newcommand{\ptoe}[1]{\tilde {#1}}
Then it would become f \ptoe{p} : A -> C. We could pedal back, but I still like Steve's proposal.
The discussion with Dan and Peter was rather about cases like A = (1->A).
ok, underscores Steve's point that it is worthwhile discussing these things in person (first). That can save some time, and then open issues when we're in doubt.
I think we should have this discussion soon. The dilemma crops up everywhere, e.g., at the end of 2.5:
The following lemma will be useful later. Definition 2.5.4. ...