Theorems · Definition · category theory

Quiver.FreeGroupoid.redStep.casesOn

∀ {V : Type u} [inst : Quiver V]
  {motive :
    ⦃X Y : CategoryTheory.Paths (Quiver.Symmetrify V)⦄ → (a a_1 : X ⟶ Y) → Quiver.FreeGroupoid.redStep a a_1 → Prop}
  ⦃X Y : CategoryTheory.Paths (Quiver.Symmetrify V)⦄ {a a_1 : X ⟶ Y} (t : Quiver.FreeGroupoid.redStep a a_1),
  (∀ (X Z : Quiver.Symmetrify V) (f : X ⟶ Z),
      motive (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of (Quiver.Symmetrify V)).obj X))
        (CategoryTheory.CategoryStruct.comp f.toPath (Quiver.reverse f).toPath) ⋯) →
    motive a a_1 t

Defined in

Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Cited by

1 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

Quiver