Equations between morphisms in notebook types

[KevinDCarlson]

Ahead of notebook elaboration of equations, this PR introduces equations into the notebook_types modules model, model_judgment, diagram_judgment, thus necessitating an upgrade of notebook types to v2. Other than the modules already listed, the main change of interest is in document, which includes code for migrating v1 to v2 documents. The only actual modification this migration requires is changing the version number, but there's some slightly wordy unpacking and repacking seemingly necessary since we have to reconstruct ModelJudgment and DiagramJudgment types for the new version.

It's probably possible to argue for not bothering with upgrading DiagramJudgment at this time, since we have no type theoretic treatment of diagrams yet, but I figured it's a minor enough change which we may want before long and versioning notebook_types is a bit fiddly. Some more specific comments are attached in the diff.

[KevinDCarlson]

I found it was necessary to remove TSIFY annotations from some old types to make the versioning work here. This didn't cause problems on the v0 -> v1 upgrade because the redefined types were structurally identical, but we actually had duplicated type definitions in the WASM output.

[epatters]

Knowing when to bump the notebook types version can be confusing. The main principle is this: we only bump the version and write a migration for changes that would break existing user data. Changes or additions to the notebook types for which existing data would remain valid do not trigger a version bump.

The most common example of such a safe change is adding new variants to an enum. And fortunately that's exactly what we have here.

So this PR can be much simplified by just adding the Equation variant to the existing v1 type ModelJudgment. We did the same thing when adding instantiations:

• #761

revised