Zuerst ein paar langweilige Importe:

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)

Angenommen, ich habe einen Typ, der beispielsweise von den Naturals indiziert wird.

postulate Foo : ℕ -> Set

Und das möchte ich einige Gleichheiten über Funktionen beweisen, die auf diesem Typ arbeitenFoo. Da agda nicht sehr klug ist, handelt es sich um heterogene Gleichheiten. Ein einfaches Beispiel wäre

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 !}

Das Ziel in bar ist

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

Was ist das|Machst du im Ziel? Und wie fange ich überhaupt an, einen solchen Begriff zu konstruieren?

In diesem Fall kann ich das Problem umgehen, indem ich die Ersetzung mit manuell vornehmesubst, aber das wird wirklich hässlich und langweilig für größere Typen und Gleichungen.

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