The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is it possible to define multiple notations using the same record field with [where]?  That is, can I do something like

  Local Reserved Notation "A ⊗ B" (at level 40, left associativity).

  Local Reserved Notation "A ⊗m B" (at level 40, left associativity).

  Let src (C : SpecializedCategory morC) s d (_ : Morphism C s d) := s.

  Let dst (C : SpecializedCategory morC) s d (_ : Morphism C s d) := d.

  Record MonoidalCategory := {

    UnderlyingCategory :> SpecializedCategory morC;

    TensorProduct : SpecializedFunctor (UnderlyingCategory * UnderlyingCategory) UnderlyingCategory where "A ⊗ B" := (TensorProduct (A, B));

    TensorProduct' := TensorProduct

      where "A ⊗m B" := (TensorProduct.(MorphismOf) (s := (src A, src B)) (d := (dst A, dst B)) (A, B));

  }.

but without defining [TensorProduct']?

Thanks.

-Jason