we want the fields (e.g. obj) to be accessible outside of the nested module as accessor functions. This eliminates a lot of boilerplace with respect to \usemodule and "nested mathstructures" (think Functor { C : Category, D : Category}), but poses the new challenge of differing arities and notations depending on whether one is "inside" or "outside" the mathstructure.
given a mathstructure
we want the fields (e.g.
obj) to be accessible outside of the nested module as accessor functions. This eliminates a lot of boilerplace with respect to\usemoduleand "nested mathstructures" (thinkFunctor { C : Category, D : Category}), but poses the new challenge of differing arities and notations depending on whether one is "inside" or "outside" the mathstructure.=> Need something like
where
\thisinstanceexpands to either nothing or the structure whose field this is (e.g. in\vC{obj}) , or#1on the "outside" (e.g.\obj{\vC!})