Every definition has a single (predicative) level, but it might be useful to have a definition with additional levels. For example, the type of categories might have two levels: for objects and for morphisms. We can allow this as follows:
Here, l is an addition level; \lp after \Level just indicates that this is a predictive level (as opposed to homotopy level). Maybe, we can add two keywords instead (e.g., \pLevel and \hLevel).
Also, we can add equations in the declaration of additional levels. For example,
Additional levels will be implicit just as ordinary levels and will be inferred as usual. If needed, they can be specified explicitly after \lp and \lh arguments.
Every definition has a single (predicative) level, but it might be useful to have a definition with additional levels. For example, the type of categories might have two levels: for objects and for morphisms. We can allow this as follows:
Here,
l
is an addition level;\lp
after\Level
just indicates that this is a predictive level (as opposed to homotopy level). Maybe, we can add two keywords instead (e.g.,\pLevel
and\hLevel
).Also, we can add equations in the declaration of additional levels. For example,
Additional levels will be implicit just as ordinary levels and will be inferred as usual. If needed, they can be specified explicitly after
\lp
and\lh
arguments.