Pushout of theories

One of the motivating features behind the Gatlab redesign was to be able to do pushouts of theory morphisms.

This is easy in the case of "strict" theory morphisms, where each type/term constructor is sent to a basic term (i.e., not a composite). We can then compute a "strict" pushout, where we don't have to add any equalities because we simply identify the relevant term/type constructors.

In the case where term constructors are sent to complex terms, we can compute "weak" pushouts, where we add equalities to the coproduct of the two theories.

However, we don't have equations between types, so we cannot compute a pushout unless all the type constructors are sent to basic types.

This implies that we should have three types of theory morphisms. The strictest type of theory morphism is simply a vector of integers, mapping each judgment in the domain to a judgment in the codomain.

The second strictest type of theory morphism maps each type constructor to a judgment in the other theory that has to match the first type constructor exactly, but term constructors can map to general term.

The third, weakest type is the current `TheoryMap`.

We can have all of these in one structure by redefining `Composite` to be `Union{Typ,Term,Nothing,Lvl}`, where `Lvl` refers to an entire judgment. Then for the "strictness" check, we can just check that all of the judgments in the domain are sent to `Lvl` arguments.

The easiest pushout to implement and work with is the strict pushout, and even this will give us a lot to work with. The pushout of Y <- X -> Z just is the judgments in Y followed by the judgments in Z\X. The tricky bit is just reindexing the judgments in Z\X.

We also will want to be able to rename judgments.

We should also come up with a nice syntax for this, that doesn't bias to the 2-ary pushout.