Нужно ли мне неоднородное равенство?

Краткая предыстория: я реализую контексты и переименования, используя индексы де Брейна, а затем расширяю эти понятия с помощью «неопределенного» имени, написанного ε. Неопределенное имя индуцирует частичный порядок имен в Γ, а также переименований между Γ и Γ '. Поиск имени в переименовании (get) и связанной функции put, которая инвертирует get определенным образом, приводит к (довольно тривиальной) связи Галуа. Вот урезанный код:

module Temp where

   open import Relation.Binary
   open import Data.Fin using (Fin; zero; suc)
   open import Data.Maybe renaming (nothing to ε; just to [_]) hiding (map)
   open import Data.Nat using (ℕ; zero; suc)
   open import Data.Product
   open import Function
   open import Relation.Binary.PropositionalEquality

   -- Pointed version of Fin, with ε indicating an undefined name.
   Name : ℕ → Set
   Name = Maybe ∘ Fin

   -- The type of names below x.
   data ↓_ {Γ} : Name Γ → Set where
      ε : {x : Name Γ} → ↓ x
      [_] : (x : Fin Γ) → ↓ [ x ]

   -- A proof that two upper-bounded names are related.
   data _≤_ {Γ} : {x : Name Γ} → ↓ x → ↓ x → Set where
      ε : {x : Name Γ} {x : ↓ x} → ε ≤ x
      [_] : (x : Fin Γ) → [ x ] ≤ [ x ]

   ≤-refl : ∀ {Γ} {y : Name Γ} → Reflexive (_≤_ {x = y})
   ≤-refl {x = ε} = ε
   ≤-refl {x = [ x ]} = [ x ]

   -- Functorial action of suc on a name.
   suc⁺₀ : ∀ {Γ} → Name Γ → Name (suc Γ)
   suc⁺₀ ε = ε
   suc⁺₀ [ x ] = [ suc x ]

   -- Lifting of suc⁺₀ to down-sets.
   suc⁺ : ∀ {Γ} {x : Name Γ} → ↓ x → ↓ suc⁺₀ x
   suc⁺ ε = ε
   suc⁺ [ x ] = [ suc x ]

   -- A renaming from Γ Γ′.
   data Ren : ℕ → ℕ → Set where
      [] : ∀ {Γ} → Ren zero Γ
      _∷_ : ∀ {Γ Γ′} → Name Γ′ → Ren Γ Γ′ → Ren (suc Γ) Γ′

   -- The type of renamings below ρ.
   data Ren-↓_ : ∀ {Γ Γ′} → Ren Γ Γ′ → Set where
      [] : ∀ {Γ} → Ren-↓ ([] {Γ})
      _∷_ : ∀ {Γ Γ′} {x : Name Γ′} {ρ : Ren Γ Γ′} →
            ↓ x → Ren-↓ ρ → Ren-↓ (x ∷ ρ)

   -- Least renaming below ρ.
   Ren-ε : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} → Ren-↓ ρ
   Ren-ε {ρ = []} = []
   Ren-ε {ρ = _ ∷ _} = ε ∷ Ren-ε

   -- Interpret a renaming as a function.
   get₀ : ∀ {Γ Γ′} → Ren Γ Γ′ × Name Γ → Name Γ′
   get₀ (_ , ε) = ε
   get₀ (x ∷ _ , [ zero ]) = x
   get₀ (_ ∷ ρ , [ suc y ]) = get₀ (ρ , [ y ])

   -- Lift get₀ to down-sets.
   get : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} {x : Name Γ} →
         Ren-↓ ρ × ↓ x → ↓ get₀ (ρ , x)
   get (_ , ε) = ε
   get (x ∷ _ , [ zero ]) = x
   get ( _ ∷ ρ , [ suc x ]) = get (ρ , [ x ])

   -- Lower adjoint of get.
   put : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} (x : Name Γ) →
         ↓ get₀ (ρ , x) → Ren-↓ ρ × ↓ x
   put ε ε = Ren-ε , ε
   put {ρ = _ ∷ _} [ zero ] ε = Ren-ε , ε
   put {ρ = ._ ∷ _} [ zero ] [ x ] = [ x ] ∷ Ren-ε , [ zero ]
   put {ρ = _ ∷ _} [ suc x ] u = map (_∷_ ε) suc⁺ (put [ x ] u)

Это установка. Теперь я хотел бы показать, что get и put образуют связь Галуа. Один из способов сделать это - показать, что каждая функция является монотонной, а из двух их составных частей одна является инфляционной, а другая дефляционной. Все в порядке, за исключением того, что я застреваю, пытаясь показать, что композит get∘put инфляционный:

   id≤get∘put : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} (x : Name Γ)
                (u : ↓ get₀ (ρ , x)) →  u ≤ get (put x u)
   id≤get∘put ε ε = ε
   id≤get∘put {ρ = _ ∷ _} [ zero ] ε = ε
   id≤get∘put {ρ = ._ ∷ _} [ zero ] [ _ ] = ≤-refl
   id≤get∘put {ρ = y ∷ ρ} [ suc x ] u 
      with put [ x ] u | id≤get∘put {ρ = ρ} [ x ] u
   ... | ρ′ , x′ | u′ = {!!}

В моем контексте это u ≤ get (ρ′ , x′) из рекурсивного вызова функции. Я хотел бы использовать это для определения цели, а именно u ≤ get (ε ∷ ρ′ , suc⁺ x′). Интуитивно это должно быть легко, поскольку поиск x' в ρ′ должен быть таким же, как поиск преемника x' в ρ′, расширенном с дополнительным именем. Фактически должно быть легко показать, что get (ρ′ , x′) равно get (ε ∷ ρ′ , suc⁺ x′).

Но если я попытаюсь сформулировать соответствующую лемму:

   -- Not typeable, because ≡ requires homogeneous types?
   postulate
      not-ok : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} {x : Name Γ}
               (ρ′ : Ren-↓ ρ) (x′ : ↓ x) → get (ρ′ , x′) ≡ get (ε ∷ ρ′ , suc⁺ x′)

тогда Agda жалуется, потому что два вызова get (который get₀ поднят до пониженных значений) имеют разные типы. Это потому, что тип get упоминает значение, вычисленное get₀.

Однако эти два вызова "на самом деле" не имеют разных типов, поэтому я могу доказать следующую лемму:

   -- This is related to the lemma I want, but not quite it.
   ok : ∀ {Γ Γ′} (ρ₀ : Ren Γ Γ′) (x₀ : Name Γ) → 
        get₀ (ρ₀ , x₀) ≡ get₀ (ε ∷ ρ₀ , suc⁺₀ x₀)
   ok _ ε = refl
   ok (_ ∷ _) [ zero ] = refl
   ok (_ ∷ ρ) [ suc x ] = ok ρ [ x ]

Я еще не использовал гетерогенное равенство в Agda, и, честно говоря, я действительно не знаю, как его использовать. Позволит ли это сформулировать нужную мне лемму?