@John this topic is very cool !! I interpret it as a great opportunity to learn a bit about your way to conduct scientific activity.. , at #56 / 3) the "lax " of "symmetric monoidal" is simply not related to the ["Lax" (a name ) pairs], isn't it?