[Agda] lifting from Set to Set1

[Chris Casinghino]

Hi Agda hackers,

In some agda code I've been working on lately, I am often in the
position of having a Set0 where a Set1 is expected.  In particular, I
have functions of type (... -> Set1), but in some cases the thing I'd
like them to return is actually in Set0.  This results in an error,
agda complains:

Set !=< Set1

A hack to get around this is to define:

data [_] : Set -> Set1 where
  ↑ : { A : Set } -> A -> [ A ]

And use [t] when t is a Set we want to be a Set1.  But this is
annoying because we must unpack and repack this constructor in many
places in our code.  So, I have two questions

1) Why isn't (Set =< Set1) in Agda?  I know this is the case in UTT

2) Are there standard ways to get around this, or better hacks than
this one?  I couldn't find anything on the wiki.

Thanks for your help!

--Chris Casinghino