Theorems · Definition · category theory

PFunctor.M.IsPath.casesOn

∀ {F : PFunctor.{uA, uB}} {motive : (a : PFunctor.Approx.Path F) → (a_1 : F.M) → PFunctor.M.IsPath a a_1 → Prop}
  {a : PFunctor.Approx.Path F} {a_1 : F.M} (t : PFunctor.M.IsPath a a_1),
  (∀ (x : F.M), motive [] x ⋯) →
    (∀ (xs : PFunctor.Approx.Path F) {a : F.A} (x : F.M) (f : F.B a → F.M) (i : F.B a) (a_2 : x = PFunctor.M.mk ⟨a, f⟩)
        (a_3 : PFunctor.M.IsPath xs (f i)), motive (⟨a, i⟩ :: xs) x ⋯) →
      motive a a_1 t

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms