[Agda] Converting Relation.Unary to be universe-polymorphic

[Daniel Peebles]

Hi all,

Well, more specifically my goal is to get a universe-polymorphic
Data.Graph.Acyclic, and that requires a universe-polymorphic
Induction.WellFounded which requires a universe-polymorphic Induction,
which requires a universe-polymorphic Relation.Unary. Talk about Yak
shaving! :)

Anyway, Relation.Unary's main function is, with universe polymorphism:

Pred : ∀ {ℓ} → Set ℓ → Set (suc ℓ)
Pred {ℓ} a = a → Set ℓ

Then I run into two major issues that I'm not sure how to resolve in a
pleasant manner. There's a Dummy module containing a bunch of utility
functions parametrized by a Set, and if I raise that Set to be a Set
in an arbitrary universe, I run into the issue of needing a
universe-polymorphic ⊥. This is fairly easy to change, but making its
level an implicit parameter doesn't really work because the
typechecker can never infer the correct level, and making it an
explicit parameter would break practically the entire standard
library. So I'm not really sure what to do about that problem. Maybe
Pred should be a -> Set for any level of a? I don't really have a very
good mental model of predicates in higher universes.

The other major problem in Relation.Unary I have is with the _⟨⊎⟩_
operator at the bottom of the module. Fully universe-polymorphic, its
type is (I think):

∀ {ℓA ℓB : Level} {A : Set ℓA} {B : Set ℓB} → Pred A → Pred B → Pred (A ⊎ B)

But if I maintain the original definition, applying either one of the
input predicates gives me a Set either in ℓA or ℓB, and the return
type is in ℓA ⊔ ℓB, and agda can't unify those two. I'm not sure how I
can "lift" both those into the combined Set.

Thanks for any help, and apologies if this is all wrong!
Dan