\equiv

[DanGrayson]

Let's do for \equiv what we did for = --- use \equivto for the type of equivalences and \equiv for its propositional truncation.

[DanGrayson]

Add them to the glossary, too.

[marcbezem]

Thinking more about this I realized there are some more issues to be solved, including the following.

1. In diagrams we currently label equivalence arrows with $\sim$ (e.g., (2.26.1)). Should this become $\equiv$? (Vote: yes)
2. If a type is not a set, it is still possible that some identity types are propositional. Example: in the universe, identification with a contractible type is propositional. How do we denote this? For $A:U$, do we write $A = 1$ or $A \eqto 1$? The choice for $A = 1$ would raise this question: what is the type of = ? (Vote: only use = as an alternative notation for $\eqto$ if the type is a set, similarly for all other ..to macros, if any)
3. If I understand our conclusion from last week, Def. 2.16.9 and Rem. 2.16.10 will be removed, since they make = slightly ambiguous in the case of a propositional identity type, and do not bring = closer to mathematical practice.
4. In the first line of the proof of Lem. 2.9.9 there is a $g \eqto f^{-1}$ which I think should be $g \defeq f^{-1}$. This happened because in the previous version there we a =, which should also have been $\defeq$.
5. Making the notation for = asymmetrical kind of strengthens the terminology "symmetry" for elements of $a \eqto a$. This could perhaps be elaborated with a sentence or so, around footnote 19 on page 12. Is "numbers don't have symmetries" in fact correct? I would prefer "the only symmetry of a number is the reflexivity path".
6. Is $\eqto_A$ in style, or should type A be delegated to the context? (Analogously for the type family in a path over)

[DanGrayson]

1. Certainly we should label arrows in diagrams the same way we label arrows in the text.
2. Having two meanings for = depending on the context would be much too confusing.
3. No, I think they stay. It's the whole point of the notation.
4. Fixed in commit 670da28c2d1e2d07819ef7839767a19f5b976721
5. I've changed it to "numbers don't have non-trivial symmetries" in commit 2f5839df919f893708a1d9f9fa43c88f394d0535
6. We haven't defined that notation. Every expression has a well-defined type, so we could depend on the context.

[marcbezem]

3. Let's discuss this again on Thursday. When Bjørn asked this, I had the impression I was not the only one who was "not comfortable" with Def.2.16.9. Two examples: 1+1=2 now stands for the propositional truncation of an inductive identity type; and a substitution principle like (a=b) -> P(a) -> P(b) would only hold for P a family of propositions. Do we have examples where this use of = is really better than writing the propositional truncation explicitly?

[bidundas]

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:



1. Let's discuss this again on Thursday. When Bjørn asked this, I had the impression I was not the only one who was "not comfortable" with Def.2.16.9. Two examples: 1+1=2 now stands for the propositional truncation of an inductive identity type; and a substitution principle like (a=b) -> P(a) -> P(b) would only hold for P a family of propositions. Do we have examples where this use of = is really better than writing the propositional truncation explicitly?

— 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: @.***>

[marcbezem]

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.

[bidundas]

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: @.***>

[DanGrayson]

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.

[marcbezem]

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.

[DanGrayson]

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:

[DanGrayson]

Okay, we've agreed:

• to not define x=y as the propositional truncation of the identity type
• to use x=y to mean the identity type only when x and y are elements of a set

The same goes for equivalence.

[DanGrayson]

And let's not use \equiv for the propositional truncation of \equivto.

[bidundas]

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:

• to not define x=y as the propositional truncation of the identity type
• to use x=y to mean the identity type only when x and y are elements of a set

— 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: @.***>