I'm gonna have a bunch of time to work on math stuff for the next few weeks. Is there something I can focus on that would be useful to other folks? I'm thinking about

- is there something regarding hierarchy builder where I could contribute?
- I have this coquelicot proof of holomorphic implies analytic I never fully ported. The big pieces of it were: contour integration, compact convergence, homotopies, and geometric series. Perhaps paths and homotopies is a good thing to do?
- Integration in general vector spaces is pretty important. The "Bochner" and "Pettis" integrals will let us extend Lebesgue integrals without too much extra machinery.

@Zachary Stone either of your two last items look very useful! I'm not sure if someone else is working on it (CC @Marie Kerjean @Reynald Affeldt ) but I'm not.

I guess I'll work on the homotopy stuff then. The integration stuff relies on dual spaces, which relies on sensible vector subspaces. That seems likely to change with HB improvements. If there are any existing materials on paths/homotopies I should know about, I'd be happy to see them. Otherwise I'll just start with some HB mixins for paths and loops and see how far I get.

I don't plan to work on any of your two items (I would love to see more of holomorphic functions ported though). As soon as the port to HB is successful I would love to start working on duality theory and topological vector spaces. Also, @Cyril Cohen if I can be of any help on HB let me know (it happened while I was away, and as far as I can see there only remains technicalities on which I'm not sure I can help).

I've posted a first pass of HB structures for paths. A long way to go to define winding numbers, but it's a start.

So I have a crazy idea, but I'm not sure how to do it.

I suspect there's an elegant approach to define path homotopies on X as paths in the "PathSpace" of X. That is, the set of paths on X, equipped with the uniform topology. If we can get this right, then

- Chaining homotopies is a trivial application of chaining paths.
- Same with reversing paths, constant homotopies, etc
- Path-connectedness partitions a topological space -> homotopies are an equivalence relation
- We'll be better positioned to work with general homotopies from A -> B as paths in
`{family compact, A -> B}`

.

probably some other major conveniences.

I can figure out the proofs, but I am not sure about some of the other issues.

- A generalization issue: How much do we care that
`X : topologialType`

rather than`X : uniformType`

? We already have the uniform topology stuff done for for`uniformType`

. Otherwise we'll need to define the`compact-open`

topology and prove stuff stuff about it. - How should I equip
`Path.type`

and`Loop.type`

with a topology? Is it better to treat these as subspaces of`{uniform, [0,1] -> T}`

or use the weak topology construction directly? - Is this gonna be one of those things where waiting for
`Topology`

and`Uniform`

to enter HB will be easier? There's plenty to prove about paths in the meanwhile, so I'm definitely not blocked.

Last updated: Feb 05 2023 at 13:02 UTC