being equivalent

[DanGrayson]

If we speak of two types being equivalent, it sounds like equivalence is a proposition. We don't do that for equality. What should we do?

[bidundas]

I'd prefer to avoid 'equivalent' in this sense, and if used it should refer to the propositional truncation of the type of equivalences.

Bjorn

On 5 Aug 2021, at 22:00, Daniel R. Grayson @.***> wrote:

If we speak of two types being equivalent, it sounds like equivalence is a proposition. We don't do that for equality. What should we do?

— 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]

Instead of saying "X and Y are equivalent", we could say "there is an equivalence between X and Y". (We do the same for identifications.) That would avoid talking about propositional truncation here.

[bidundas]

That would work and treating them in the same fashion seems ideologically sound.

Bjorn

On 6 Aug 2021, at 16:39, Daniel R. Grayson @.***> wrote:

Instead of saying "X and Y are equivalent", we could say "there is an equivalence between X and Y". (We do the same for identifications.) That would avoid talking about propositional truncation here.

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

[UlrikBuchholtz]

I agree!

[DanGrayson]

Okay, I've eliminated several uses of the word "equivalent", and reworded its introduction. (I didn't have the energy to remove them all.)