Сначала скучный импорт:

import Relation.Binary.PropositionalEquality as PE
import Relation.Binary.HeterogeneousEquality as HE
import Algebra
import Data.Nat
import Data.Nat.Properties
open PE
open HE using (_≅_)
open CommutativeSemiring commutativeSemiring using (+-commutativeMonoid)
open CommutativeMonoid +-commutativeMonoid using () renaming (comm to +-comm)

Теперь предположим, что у меня есть тип, проиндексированный, скажем, натуральными.

postulate Foo : ℕ -> Set

И что я хочу доказать некоторые равенства в отношении функций, работающих с этим типомFoo, Поскольку агда не очень умна, это будут неоднородные равенства. Простой пример будет

foo : (m n : ℕ) -> Foo (m + n) -> Foo (n + m)
foo m n x rewrite +-comm n m = x

bar : (m n : ℕ) (x : Foo (m + n)) -> foo m n x ≅ x
bar m n x = {! ?0 !}

Цель в баре

Goal: (foo m n x | n + m | .Data.Nat.Properties.+-comm n m) ≅ x
————————————————————————————————————————————————————————————
x : Foo (m + n)
n : ℕ
m : ℕ

Что это|делает в цели? И как мне вообще начать строить термин такого типа?

В этом случае я могу обойти проблему, выполнив замену вручнуюsubst, но это становится действительно уродливым и утомительным для больших типов и уравнений.

foo' : (m n : ℕ) -> Foo (m + n) -> Foo (n + m)
foo' m n x = PE.subst Foo (+-comm m n) x

bar' : (m n : ℕ) (x : Foo (m + n)) -> foo' m n x ≅ x
bar' m n x = HE.≡-subst-removable Foo (+-comm m n) x