ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<VAR>f g : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y Z<VAR>w₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst<VAR>w₂ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>𝟙_ C = ⊤_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.tensorObj X Y = (X ⨯ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.Limits.prod.map f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X f = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight f Z = CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X) (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.terminal.from X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>X Y : C<GOAL>β_ X Y = CategoryTheory.Limits.prod.braiding X Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.tensorObj X Y = (X ⨿ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.Limits.coprod.map f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X f = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight f Z = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to X) (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.initial.to X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv = CategoryTheory.Limits.coprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>P Q : C<GOAL>β_ P Q = CategoryTheory.Limits.coprod.braiding P Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasTerminal D<VAR>CategoryTheory.Limits.HasBinaryProducts D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>X Y : C<GOAL>F.toMonoidalFunctorOfHasFiniteProducts.μ X Y = (CategoryTheory.asIso (CategoryTheory.Limits.prodComparison F X Y)).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasTerminal D<VAR>CategoryTheory.Limits.HasBinaryProducts D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<GOAL>F.toMonoidalFunctorOfHasFiniteProducts.toFunctor = F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasTerminal D<VAR>CategoryTheory.Limits.HasBinaryProducts D<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<GOAL>F.toMonoidalFunctorOfHasFiniteProducts.ε = (CategoryTheory.asIso (CategoryTheory.Limits.terminalComparison F)).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X X' Y Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f g) (CategoryTheory.Limits.BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ g f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z)).isLimit (ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z) X).isLimit).hom (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y X Z).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y) Z).isLimit (ℬ Z (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y)).isLimit).hom (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.BinaryFan.braiding (ℬ Y Z).isLimit (ℬ Z Y).isLimit).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Z Y).inv (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom (CategoryTheory.CategoryStruct.id Y)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (CategoryTheory.Limits.BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>A : Comon_ C<GOAL>A.counit = CategoryTheory.Limits.terminal.from A.X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>A : Comon_ C<GOAL>A.comul = CategoryTheory.Limits.diag A.X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>A : Comon_ C<GOAL>(iso_cartesianComon_ A).inv.hom = 𝟙 ((cartesianComon_ C).obj A.X).X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>A : Comon_ C<GOAL>(iso_cartesianComon_ A).hom.hom = 𝟙 A.X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>comonEquiv.functor = Comon_.forget C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>comonEquiv.inverse = cartesianComon_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>comonEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun A => iso_cartesianComon_ A) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>comonEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl ((cartesianComon_ C ⋙ Comon_.forget C).obj X)) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>self : CommMon_ C<GOAL>(β_ self.X self.X).hom ≫ self.mul = self.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.trivial C).X = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.trivial C).one = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(CommMon_.trivial C).mul = (λ_ (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>(𝟙 A).hom = 𝟙 A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>R S T : CommMon_ C<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>(f ≫ g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A B : CommMon_ C<VAR>f g : A ⟶ B<VAR>h : f.hom = g.hom<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>𝟙 A = 𝟙 A.toMon_
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A₁ A₂ A₃ : CommMon_ C<VAR>f : A₁ ⟶ A₂<VAR>g : A₂ ⟶ A₃<GOAL>f ≫ g = f ≫ g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>((CommMon_.forget₂Mon_ C).obj A).one = A.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>((CommMon_.forget₂Mon_ C).obj A).mul = A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A B : CommMon_ C<VAR>f : A ⟶ B<GOAL>((CommMon_.forget₂Mon_ C).map f).hom = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>A : CommMon_ C<GOAL>(F.mapCommMon.obj A).X = F.obj A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : CategoryTheory.LaxBraidedFunctor C D<GOAL>∀ {X Y : CommMon_ C} (f : X ⟶ Y), (F.mapCommMon.map f).hom = F.map f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>A : CommMon_ C<GOAL>(F.mapCommMon.obj A).mul = F.μ A.X A.X ≫ F.map A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : CategoryTheory.LaxBraidedFunctor C D<VAR>A : CommMon_ C<GOAL>(F.mapCommMon.obj A).one = F.ε ≫ F.map A.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>∀ {X Y : CategoryTheory.LaxBraidedFunctor C D} (α : X ⟶ Y) (A : CommMon_ C), (((CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor C D).map α).app A).hom = α.app A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : CategoryTheory.LaxBraidedFunctor C D<GOAL>(CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor C D).obj F = F.mapCommMon
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>F : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C<GOAL>(CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).obj F = F.mapCommMon.obj (CommMon_.trivial (CategoryTheory.Discrete PUnit.{u + 1}))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C} (α : X ⟶ Y), (CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).map α = ((CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C).map α).app (CommMon_.trivial (CategoryTheory.Discrete PUnit.{u + 1}))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>∀ {X Y : CategoryTheory.Discrete PUnit.{u + 1}} (x : X ⟶ Y), ((CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).obj A).map x = 𝟙 ((fun x => A.X) X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>∀ (x : CategoryTheory.Discrete PUnit.{u + 1}), ((CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).obj A).obj x = A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>∀ (x x_1 : CategoryTheory.Discrete PUnit.{u + 1}), ((CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).obj A).μ x x_1 = A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : CommMon_ C<GOAL>((CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).obj A).ε = A.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : CommMon_ C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{u + 1}), ((CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).map f).app x = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C<GOAL>∀ (X_1 : CategoryTheory.Discrete PUnit.{u + 1}), ((CommMon_.EquivLaxBraidedFunctorPUnit.unitIso C).hom.app X).app X_1 = 𝟙 (X.obj X_1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C<GOAL>∀ (X_1 : CategoryTheory.Discrete PUnit.{u + 1}), ((CommMon_.EquivLaxBraidedFunctorPUnit.unitIso C).inv.app X).app X_1 = 𝟙 (X.obj (𝟙_ (CategoryTheory.Discrete PUnit.{u + 1})))