Notation clash for `≌`

Stream: mathlib4

[Calle Sönne]

I have a problem where the notation ≌ has two possible interpretations, either equivalence of categories or equivalence in terms of some (other) bicategory structure. Is there a way I can give preference to the latter? Maybe at the top of the file? The notation for equivalence in terms bicategories is defined using scoped infixr, could this be helpful?

Here is my specific situation:
I have defined the bicategory FiberCat S of fibered categories over a base S. This lets me use the notation ≌ to denote equivalence in the sense of the bicategory structure. An object C : FiberCat S consists of a category C.carrier : Type _ and a functor C.carrier ⥤ S. Now, I have also equipped the type FiberCat S with a CoeToSort instance sending C : FiberCat S to C.carrier : Type _. Because of this (I think) ≌ can also denote an equivalence of underlying categories C.carrier. I would like to give preference for ≌ to denote equivalence in the sense of the bicategory structure, is this possible? Or will I have to remove the CoeToSort instance?

[Eric Wieser]

Does using (priority := high) work?

[Eric Wieser]

(or is it prio := ?)

[Adam Topaz]

I would get rid of that coercion

[Adam Topaz]

I feel like it’s likely to cause other similar issues elsewhere.

[Calle Sönne]

Eric Wieser said:

Does using (priority := high) work?

You mean next to the bicategory instance?

[Calle Sönne]

Calle Sönne said:

Eric Wieser said:

Does using (priority := high) work?

You mean next to the bicategory instance?

Okay I figured out where to put it in the scoped infixr expression, and it works :)

[Calle Sönne]

(deleted)

[Eric Wieser]

Yes, I meant on the notation

[Calle Sönne]

Adam Topaz said:

I feel like it’s likely to cause other similar issues elsewhere.

After the next issue I run into, I will delete it ;)

[Adam Topaz]

If X Y : C, what does X \hom Y mean?

[Calle Sönne]

Adam Topaz said:

If X Y : C, what does X \hom Y mean?

hom within the category C

[Adam Topaz]

Isn't C also a bicategory?

[Calle Sönne]

Adam Topaz said:

Isn't C also a bicategory?

Oh I meant that FiberedCat S is a bicategory. So the bicategory of fibered categories.

[Adam Topaz]

Oh so I'm confused why using \backcong causes issues...

[Calle Sönne]

Adam Topaz said:

Oh so I'm confused why using \backcong causes issues...

I think its because if I have C D : FiberedCat S, then C \backcong D could either mean C.carrier \backcong D.carrier or C \backcong D, meaning an equivalence in the bicategory structure on FiberedCat S. (Or maybe you are not confused about this part)

[Adam Topaz]

Aha I see now.

[Adam Topaz]

I still think that the coercion is problematic because there's more notation that's shared between the category theory library and stuff internal to a bicategory (I think whiskering is another example). If writing C.carrier is too much I would suggest renaming it C.cat or something like that.

[Calle Sönne]

Adam Topaz said:

I still think that the coercion is problematic because there's more notation that's shared between the category theory library and stuff internal to a bicategory (I think whiskering is another example). If writing C.carrier is too much I would suggest renaming it C.cat or something like that.

Yeah I think you are right, I was more just curious about the next time it would break. And C.cat is a good suggestion, way less painful than C.carrier!