Agda does not allow datatypes in one universe to be indexed by, or non-trivially parametrized by a type in a larger universe (strangely, Coq does not appear to require this for propositional inductives, but perhaps this is related to prop erasure).
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₂)