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₂)