@ncf after you prove the third monoidal product coincides with the first two, the associators and unitors etc are actually left over unused and uneliminated (unlike the situation in eg. half adjoint equivalences where you can add two levels of data which bundles up into a contractible type and disappears), so in the final form you just get an invertible element in that monoid
=> More informations about this toot | View the thread | More toots from trebor@types.pl
text/geminiThis content has been proxied by September (3851b).