"subst" where indices to be equated also use subst

Question

I'm stuck on the following. I have the derivation of a pi calculus transition that takes place in some context Γ, plus a proof that Γ ≡ Γ′. I would like to coerce the derivation into a transition in Γ′, using subst. The details of the setting are mostly unimportant, as usual.

module Temp where
   open import Data.Nat as Nat using (_+_) renaming (ℕ to Cxt)
   open import Function
   open import Relation.Binary.PropositionalEquality

   data _⟿ (Γ : Cxt) : Set where
      bound : Γ ⟿
      nonBound : Γ ⟿

   target : ∀ {Γ} → Γ ⟿ → Cxt
   target {Γ} bound = Γ + 1
   target {Γ} nonBound = Γ

   data Proc (Γ : Cxt) : Set where
   data _—[_]→_ {Γ} : Proc Γ → (a : Γ ⟿) → Proc (target a) → Set where

   -- Use a proof that Γ ≡ Γ′ to coerce a transition in Γ to one in Γ'.
   coerce : ∀ {Γ Γ′} {P : Proc Γ} {a R} → P —[ a ]→ R → (q : Γ ≡ Γ′) →
               subst Proc q P —[ subst _⟿ q a ]→ subst (Proc ∘ target) {!!} R
   coerce E refl = {!!}

It's easy enough to coerce both the source P of the transition, and the action a which appears as a label on the transition. The problem is the target R of the transition, whose type depends on a. In the coerced transition, I use subst to coerce a from Γ ⟿ to Γ' ⟿. Naively, I would like to then also use subst to change the type of R from Proc (target a) to Proc (target (subst _⟿ q a) by showing that the Proc indices are equal. However, by its very nature subst _⟿ q a has a distinct type from a, so I'm unsure how to do this. Maybe I need to use the proof of Γ ≡ Γ′ again or somehow "undo" the inner subst to unify the types.

Is what I'm trying to do reasonable? If so, how do I coerce R given the heterogeneity?

Answer 1

Generally, when you want to compare two things of different types (that can become equal given suitable reduction), you would want to use heterogeneous equality.

The proof that subst doesn't actually change the value cannot be done with usual (propositional) equality, because a and subst P q a have different types. However, once you know that q = refl, you can reduce those expressions enough so that their types now match. This can be expressed using heterogeneous equality:

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

This allows you to even express the fact that a ≅ subst P q a. When you then pattern match on q, the goal reduces to simple a ≅ a, which can then be proven by reflexivity:

≡-subst-removable : ∀ {a p} {A : Set a}
                    (P : A → Set p) {x y} (eq : x ≡ y) z →
                    P.subst P eq z ≅ z
≡-subst-removable P refl z = refl

---

So, the first instinct is to change the last subst to heterogeneous subst (from Relation.Binary.HeterogeneousEquality) and use the proof ≡-subst-removable. This almost works; the problem is that this subst cannot capture the change from a : Γ ⟿ to Γ′ ⟿.

As far as I know, the standard library doesn't provide any alternate substs that capture this interaction. The simple solution is to write the combinator ourselves:

subst′ : ∀ {Γ Γ′} {a} (q : Γ ≡ Γ′) (R : Proc (target a)) →
         Proc (target (subst _⟿ q a))
subst′ refl R = R

As you noted in the comments, this can be further generalized. However, unless you expect to do a lot of proofs of this kind, this generalization is not very useful since the problem is fairly rare and for the simpler cases, heterogeneous equality usually does the work.