Equation types in DoubleTT

[KevinDCarlson]

Resolves #782

We add type syntax and values for identity types, with the intended usage being for extensional equality types for morphism terms.

The formal syntax is Id(TyS,TmS,TmS) where the two terms will evaluate as members of the evaluation of the type, and similar for the value. This type is displayed and entered in plain text as a == b.

In the text elaborator, we throw errors if the user attempts to construct the equality type between two terms that are not in a Morphism type, or if their types are not themselves convertible.

We have a snapshot test to look at the model generated by a commutative square, as well as an test internal to Rust to confirm that this model successfully gets an equation, as a stopgap while pretty-printing for equations remains unimplemented.

The largest diff is in modelgen, but part of this diff count is spurious: we move a lot of methods from modelgen::Model to ModelGenerator. This is for consistency with the primary really new function, make_mor, which makes a morphism in a ModelGenerator's model, but needs access to the theory in order to make the object of an identity morphism's basepoint. It would be possible to move the moved stuff back and put make_mor on Model, at the cost of asking it to carry around an extra ObType argument for the Id case that would be irrelevant in the other cases.

For making composite morphisms, we include an unchecked concat_paths function, which is only used to concatenate paths built from morphism terms which we already know to match up from syn. This function could be moved onto Path if that seems desirable.

I haven't included any way for the elaborator to use the equations from the equality type itself, since there should be no need: we never need to run equal_tm modulo propositional equality on morphism terms. I also haven't included a refl equality term, since again there's no obvious need for it; we just let equalities eta-convvert to tt.

I haven't tried to do anything with the notebook elaborator yet. I think this requires changes to the notebook data structure first, right?

[KevinDCarlson]

@epatters You were wondering about what I was muttering about an eta-conversion to tt; this is used in eta_neu(tm) where tm : Id(_,_,_) is an equation, rather than before when tm:Hom(_,_,_) was a morphism. That is, any two terms of an identity type will check as equal up to eta, so the type theory behaves extensionally in this way. I think that in fact we will never even actually run this eta in the current state.

[epatters]

Thanks Kevin, this is really nice work. Just a few small comments below.

[epatters]

@KevinDCarlson, I noticed this problem while doing a little cleanup.

To avoid a build up of PRs and subsequent merge conflicts, I'm going to merge this as is but I have created #1070 as a tracking issue.