Instances in DoubleTT#1246
Conversation
epatters
added
enhancement
KevinDCarlson
changed the title
…screteDblModelDiagrams, behaving as dopfs
KevinDCarlson
force-pushed
the
instances_tt
branch
from
f768a25 to
7f6f9bd
Compare
…id of diagram keyword and started interpret instances as terms of types.
| weight(we.e) := w, | ||
| weight(wf.e) := w | ||
| ] | ||
|
|
There was a problem hiding this comment.
As the syntax suggests, an instance is now simply a term of the type of which it's an instance. We can declare generators explicitly with lists of new names, or by importing them from another instance (semantically, getting an instance map in from there.) We can specify mappings explicitly, as below, but the mappings need not be total, and are in that case implicitly filled out via the dopf property.
There was a problem hiding this comment.
OK, this changed a bit again: we needed to keep the standard Cons terms of dependent records for, primarily, internal reasons. These correspond semantically to tight transformations of models. I've thus reintroduced a new keyword for instance-type terms. These are expected to always be closed, thus corresponding to lax loose transformations from the point into a model--the open analogue doesn't seem obviously useful to me. So the semantics at the moment is in the category of instances of models, fibered over the category of models and tight transformations.
2 participants
Here are some instances in doublett. Runnable for text elaborator, notebook elaborator TBD pending #1257