Theorems · Definition · category theory

CategoryTheory.Cat.FreeReflRel.recOn

{V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {X : CategoryTheory.Paths V} →
      {motive : (Y : CategoryTheory.Paths V) → (f g : X ⟶ Y) → CategoryTheory.Cat.FreeReflRel V X Y f g → Sort u} →
        {Y : CategoryTheory.Paths V} →
          {f g : X ⟶ Y} →
            (t : CategoryTheory.Cat.FreeReflRel V X Y f g) →
              motive X (CategoryTheory.ReflQuiver.id X).toPath Quiver.Path.nil ⋯ → motive Y f g t

Defined in: Mathlib.CategoryTheory.Category.ReflQuiv
Cited by: 0 results in Mathlib
Foundations: Depth 16 from the axioms · uses propext
Assumes: CategoryTheory.ReflQuiver

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Pathsstatement and proof · cited by 82
CategoryTheory.ReflQuiverstatement and proof · cited by 64
Quiver.Hom.toPathstatement and proof · cited by 38
CategoryTheory.ReflQuiver.idstatement and proof · cited by 18
CategoryTheory.Cat.FreeReflRelstatement and proof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.