propositional truncation of identity

[DanGrayson]

In group theory, not only do we consider isomorphisms between G and H, but we also have the adjective "isomorphic", which corresponds to the propositional truncation of the identity type. In set theory, equations are always propositions, and it's tempting to say "let's prove that G = H". If we were to use the notation G ≡ H for the identity type and G = H for its propositional truncation, it might add some flexibility to our language.

[UlrikBuchholtz]

OK, but why ≡ for the identity type? (Which we're already using for definitional equality.)

We're not using ≅ for anything at the moment. Would that work to denote the identity type?

[marcbezem]

And why only for groups? The book is full of truncated identities (components, for example).

[pierrecagne]

I would suggest to use a new sign for the propositional truncation of the identity types rather than for the identity types. (Actually I would suggest to keep it the way it is, I don't think truncations are so hard to read.)

The use of = for identity types is well-established afaik in the community (the alternative being Id(-,-)) and it would probably be misleading to redefine the symbol.

[DanGrayson]

[UlrikBuchholtz]

I'll make the macros.

[UlrikBuchholtz]

Here are the suggested macros: I like the idea of having the untruncated macro be the truncated macro plus to, but I'm not committed to the names of the untruncated ones.

Another issue is whether to keep \we (arrow with tilde). It can always be replaced by \equivto, but in a big diagram it might look better with just a tilde to indicate an equivalence. And when drawing paths in a type (e.g., ft. 20), we shouldn't have to put equals signs on the arrows, since it's clear that it's an identification.

If you like the above, I'll commit it and push it.

[bidundas]

I like it.

There is a slight inconsistency in that we’d tend to use the WORD “to” as in “a is equal TO b” for the truncated version. I can live with that.

Bjorn

On 29 Oct 2021, at 09:13, Ulrik Buchholtz @.***> wrote:

Here are the suggested macros:

I like the idea of having all the untruncated macro be the truncated macro plus to, but I'm not committed to the names of the untruncated ones.

Another issue is whether to keep \we (arrow with tilde). It can always be replaced by \equivto, but in a big diagram it might look better with just a tilde to indicate an equivalence. And when drawing paths in a type (e.g., ft. 20), we shouldn't have to put equals signs on the arrows, since it's clear that it's an identification.

If you like the above, I'll commit it and push it.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[DanGrayson]

I like it.