Cateno
Cateno copied to clipboard
What should ev(I), id(I), etc do?
If we use uniformscaling, we don't know the type, need uniformsclaing morphism id(I) that these can be equal to. If we choose correctly, transpose will work as used with the id(I) and coev(I) even when applied to f:I->A. Will require special casing otimes of MWords to look for id(I). Stopgap is to special case transpose.
Strict fts should collapse them Lax fts should leave in Otherwise the meaning of id(I) should be delegated to the quantitative category. I is mapped to the munit of Q. Then id(munit(Q)) is called. Usually it is multiplication by one, or empty box, etc. No uniform scaling unless Q uses it as the monoidal unit.
Careful about rewriting border: should composing with idA or idI be automatically collapsed? Prob not