Combine signatures

[calintat]

In the "Signature" panel, we should be able to insert the signature of a different workspace to our current signature. This is different from the import functionality which replaces the current project so it doesn't let you combine signatures.

This way, we could easily add structures such as monoids to the signature.

[calintat]

Maybe place the inserted signature in a folder.

[regular-citizen]

Do we have some UI in mind for how to do this without creating a "checkbox hell"? I really like the idea of "import workspace inside a new folder", but I still can't picture a non-clunky UI.

[jamievicary]

Drag the .hom file onto the directory icon?

On Mon, 5 Sept 2022, 09:17 Chiara Sarti, @.***> wrote:

Do we have some UI in mind for how to do this without creating a "checkbox hell"? I really like the idea of "import workspace inside a new folder", but I still can't picture a non-clunky UI.

— Reply to this email directly, view it on GitHub https://github.com/homotopy-io/homotopy-rs/issues/523#issuecomment-1236681982, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACQ4OHS2IYTN2S3ODRXXY4DV4WUC3ANCNFSM5ZIEOVWQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[regular-citizen]

I like this idea. Though if we do it for folders we should also support it for old-school "replace workspace" imports.

[mlharaujo]

It would be nice if you could also choose how to attach the new cells. For example, you might want to add a monoid structure to an already existing cell (or even to a diagram).

[jamievicary]

The way to do this would be by first importing the external signature by disjoint union, then identifying generators with the same boundary.

[doctorn]

This is a restricted push-out of computads right?

[jamievicary]

Hi Nathan yes definitely that would be the expectation.

[mlharaujo]

What do you mean by "restricted"?

[doctorn]

Restricted in the sense that extending a signature like this will only provide you with a subclass of all push-outs of computads (my hunch is that not all of them will be constructible without assuming the existence of inverses and postulating some coherence data — something we can only do on the labelled branch).

[jamievicary]

This is something we do not yet give a full mathematical treatment of, however it is clear that identifying two variables with identical boundaries is a very simple sort of pushout, which can be computed more straightforwardly than other richer sorts of pushouts one might consider.