Theorems · Definition · category theory

CategoryTheory.Functor.Braided.noConfusionType

Sort u →
  {C : Type u₁} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.BraidedCategory C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.BraidedCategory D] →
                  {F : CategoryTheory.Functor C D} →
                    F.Braided →
                      {C' : Type u₁} →
                        [inst' : CategoryTheory.Category.{v₁, u₁} C'] →
                          [inst'_1 : CategoryTheory.MonoidalCategory C'] →
                            [inst'_2 : CategoryTheory.BraidedCategory C'] →
                              {D' : Type u₂} →
                                [inst'_3 : CategoryTheory.Category.{v₂, u₂} D'] →
                                  [inst'_4 : CategoryTheory.MonoidalCategory D'] →
                                    [inst'_5 : CategoryTheory.BraidedCategory D'] →
                                      {F' : CategoryTheory.Functor C' D'} → F'.Braided → Sort u

Defined in

Mathlib.CategoryTheory.Monoidal.Braided.Basic

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategory