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