Theorems · Theorem · category theory

CategoryTheory.comp_dite

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : X ⟶ Y)
  (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)),
  CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) =
    if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)

Defined in

Mathlib.CategoryTheory.Category.Basic

Cited by

14 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

CategoryTheory.CategoryDecidable