Transport Braided Category

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe v₁ w₁ v₂ w₂ u₁ u₂

namespace CategoryTheory

namespace BraidedCategory

variable (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D]
  [MonoidalCategory C] [BraidedCategory C] (e : C ≌ D)

instance : @BraidedCategory D _ (Monoidal.transport e) :=
  letI := Monoidal.transport e
  ⟨fun X Y ↦ e.functor.mapIso (β_ _ _),
    fun X Y Z f ↦ sorry, sorry, sorry, sorry⟩

#check Equivalence.functor

end BraidedCategory

end CategoryTheory

[Kenny Lau]

Do we have code for transporting a braided category (i.e. where the tensor product is commutative up to iso) over an equivalence?

[Dagur Asgeirsson]

#24490

[Dagur Asgeirsson]

It's ready for review now

[Kenny Lau]

@Dagur Asgeirsson i would love to review your PR, but I'm not very familiar with category theory; still, i left one comment asking if the things should be computable