Theorems · Definition · category theory

MvPFunctor.M.pathDestRight

{n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {x : P.last.M} →
        {a : P.A} →
          {f : P.last.B a → P.last.M} →
            x.dest = ⟨a, f⟩ →
              TypeVec.Arrow (MvPFunctor.M.Path P x) α → (j : P.last.B a) → TypeVec.Arrow (MvPFunctor.M.Path P (f j)) α

Implementation of destructor for M-type of P

Defined in

Mathlib.Data.PFunctor.Multivariate.M

Cited by

3 results in Mathlib

Foundations

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