Transport a symmetric monoidal structure along an equivalence of categories

@[implicit_reducible]

instance CategoryTheory.Monoidal.Transported.instBraidedCategory {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : BraidedCategory (Transported e)

@[implicit_reducible]

instance CategoryTheory.Monoidal.instBraidedTransportedInverseEquivalenceTransported {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : (equivalenceTransported e).inverse.Braided

@[implicit_reducible]

noncomputable def CategoryTheory.Monoidal.transportedFunctorCompInverseLaxBraided {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : ((equivalenceTransported e).functor.comp (equivalenceTransported e).inverse).LaxBraided

This is a def because once we have that both (e' e).inverse and (e' e).functor are braided, this causes a diamond.

@[implicit_reducible]

noncomputable def CategoryTheory.Monoidal.transportedFunctorCompInverseBraided {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : ((equivalenceTransported e).functor.comp (equivalenceTransported e).inverse).Braided

This is a def because once we have that both (e' e).inverse and (e' e).functor are braided, this causes a diamond.

@[implicit_reducible]

noncomputable instance CategoryTheory.Monoidal.instBraidedTransportedFunctorEquivalenceTransported {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : (equivalenceTransported e).functor.Braided

@[implicit_reducible]

instance CategoryTheory.Monoidal.Transported.instSymmetricCategory {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [SymmetricCategory C] : SymmetricCategory (Transported e)