Theorems · Definition · category theory

CategoryTheory.PositiveCategory.recOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {motive : CategoryTheory.PositiveCategory C → Sort u_1} →
        (t : CategoryTheory.PositiveCategory C) →
          ([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)) →
                motive { toMarkovCategory := toMarkovCategory, copy_comp_natural := copy_comp_natural }) →
            motive t

Defined in

Mathlib.CategoryTheory.MarkovCategory.Positive

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory