search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Naming of fields in CartesianClosed Functor #344

Open JacquesCarette opened 2 years ago

JacquesCarette commented 2 years ago

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

Trebor-Huang commented 2 years ago

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.

JacquesCarette commented 2 years ago

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