[Agda] Reflection with terms in different universes

[Roman]

I think both your attempts are plausible. I've done a similar thing to this:

> One idea was to replace the magmas with placeholders (say, natural
numbers) during reflection.

when I needed to evaluate types of the following form:

    data Type n : Set where
      Var : Fin n -> Type n
      _⇒_ : Type n -> Type n -> Type n

to regular Agda types. The idea is that you generate an implicit
product vector for levels using

    _^_ : ∀ {α} -> Set α -> ℕ -> Set α
    A ^ 0     = Lift ⊤
    A ^ suc n = A × A ^ n

and supply a universe for each of these levels:

    Sets : ∀ {n} -> (αs : Level ^ n) -> Set blah-blah
    Sets {0}      _       = ⊤
    Sets {suc _} (α , αs) = Set α × Sets αs

The interpretation function then is

    ⟦_⟧ᵗˡ : ∀ {n} σ -> Level ^ n -> Level
    ⟦ Var i ⟧ᵗˡ αs = lookup i αs
    ⟦ σ ⇒ τ ⟧ᵗˡ αs = ⟦ σ ⟧ᵗˡ αs ⊔ ⟦ τ ⟧ᵗˡ αs

    ⟦_⟧ᵗ : ∀ {n} {αs : Level ^ n} σ -> Sets αs -> Set (⟦ σ ⟧ᵗˡ αs)
    ⟦ Var i ⟧ᵗ As = Lookup i As
    ⟦ σ ⇒ τ ⟧ᵗ As = ⟦ σ ⟧ᵗ As -> ⟦ τ ⟧ᵗ As

Then when you need to construct a term rather than a type, you make
those implicit `{αs : Level ^ n} {As : Sets αs}` and Agda will
perfectly unify them with, say, ∀ {l} {M : Magma l} {l′} {N : Magma
l′} from your example.

For example, for me it was

    ⟦_⟧ : ∀ {n Γ σ} {αs : Level ^ n} {As : Sets αs} -> Γ ⊢ σ -> ⟦ Γ ⟧ᶜ
As -> ⟦ σ ⟧ᵗ As

The `Sets` machinery can be found at [1].
The example interpretation can be found at [2].

[1] https://github.com/effectfully/STLC/blob/master/src/STLC/Lib/Sets.agda
[2] https://github.com/effectfully/STLC/blob/master/src/STLC/Semantics/Eval.agda