小编fun*_*emy的帖子

我对 Agda 很陌生，我正在尝试做一个简单的证明“地图的组合就是组合的地图”。

（本课程中的练习）

相关定义：

_=$=_ : {X Y : Set}{f f' : X -> Y}{x x' : X} ->
        f == f' -> x == x' -> f x == f' x'
refl f =$= refl x = refl (f x)

和

data Vec (X : Set) : Nat -> Set where
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_

我想证明： …