search

homotopy-io / homotopy-rs

A Rust/WASM implementation of homotopy.io
https://homotopy.io
BSD 3-Clause "New" or "Revised" License
84 stars 7 forks source link

Add structure to a generator #524

Open calintat opened 2 years ago

calintat commented 2 years ago

Not sure how this generalises, but it would be nice if you could click on a generator and say make it a monoid.

With #522 and #523, you could do this by inserting your monoid signature and then merging your original generator and the new generator, but it would be nice if we could do this automatically. Maybe it would only work for signatures with a single 0-generator.

calintat commented 2 years ago

Also what if I wanted to make a 1-cell f into a monoid but my monoid signature is defined on a 0-cell x. We should be able to lift the monoid signature one dimension higher by literally replacing x with f.

calintat commented 2 years ago

We could also have a feature inside homotopy.io where you can view a library of structures that we have formalised and add them to your signature or a generator with one click.

NickHu commented 2 years ago

I have wanted this feature for years, but I thought it was predicated on a greater understanding of what it means to have a functor on signatures. I've forgotten why I thought this though, so it might not be relevant.

calintat commented 2 years ago

I don't see how this is related to functors. This is about adding stuff to the signature.

NickHu commented 2 years ago

Because 'equipping a 1-cell $f$ with the structure of a monoid' is like having a functor (in an appropriate sense) which sends $f$ to the carrier of a monoid object in some category freely generated by a different signature. I don't know if it has to be thought of this way; I remember talking to @alexarice about this, maybe he can add?

calintat commented 2 years ago

I don't really see that. You can't send a 1-cell $f$ to the carrier of a monoid object which is 0D.