"Universe-shrinking" function in Agda

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

• I don't know for sure, but this smells like a parametricity thing Aug 30 at 5:53
• Agda does allow parameters in arbitrary larger universes. Aug 30 at 8:39
• @AndrásKovács oh, well that would be an easy solution there. I tried this but perhaps made a typo and accidentally had it treated as an index. I was able to parametrize by a higher universe even with --without-K so this could be an answer Aug 30 at 16:48
• Ah so actually yes that was it. While you can technically parametrize, there doesn't appear to be any way to use the larger type in a constructor, so it must be a phantom parameter and can't enable proofs of inequality. I've updated the text of the question to say non-trivially Aug 30 at 16:50