GATs aren't able to express everything (such as sum types, function types) and therefore it is a useful design pattern to be able to declare a type in a theory and expect models of that theory to send it to a specific Julia type, for example DiscDiagram::TYPE might be expected to be sent to Catlab's DiscreteDiagram type, which can't be axiomatized in a GAT (insofar as it involves a list of objects).

There ought be a means of making this assumption explicit (and enforceable) rather than just left to documentation.

For example:

@theory ThCategoryUnbiasedCoproducts <: ThCategoryWithColimits begin
  DiscDiagram::TYPE{DiscreteDiagram} # uses whatever `DiscreteDiagram` is in scope
  colimit(d::DiscDiag)::Colimit 
  universal(Σ::Colimit, d::DiscDiag, csp::MCospan)::(ob(Σ) → apex(csp))
end

Then @instance ThCategoryUnbiasedCoproducts{...} would not require filling in a Julia type for the DiscDiagram sort.

Some issues: if the theory stores Julia types, then GATs which use this feature are no longer serializable. It's hard to imagine what theory morphisms could do other than demand that any TYPE{Foo} be sent to another TYPE{Foo} in the codomain (requires checking equality of types).

A natural follow-up would be to associate a particular julia method name with a term constructor of the theory, but that hasn't yet shown up as obviously useful.