agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard

Naming of fields in CartesianClosed Functor

Open JacquesCarette opened this issue 3 years ago • 2 comments

See PR #339 by @Trebor-Huang for the details. The current names are sub-optimal.

JacquesCarette avatar Mar 25 '22 19:03 JacquesCarette

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.

Trebor-Huang avatar Apr 05 '22 17:04 Trebor-Huang

(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?

JacquesCarette avatar Apr 15 '22 13:04 JacquesCarette