pub fn th_sym_monoidal_category() -> ModalDblTheory
The theory of strict symmetric monoidal categories.