# logic – “Universe-shrinking” function in Agda

Agda does not allow datatypes in one universe to be parametrized or indexed by a type in a larger universe (strangely, Coq does not appear to require this for propositional inductives, but perhaps this is).

What then, can we say about the definable functions from `Set₁` to `Set`? In particular, can we prove the existence of a non-constant function without applying any axioms?

That is, can we construct a function `f` from `Set₁` to `Set` such that there are types `t₁ t₂ : Set₁` with `¬(f t₁ ≡ f t₂)`