universe level in SimplyConnectedSpace.ofConnected

Stream: mathlib4

[Matthew Ballard]

Am I correct in believing we did not intend for Y from docs#SimplyConnectedSpace.ofContractible to live in Type?

[Matthew Ballard]

I mentioned this in the porting meeting but I think it useful to record. The issue here is that Bundle.of forces partial monomorphization of the universe levels as docs#Bundled.of only accepts arguments from the same u.

In multiple situations, we pass from types to a category back to types and then to the category many times. Each pass with Bundled.of creates new universe constraints that Lean needs to solve. #6370 shows that universe behavior can significantly influence performance. Is this contributing to some of the worst slowdowns we are seeing?