Closed DanGrayson closed 2 years ago
Add them to the glossary, too.
Thinking more about this I realized there are some more issues to be solved, including the following.
I’m at a motivic conference and am unavailable Thursday afternoon. I’m comfortable with any clear conclusion
Bjorn
On 9 Aug 2022, at 20:30, Marc Bezem @.***> wrote:
— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/145#issuecomment-1209737261, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK3HS5TOFTAQ77HK6QDVYKPVPANCNFSM55SZIV7Q. You are receiving this because you are subscribed to this thread.Message ID: @.***>
My proposal would be to define $x =_A y$ as $(x \eqto y) \times \isset(A)$, with conventions that allow to omit the proof of $\isset(A)$ and to drop the subscript $A$ if $A$ is clear from the context. I think this is argueably closer to = in ordinary mathematics, at least in comparison = in the HoTT-book (stretching = to higher identities), and to Def. 2.16.9 (stretching = to truncated higher identities). All versions are equivalent on sets.
I'm fine with this
Bjorn
On 11 Aug 2022, at 10:40, Marc Bezem @.***> wrote:
My proposal would be to define $x =_A y$ as $(x \eqto y) \times \isset(A)$, with conventions that allow to omit the proof of $\isset(A)$ and to drop the subscript $A$ if $A$ is clear from the context. I think this is argueably closer to = in ordinary mathematics, at least in comparison = in the HoTT-book (stretching = to higher identities), and to Def. 2.16.9 (stretching = to truncated higher identities). All versions are equivalent on sets.
— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/145#issuecomment-1211702994, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SK4T2BSP2F6XIF2FQ43VYS37PANCNFSM55SZIV7Q. You are receiving this because you commented.Message ID: @.***>
My proposal would be to define x=Ay as (x\eqtoy)×\isset(A), with conventions that allow to omit the proof of \isset(A) and to drop the subscript A if A is clear from the context. I think this is argueably closer to = in ordinary mathematics, at least in comparison = in the HoTT-book (stretching = to higher identities), and to Def. 2.16.9 (stretching = to truncated higher identities). All versions are equivalent on sets.
That would mean that in a non-set, two elements are never equal. I think that goes against standard mathematical practice. For example, two groups can be isomorphic.
Opinions by others:
Mazur (Bjørn showed me this back in 2018 at CAS): When is one thing equal to some other thing
Serre: How to write mathematics badly
Shulman et al.: discussion on zulip on = in Agda
Another point that occurred to me: with Def. 2.16.9, formalizing equality reasoning with = in a set becomes more tedious.
Another point that occurred to me: with Def. 2.16.9, formalizing equality reasoning with = in a set becomes more tedious.
That's the purpose of the next remark:
Okay, we've agreed:
The same goes for equivalence.
And let's not use \equiv for the propositional truncation of \equivto.
amen
From: Daniel R. Grayson @.***> Sent: Thursday, August 18, 2022 4:46 PM To: UniMath/SymmetryBook Cc: Bjorn Ian Dundas; Comment Subject: Re: [UniMath/SymmetryBook] \equiv (Issue #145)
Okay, we've agreed:
— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/145#issuecomment-1219586984, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SKY27DCGFLWLVLEOG7DVZZEFPANCNFSM55SZIV7Q. You are receiving this because you commented.Message ID: @.***>
Let's do for \equiv what we did for = --- use \equivto for the type of equivalences and \equiv for its propositional truncation.