Merge generators with non-generator cells

[wilfofford]

Currently, homotopy.io has the feature to merge two generator cells if they have the same source and target. Theoretically, if I have a generator G and I manage to construct in the workspace a non-generator cell C with the same boundary as G, it should be possible to replace G with C in all other cells of the signature, at least up to homotopy. If G is not contained in the support of C, this process should also delete G from the signature. Replacement may only be possible "up to homotopy" because it could be the case that at some other place in the signature, G appears on a singular level with another cell D, and then if C is some nontrivial composite, you would have to make some arbitrary choice about what level D lies on with respect to the morphisms comprising C.

You can already approximate this feature by saving C as a theorem, and then merging the theorem generator with G. However, if you ever then want to construct homotopies that utilise the particular features of C, you have to insert bubbles everywhere which is a hassle.

This is related to defining functors from one signature S to another S'. Defining such a functor amounts to loading S and S' in the same workspace, then merging generators of S with cells constructed from S', until all generators of S are cleared. For instance, this would allow you to prove things like the fact that adjunctions induce monads, in a "backwards reasoning" style akin to that of Coq: load the signatures for a monad and an adjunction into the same workshop, then the monad generators are your "proof obligations", which you clear by merging them with cells constructed from the adjunction signature. Using the existing theorem feature it is already possible to prove such facts, but this forces you to reason in a "forwards" style, where you have to keep track of proof obligations yourself.

A special case of this is currently implemented, namely suspension at a 0-cell A: this shifts the other cells up one dimension, while replacing all occurrences of A with $\text{id} (A)$. The same effect could be achieved by suspending the whole diagram, merging the two new basepoints into a single point $\star$, and then merging A with $\text{id}(\star)$. The general case may be more problematic to implement, though.

I think this would probably be a hard feature to implement, as it requires changing the shape of cells rather than just relabelling them, but has anyone thought about doing something like this?

[jamievicary]

Hi Wilf this is an interesting idea. Due to this being "up to homotopy" I think there would be no direct way to implement it at the moment. I agree it could have some nice advantages, so worth continuing to think about!