Commit 2026-03-22 10:55 d482465e

View on Github →

feat(Data/PFunctor): Universe generic W (#36069) Previously W.ind was limited to Prop. It can for free be changed to Sort w forall w.

Estimated changes

added def MvPFunctor.wInd
added theorem MvPFunctor.wInd_wMk
modified def MvPFunctor.wRec
modified theorem MvPFunctor.wRec_eq
deleted theorem MvPFunctor.w_cases
deleted theorem MvPFunctor.w_ind
added def MvPFunctor.wpInd
modified def MvPFunctor.wpRec
modified theorem MvPFunctor.wpRec_eq
deleted theorem MvPFunctor.wp_ind