issue #1097: transport a monoidal structure across an equ...

Stream: triage

[Random Issue Bot]

Today I chose issue 1097 for discussion!

transport a monoidal structure across an equivalence of categories
Created by @Scott Morrison (@semorrison) on 2019-05-30
Labels: feature-request, help wanted

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 1097 for discussion!

transport a monoidal structure across an equivalence of categories
Created by @Scott Morrison (@semorrison) on 2019-05-30
Labels: help wanted, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

[Scott Morrison]

This even gets used now, to "effortlessly" put the monoidal structure on Rep k G, via the fact this is equivalent to functors single_obj G ⥤ Module k, and functor categories inherit monoidal structures from their codomain. It even ends up having the right definitional properties, afaict.