小编Twa*_*ven的帖子

首先是一些无聊的进口:

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.因为agda不是很聪明,所以这些将是异构的平等.一个简单的例子就是

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

bar : (m n : ?) (x : Foo …