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? In particular, can we prove the existence of a non-constant function without applying any axioms?
That is, can we construct a function
Set such that there are types
t₁ t₂ : Set₁ with
¬(f t₁ ≡ f t₂)