Commit 2025-06-08 17:42 1150bf56

View on Github →

feat(Data/PFunctor/Univariate): Generalize universe level in PFunctor (#24257) This PR generalizes PFunctor to have potentially different universe levels for its A and B fields. This is to aid with my formalization attempt (with @dtumad ) of poly functors here (in order to model interactive systems in general, and cryptographic protocols in particular). There is no plan yet to need MvPFunctor, so I do not generalize universe levels of that for now.

Estimated changes

modified def PFunctor.Idx
modified def PFunctor.Obj
modified def PFunctor.W
modified def PFunctor.comp.get
modified def PFunctor.comp.mk
modified def PFunctor.comp
modified inductive PFunctor.Approx.CofixA
modified def PFunctor.Approx.Path
modified def PFunctor.M.corec'