We should have wrapper functions around GAT models, like compose, etc., which are exported from the module where categories are defined.
Note that these would not be the functions that you overload in order to define a model. Rather, these call ap, typarg, and checkvalidity with Val types of the appropriate level.
We should have wrapper functions around GAT models, like
compose
, etc., which are exported from the module where categories are defined.Note that these would not be the functions that you overload in order to define a model. Rather, these call
ap
,typarg
, andcheckvalidity
with Val types of the appropriate level.I.e.
We also need
@getlvl
for this to work.