Najpierw nudne importy:

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)

Załóżmy teraz, że mam typ indeksowany przez, powiedzmy, naturals.

postulate Foo : ℕ -> Set

I że chcę udowodnić pewne równości dotyczące funkcji działających na tym typieFoo. Ponieważ agda nie jest zbyt mądra, będą to heterogeniczne równości. Prostym przykładem może być

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

Celem w barze jest

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

Co to jest|robi w celu? A jak mogę zacząć konstruować termin tego typu?

W tym przypadku mogę obejść problem, ręcznie wykonując podstawienie za pomocąsubst, ale to staje się naprawdę brzydkie i nużące dla większych typów i równań.

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