Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.FunctorialFactorizationData.mk.sizeOf_spec

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)]
  [inst_3 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)] (Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C)
  (i : CategoryTheory.Arrow.leftFunc ⟶ Z) (p : Z ⟶ CategoryTheory.Arrow.rightFunc)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = CategoryTheory.Arrow.leftToRight)
      CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac._autoParam)
  (hi : ∀ (f : CategoryTheory.Arrow C), W₁ (i.app f)) (hp : ∀ (f : CategoryTheory.Arrow C), W₂ (p.app f)),
  sizeOf { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } = 1 + sizeOf Z + sizeOf i + sizeOf p + sizeOf fac

Defined in

Mathlib.CategoryTheory.MorphismProperty.Factorization

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategorySizeOfSizeOfSizeOf