More equivalence notations?

[JasonGross]

Should we make more notations for equivalences, like + for equiv_functor_sum' and * for equiv_functor_prod' and -> for equiv_functor_arrow', etc?

[spitters]

I am inclined to say yes.

On Tue, Feb 3, 2015 at 2:36 AM, Jason Gross [email protected] wrote:

Should we make more notations for equivalences, like + for equiv_functor_sum' and * for equiv_functor_prod' and -> for equiv_functor_arrow', etc?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/707.

[JasonGross]

Are there good notations for equiv_functor_forall' f (fun x => g) and equiv_functor_sigma' f (fun x => g)? (The issue being that the normal notations have a binder, but here, we need to specify two things, and neither is the type of the binder.)

[JasonGross]

I guess we could do something like f =(x)=> g and f =>{ x | g } or something...

[JasonGross]

Should <~> be equiv_functor_equiv, or would that be too confusing?

[mikeshulman]

+ and * might be okay, but I need to think it over. (One could also propose them in function_scope for simple functor_sum and functor_prod.) I think I would be against overloading -> and <~>, though.

[mikeshulman]

Oh, except that there is no function_scope, right. d-:

[JasonGross]

I've done +, *, and -> in #708. I can remove them, though. Note that I've overloaded + and * for functors (here and here) and categories.

[JasonGross]

There is function_scope, you just have to bind it manually.

[mikeshulman]

Meaning with Arguments?

[JasonGross]

Yes.

[mikeshulman]

Any other opinions? E.g. @peterlefanulumsdaine, @andrejbauer ?

[andrejbauer]

If we do lots of notations, how much are we raising teh bar?

[mikeshulman]

Some, certainly. I think -> for equiv_functor_arrow is raising the bar too much (too much for me, at least). But + and * are fairly commonly used in (at least certain parts of) mathematics for the action of those functors on morphisms as well as on objects. On the other hand, if we don't have notations for all the equiv_functor_... operations, then the inconsistency of having notations for some of them might be more confusing than it is worth, especially since equiv_functor_sum and equiv_functor_prod seem to be rather less commonly used than (say) equiv_functor_sigma and equiv_functor_forall.

[Alizter]

I think having such notations, especially non-standard compared to the literature, makes things unnecessarily obfuscated. I don't think we should expect readers to recall what exactly each little notation means when equiv_functor_forall perfectly describes the situation. I am therefore inclined to close this issue.