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.
olynch
commented
1 year ago
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
Compositeto beUnion{Typ,Term,Nothing,Lvl}, whereLvlrefers to an entire judgment. Then for the "strictness" check, we can just check that all of the judgments in the domain are sent toLvlarguments.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.