Make Lift's level argument explicit

[anshwad10]

See the discussion at #1236

[anshwad10]

I'm also making Unit*, ⊥* and Bool* take their level arguments explicitly for the same reason

[anshwad10]

While going through the library I noticed that the stronger hypothesis of epi⇒surjective is actually unnecessary. perhaps I should fix that in a later PR

[anshwad10]

Hmm I noticed that most usages of Unit* actually don't need to give the level arguments explicitly, and when they do it's not that big of a difference between Unit* {ℓ} and Unit* ℓ (unlike the case with Lift ℓ where we have to give it as Lift {j = ℓ}). So I think Unit*, ⊥* and Bool* can keep their implicit arguments

[anshwad10]

lets go it finally typechecked
@maxsnew can you review this?

[maxsnew]

@anshwad10 can you write a summary of what is changed in this PR to make it easier to review? It is quite large so it would be good to know that you changed arguments to be explicit specifically in XYZ files and everything else is just updated to fit the new interface. Since you made the change yourself it is much easier for you to write up than it is for a reviewer to figure out.