Theorems · Theorem · category theory

MvPFunctor.M.Path.root.inj

∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} {h : x.dest = ⟨a, f⟩}
  {i : Fin2 n} {c : P.drop.B a i} {a_1 : P.A} {f_1 : P.last.B a_1 → P.last.M} {h_1 : x.dest = ⟨a_1, f_1⟩}
  {c_1 : P.drop.B a_1 i},
  MvPFunctor.M.Path.root x a f h i c = MvPFunctor.M.Path.root x a_1 f_1 h_1 i c_1 → a = a_1 ∧ f ≍ f_1 ∧ c ≍ c_1

Defined in

Mathlib.Data.PFunctor.Multivariate.M

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound