您不会在这里遗漏任何明显的东西。即使Key⁺ 忽略了Value 参数，Agda 仍然将它们视为不同的类型。但是，您可以很容易地编写转换函数。我将打开一些模块以保持名称可以接受：
open Extended-key
open Height-invariants
open import Data.Nat
移动Key⁺ 非常容易，因为底层Keys 是相同的：
to : ∀ {A B} → Key⁺ A → Key⁺ B
to ⊥⁺ = ⊥⁺
to ⊤⁺ = ⊤⁺
to [ k ] = [ k ]
移动_<⁺_ 关系也是可行的，您只需要在Key⁺s 上进行模式匹配，以便将类型简化为（基本上）身份：
to< : ∀ {A B} l u → _<⁺_ A l u → _<⁺_ B (to l) (to u)
to< ⊥⁺ ⊥⁺ p = p
to< ⊥⁺ ⊤⁺ p = p
to< ⊥⁺ [ _ ] p = p
to< ⊤⁺ _ p = p
to< [ _ ] ⊥⁺ p = p
to< [ _ ] ⊤⁺ p = p
to< [ _ ] [ _ ] p = p
现在，这似乎应该可以解决问题，但是当您尝试将其写下来时，您很快就会发现您还需要一种运输天平的方法。同样，没什么特别的：
to∼ : ∀ {A B h₁ h₂} → _∼_ A h₁ h₂ → _∼_ B h₁ h₂
to∼ ∼+ = ∼+
to∼ ∼0 = ∼0
to∼ ∼- = ∼-
fmap 的类型则如下所示：
fmap : ∀ {A B} (f : ∀ {x} → A x → B x) {l u h} →
Indexed.Tree A l u h → Indexed.Tree B (to l) (to u) h
这不是一个“真实的”fmap，但考虑到您需要有不同的Key⁺s，这是我们可以得到的最接近的。
leaf case 需要使用to<，但在其他方面是微不足道的：
fmap f {lb} {ub} (Indexed.leaf l<u) = Indexed.leaf (to< lb ub l<u)
node case 是事情变得有趣的地方。显而易见的解决方案：
fmap f (Indexed.node (k , v) l r bal) =
Indexed.node (k , f v) (fmap f l) (fmap f r) (to∼ bal)
不进行类型检查。让我们找出原因。以下是上述表达式的类型和目标类型：
-- Have:
Indexed.Tree .B (to .l) (to .u) (suc (max .B (to∼ bal)))
-- Goal:
Indexed.Tree .B (to .l) (to .u) (suc (max .A bal))
所以我们需要一个额外的证明：
max≡ : ∀ {A B} {h₁ h₂} (bal : _∼_ A h₁ h₂) →
max A bal ≡ max B (to∼ bal)
max≡ ∼+ = refl
max≡ ∼0 = refl
max≡ ∼- = refl
最后，我们可以通过max≡ bal重写目标类型，得到想要的实现：
fmap f (Indexed.node (k , v) l r bal) rewrite max≡ bal =
Indexed.node (k , f v) (fmap f l) (fmap f r) (to∼ bal)
我也在使用树的更依赖的变体。这是通过将AVL 模块定义为：
import Data.AVL
module AVL (Value : Key → Set)
= Data.AVL Value isStrictTotalOrder
然后简单地要求映射函数尊重Key 值：
mapping-function : {A B : Key → Set} {x : Key} → A x → B x
还有另一种选择：重写Data.AVL 模块，使Extended-key 和Height-invariants 不被Value 参数化。虽然这需要更改标准库，但我认为这是更好的解决方案。 Extended-key 和 Heigh-invariants 在 Data.AVL 之外肯定有用 - 事实上，我有一个 Data.BTree 正是使用它。
如果您决定采用这种方式，请考虑将它们分成新模块（例如Data.ExtendedKey）并提交补丁/拉取请求。