[Agda] Reflection with terms in different universes

[Jannis Limperg]

Dear all,

I'm trying and failing to write a reflective simplification tactic
involving terms at different universe levels. (Jesper: Here's yet
another argument for cumulativity.) For a simple example, consider
the following definitions of magmas and their morphisms:

\begin{code}
open import Agda.Primitive using (lsuc ; _⊔_)

record Magma l : Set (lsuc l) where
  field
    Carrier : Set l
    eq : Carrier → Carrier → Set l
    plus : Carrier → Carrier → Carrier

open Magma

record _⇒_ {l} (M : Magma l) {l′} (N : Magma l′) : Set (l ⊔ l′) where
  field
    arr : Carrier M → Carrier N
    resp : ∀ {x y}
      → eq M x y → eq N (arr x) (arr y)
    plus : ∀ {x y}
      → eq N (plus N (arr x) (arr y)) (arr (plus M x y))

open _⇒_
\end{code}

The tactic should simplify magma expressions. Of course, with magmas
there's not much to simplify (the actual problem involves categories and
functors), but one goal I'd like to have proven for me is this:

\begin{code}
postulate
  goal : ∀ {l} {M : Magma l} {l′} {N : Magma l′} (f : M ⇒ N) x y
    → eq N (plus N (arr f x) (arr f y)) (arr f (plus M x y))
\end{code}

To get a reflective tactic that solves this sort of goal, I'd usually
define a language of terms and an interpretation function:

\begin{code}
data Tm {l} : Magma l → Set (lsuc l) where
  var : ∀ {M} (x : Carrier M) → Tm M
  _+_ : ∀ {M} (x y : Tm M) → Tm M
  hom : {M N : Magma l} → M ⇒ N → Tm M → Tm N

⟦_⟧ : ∀ {l} {M : Magma l} → Tm M → Carrier M
⟦ var x ⟧ = x
⟦_⟧ {M = M} (x + y) = plus M ⟦ x ⟧ ⟦ y ⟧
⟦ hom f x ⟧ = arr f ⟦ x ⟧
\end{code}

But here's the rub: In a `Tm {l} M`, *all* magmas must be at level `l`.
Consequently, there is no `Tm M` corresponding to the goal above, which
contains two magmas, `M` and `N`, at different levels. So the question
is: How do I write a reflective tactic that can deal with this sort of
problem?

Here are my previous attempts at a solution, which you can probably
skip:

One idea was to replace the magmas with placeholders (say, natural
numbers) during reflection. But then the interpretation function needs
to substitute the actual magmas for the placeholders, so it needs a
mapping from natural numbers to magmas at different levels, which seems
to run into the same problem.

Another idea involves lifting all the magmas up to the maximum of their
levels during reflection. The tactic would then yield an equation that
corresponds to the goal, only with all magmas replaced by lifted ones.
Perhaps I could then reflectively generate a proof that this equation
over lifted magmas implies the goal; this proof should be entirely
syntax-directed. This approach seems promising, but before going on a
wild adventure, I wanted to ask if someone had dealt with this sort of
thing before.

Thanks for your time,
Jannis
-------------- next part --------------
Dear all,

I'm trying and failing to write a reflective simplification tactic
involving terms at different universe levels. (Jesper: Here's yet
another argument for cumulativity.) For a simple example, consider
the following definitions of magmas and their morphisms:

\begin{code}
open import Agda.Primitive using (lsuc ; _⊔_)

record Magma l : Set (lsuc l) where
  field
    Carrier : Set l
    eq : Carrier → Carrier → Set l
    plus : Carrier → Carrier → Carrier

open Magma

record _⇒_ {l} (M : Magma l) {l′} (N : Magma l′) : Set (l ⊔ l′) where
  field
    arr : Carrier M → Carrier N
    resp : ∀ {x y}
      → eq M x y → eq N (arr x) (arr y)
    plus : ∀ {x y}
      → eq N (plus N (arr x) (arr y)) (arr (plus M x y))

open _⇒_
\end{code}

The tactic should simplify magma expressions. Of course, with magmas
there's not much to simplify (the actual problem involves categories and
functors), but one goal I'd like to have proven for me is this:

\begin{code}
postulate
  goal : ∀ {l} {M : Magma l} {l′} {N : Magma l′} (f : M ⇒ N) x y
    → eq N (plus N (arr f x) (arr f y)) (arr f (plus M x y))
\end{code}

To get a reflective tactic that solves this sort of goal, I'd usually
define a language of terms and an interpretation function:

\begin{code}
data Tm {l} : Magma l → Set (lsuc l) where
  var : ∀ {M} (x : Carrier M) → Tm M
  _+_ : ∀ {M} (x y : Tm M) → Tm M
  hom : {M N : Magma l} → M ⇒ N → Tm M → Tm N

⟦_⟧ : ∀ {l} {M : Magma l} → Tm M → Carrier M
⟦ var x ⟧ = x
⟦_⟧ {M = M} (x + y) = plus M ⟦ x ⟧ ⟦ y ⟧
⟦ hom f x ⟧ = arr f ⟦ x ⟧
\end{code}

But here's the rub: In a `Tm {l} M`, *all* magmas must be at level `l`.
Consequently, there is no `Tm M` corresponding to the goal above, which
contains two magmas, `M` and `N`, at different levels. So the question
is: How do I write a reflective tactic that can deal with this sort of
problem?

Here are my previous attempts at a solution, which you can probably
skip:

One idea was to replace the magmas with placeholders (say, natural
numbers) during reflection. But then the interpretation function needs
to substitute the actual magmas for the placeholders, so it needs a
mapping from natural numbers to magmas at different levels, which seems
to run into the exact same problem.

Another idea involves lifting all the magmas up to the maximum of their
levels during reflection. The tactic would then yield an equation that
corresponds to the goal, only with all magmas replaced by lifted ones.
Perhaps I could then reflectively generate a proof that this equation
over lifted magmas implies the goal; this proof should be entirely
syntax directed. This approach seems promising, but before going on a
wild adventure, I wanted to ask if someone had dealt with this sort of
thing before.

Thanks for your time,
Jannis