Decide on the kind of functors

[omelkonian]

Functors are currently given the type/kind: Type↑ = ∀ {ℓ} → Type ℓ → Type ℓ . This disallows valid cases that the level changes in the output index, so we should carefully decide which ones we want to support + provide alternative definitions to cover the rest.

@WhatisRT has a use case for his axiomatic set-theory library, where one cannot a monad instance for the powerset construction.

---

Possible alternative definitions:

• outer quantification: Type↑ a b = Type a → Type b (e.g. covers disjoint union / co-products, but fails for TC)
  • c.f. PR Change Monad polymorphism #11
• the ultra-general Type↑ f = ∀ {ℓ} → Type ℓ → Type (f ℓ)
  • c.f. PR Change Monad polymorphism #19
• ...

[omelkonian]

Eventually settled on the output-reindexing approach of #19, as #11 is not as general (no cross-level maps) and #20 is too general for unification's sake (but it also allows input-reindexing, also enabling non-polymorphic instances).

Only downside: we no longer allow non-polymorphic instances (e.g. Type -> Type).

[WhatisRT]

Another use case that I've encountered recently: A Monad (or KleisliTriple) from agda-categories operates always at a fixed level (and there's no obvious way to change that). I think we should support both use cases, and the only way I know how to is by having both variants, even if it means duplication.

[omelkonian]

Hmm, I would need a more detailed example to justify duplicating the whole library :P

But as a first gut feeling, I do not think our class definitions should have anything to do with the categorical stuff in agda-categories, right?

It's interesting the construction you point at uses relative monads, which was suggested as a thing to look at by Mauro Jaskelioff when I showed him this Monad-level issue, as a way to actually think about universe levels in the categorical setting.

[WhatisRT]

My categorical-crypto library already contains machinery to translate a monad in the sense of this library into an agda-categories monad because I needed it for something. This would be about the reverse direction. I don't think we need to do anything right now, but I do think it's good to collect data points.