agda-categories
agda-categories copied to clipboard
Naming of fields in CartesianClosed Functor
See PR #339 by @Trebor-Huang for the details. The current names are sub-optimal.
After looking at some materials, I think a good candidate is ^-comp standing for comprison maps. Generally, when some functor is expected to respect some structure, there's often already a onesided map. So we can similarly have ×-comp which is roughly F(X×Y) → FX × FY etc.
(Sorry for the slowness, my term was crazy. Slowly emerging now.)
Comparing with monoidal functor, I think that ^-homo would perhaps be an even better name?