Theorems/proofs and invertibility

[calintat]

How will theorems and proofs interact with invertibility?

I think the theorem cell should be non-invertible and the proof cell should be invertible.

I don't think you should be able to toggle these, so we should disable the UI for toggling invertibility (#589) for such generators.

[calintat]

Also should these generators be framed or oriented? Will that even matter?

[jamievicary]

I agree with this. The theorem cell should be framed invertible, because this is what corresponds to "ordinary" invertibility in higher category theory.

[calintat]

But it sounds like you don't agree. I said the theorem cell should be directed and the proof cell should be invertible. Are you saying the theorem cell should be invertible as well? Because I don't think that makes sense if for example you used a directed generator to prove the theorem.

[jamievicary]

No I'm agreeing with you, the theorem cell should be directed, the proof cell should be framed invertible.

On Mon, 18 Jul 2022, 18:37 Calin Tataru, @.***> wrote:

But it sounds like you don't agree. I said the theorem cell should be directed and the proof cell should be invertible. Are you saying the theorem cell should be invertible as well? Because I don't think that makes sense if for example you used a directed generator to prove the theorem.

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

[jamievicary]

This is high-priority low-hanging bug fruit.

[calintat]

Yes, this should be a priority.

It's easy to make sure the theorem cells are framed directed and proof cells are framed invertible by default (right now everything is framed directed by default, so we'd just need to do something different for proof cells).

We also don't want the user to change these, so we need to label theorem and proof cells as "special" and then disable the framed/oriented or directed/invertible toggles for special cells. Again not too hard, but involves some UI work.

My only concern is how do we handle generators migrated from homotopy-js. Right now a migrated theorem/proof cell is oriented directed by default. Do we want migrated proof cells to be oriented invertible instead? Also how do we stop users from taking a migrated theorem cell and making it invertible? There is no way to figure out if a migrated generator from homotopy-js was a theorem or proof cell as we never recorded that information before.

[jamievicary]

The last point does not concern me, see discussion in #795. Anyway we can discuss that in that other issue, for this issue can we please just make the "Proof" cells invertible.

[calintat]

I made proof cells invertible, so we can close this.

I am leaving #789 open so we can think about making theorem cells invertible too in certain cases.