agda学习笔记---等式

 

可以开始证明之前用到的好多东西了

这是训练与emacs互动的好机会（

sym : ∀ {A : Set} {x y : A}
    → x ≡ y
    → y ≡ x

sym refl = refl

trans : ∀  {A : Set} {x y z : A}
    → x ≡ y
    → y ≡ z 
    → x ≡ z 

trans refl refl = refl

cong : ∀ {A B : Set} (f : A → B) {x y : A}
    → x ≡ y
    → f x ≡ f y

cong f refl = refl

cong-app : ∀ {A B : Set} {f g : A → B} 
    → f ≡ g 
    → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl