Theorems · Theorem · category theory

CategoryTheory.dite_comp

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

Defined in

Mathlib.CategoryTheory.Category.Basic

Cited by

11 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

CategoryTheory.CategoryDecidable