[ add ] `Level`-lifting for `Relation.Binary.{Structures|Bundles}` and `Algebra.{Structures|Bundles}`

[jamesmckinna]

Try:

  lift : ∀ a → Setoid c (a ⊔ ℓ)
  lift a = record
    { _≈_ = _≈↑_
    ; isEquivalence = record { refl = refl↑ ; sym = sym↑ ; trans = trans↑ }
    }
    where
    _≈↑_ : Rel Carrier (a ⊔ ℓ)
    x ≈↑ y = Level.Lift a (x ≈ y)
    refl↑ : Reflexive _≈↑_
    refl↑ = Level.lift refl
    sym↑ : Symmetric _≈↑_
    sym↑ (Level.lift x≈y) = Level.lift (sym x≈y)
    trans↑ : Transitive _≈↑_
    trans↑ (Level.lift x≈y) (Level.lift y≈z) = Level.lift (trans x≈y y≈z)

While @andreasabel is correct regarding the defined choice of Levels for bundles in stdlib, I do still regret that Agda's approach to level polymorphism for records makes this kind of heavyweight construction necessary... given that a record is a particular kind of parametrised Set, it's pity that Level-lifting for Set can't 'see through' the telescopic parametrisation associated to records.

Originally posted by @jamesmckinna in #2766

Presumably under Relation.Binary.Construct.Lift and Algebra.Construct.Lift?