Commit 2026-06-23 10:53 2a63917e

feat(Topology): generalise Trivialization.symm (#40903) Change Bundle.Trivialisation.symm to get its junk values via Classical.arbitrary from a Nonempty instance, instead of requiring using 0 as the junk value and requiring Zero instances for that. This in particular allows us to generalise FiberBundle.pullback to bundles with nonempty fibres, which previously also required the bundle fibres to have zeroes. This is motivated by future work on principal bundles, whose fibres are always nonempty but have no preferred elements and hence no instances like Zero or Inhabited. Bundle.Trivialisation.symmₗ and Bundle.Trivialisation.symmL use 0 as the junk value as before; so while their definition got slightly more complicated and their underlying function no longer definitionally equal to .symm, all statements that were true about them previously continue to be true now. In particular, I've tested this PR against the sphere eversion project and ran into minimal breakage there.