omelkonian / agda-stdlib-classes Goto Github PK

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)
• the ultra-general Type↑ f = ∀ {ℓ} → Type ℓ → Type (f ℓ)
• ...