Commit 2025-11-07 17:06 707df076
View on Github →feat(Data/PFunctor): make M.corec' universe generic (#30400)
Previously corec' required the generating type reside in the same universe as the constructed object.
This change corrects this by separating the universes.
As corec takes the parameter (g : β → P (α ::: β)), (where α is a TypeVec.{u} and β is a Type u) it is forced into the same universe by how the TypeVec construction works. This means corec cant be generalised by this construction.