[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
src✝ : Mon_ C := Mon_.trivial C
⊢ (β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
      (Mon_.mk src✝.X src✝.one src✝.mul).mul =
    (Mon_.mk src✝.X src✝.one src✝.mul).mul
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
src✝ : Mon_ C := Mon_.trivial C
⊢ (β_ (𝟙_ C) (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom = (λ_ (𝟙_ C)).hom
[PROOFSTEP]
rw [braiding_leftUnitor, unitors_equal]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
⊢ (β_ (Mon_.mk src✝.X src✝.one src✝.mul).X (Mon_.mk src✝.X src✝.one src✝.mul).X).hom ≫
      (Mon_.mk src✝.X src✝.one src✝.mul).mul =
    (Mon_.mk src✝.X src✝.one src✝.mul).mul
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
⊢ (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul =
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul
[PROOFSTEP]
have := F.braided
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
⊢ (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul =
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul
[PROOFSTEP]
slice_lhs 1 2 => rw [← this]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map A.mul
[PROOFSTEP]
rw [← this]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map A.mul
[PROOFSTEP]
rw [← this]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| (β_ (F.obj A.X) (F.obj A.X)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map A.mul
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map (β_ A.X A.X).hom) ≫ F.map A.mul =
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X ≫ F.map A.mul
[PROOFSTEP]
slice_lhs 2 3 => rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map (β_ A.X A.X).hom ≫ F.map A.mul
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
[PROOFSTEP]
rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map (β_ A.X A.X).hom ≫ F.map A.mul
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
[PROOFSTEP]
rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| F.map (β_ A.X A.X).hom ≫ F.map A.mul
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : LaxBraidedFunctor C D
A : CommMon_ C
src✝ : Mon_ D := (LaxMonoidalFunctor.mapMon F.toLaxMonoidalFunctor).obj A.toMon_
this :
  ∀ (X Y : C),
    LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y ≫ F.map (β_ X Y).hom =
      (β_ (F.obj X) (F.obj Y)).hom ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X
| LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X
[PROOFSTEP]
rw [← CategoryTheory.Functor.map_comp, A.mul_comm]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
X✝ Y✝ : LaxBraidedFunctor C D
α : X✝ ⟶ Y✝
⊢ ∀ ⦃X Y : CommMon_ C⦄ (f : X ⟶ Y),
    (mapCommMon X✝).map f ≫ (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) Y =
      (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) X ≫ (mapCommMon Y✝).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
X✝¹ Y✝¹ : LaxBraidedFunctor C D
α : X✝¹ ⟶ Y✝¹
X✝ Y✝ : CommMon_ C
f✝ : X✝ ⟶ Y✝
⊢ (mapCommMon X✝¹).map f✝ ≫ (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) Y✝ =
    (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) X✝ ≫ (mapCommMon Y✝¹).map f✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
X✝¹ Y✝¹ : LaxBraidedFunctor C D
α : X✝¹ ⟶ Y✝¹
X✝ Y✝ : CommMon_ C
f✝ : X✝ ⟶ Y✝
⊢ ((mapCommMon X✝¹).map f✝ ≫ (fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) Y✝).hom =
    ((fun A => Mon_.Hom.mk (NatTrans.app α.toNatTrans A.X)) X✝ ≫ (mapCommMon Y✝¹).map f✝).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommMon_ C
f : X✝ ⟶ Y✝
x✝² x✝¹ : Discrete PUnit
x✝ : x✝² ⟶ x✝¹
⊢ ((fun A =>
              LaxBraidedFunctor.mk
                (LaxMonoidalFunctor.mk
                  (CategoryTheory.Functor.mk { obj := fun x => A.X, map := fun {X Y} x => 𝟙 ((fun x => A.X) X) }) A.one
                  fun x x => A.mul))
            X✝).map
        x✝ ≫
      (fun x => f.hom) x✝¹ =
    (fun x => f.hom) x✝² ≫
      ((fun A =>
              LaxBraidedFunctor.mk
                (LaxMonoidalFunctor.mk
                  (CategoryTheory.Functor.mk { obj := fun x => A.X, map := fun {X Y} x => 𝟙 ((fun x => A.X) X) }) A.one
                  fun x x => A.mul))
            Y✝).map
        x✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommMon_ C
f : X✝ ⟶ Y✝
x✝² x✝¹ : Discrete PUnit
x✝ : x✝² ⟶ x✝¹
⊢ 𝟙 X✝.X ≫ f.hom = f.hom ≫ 𝟙 Y✝.X
[PROOFSTEP]
rw [Category.id_comp, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
x✝ : Discrete PUnit
⊢ x✝ = (trivial (Discrete PUnit)).toMon_.X
[PROOFSTEP]
ext
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
⊢ ∀ {X Y : Discrete PUnit} (f : X ⟶ Y),
    ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).map f ≫
        ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) Y).hom =
      ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) X).hom ≫
        ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).map f
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ f
[GOAL]
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
as✝¹ as✝ : PUnit
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).map f ≫
      ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) { as := as✝ }).hom =
    ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) { as := as✝¹ }).hom ≫
      ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
⊢ ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).ε ≫
      ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) (𝟙_ (Discrete PUnit))).hom =
    ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).ε
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
F : LaxBraidedFunctor (Discrete PUnit) C
⊢ ∀ (X Y : Discrete PUnit),
    LaxMonoidalFunctor.μ ((𝟭 (LaxBraidedFunctor (Discrete PUnit) C)).obj F).toLaxMonoidalFunctor X Y ≫
        ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) (X ⊗ Y)).hom =
      (((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) X).hom ⊗
          ((fun x => F.mapIso (eqToIso (_ : x = (trivial (Discrete PUnit)).toMon_.X))) Y).hom) ≫
        LaxMonoidalFunctor.μ ((laxBraidedToCommMon C ⋙ commMonToLaxBraided C).obj F).toLaxMonoidalFunctor X Y
[PROOFSTEP]
aesop_cat
