Theorems · Definition · category theory

CategoryTheory.PositiveCategory.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {P : Sort u_1} →
        {toMarkovCategory : CategoryTheory.MarkovCategory C} →
          {copy_comp_natural :
              ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
                [h : CategoryTheory.Deterministic (CategoryTheory.CategoryStruct.comp f g)],
                CategoryTheory.CategoryStruct.comp f
                    (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id Y))) =
                  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) f)} →
            {toMarkovCategory' : CategoryTheory.MarkovCategory C} →
              {copy_comp_natural' :
                  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
                    [h : CategoryTheory.Deterministic (CategoryTheory.CategoryStruct.comp f g)],
                    CategoryTheory.CategoryStruct.comp f
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id Y))) =
                      CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) f)} →
                { toMarkovCategory := toMarkovCategory, copy_comp_natural := copy_comp_natural } =
                    { toMarkovCategory := toMarkovCategory', copy_comp_natural := copy_comp_natural' } →
                  (toMarkovCategory ≍ toMarkovCategory' → P) → P

Defined in

Mathlib.CategoryTheory.MarkovCategory.Positive

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms