Agda 小知識 [agda-0000]

在我們開始之前需要知道怎麼閱讀 agda 的證明，這裡使用的是由 Martin Escardo 維護的 TypeTopology 程式庫，下面經常會用到的是等式證明，寫成形式

A ＝⟨ B ⟩ C ∎

這段程式的意思是「因為 $B$ ，所以 $A$ 等於 $C$ 」。每個寫好的證明，都可由其他程式引用，比如

proposition-4 : {G H : 𝓤 ̇} {{∈G : Group G}} {{∈H : Group H}}
  → (φ : G → H)
  → IsGroupHomomorphism G H φ
  → φ e ＝ e

就可以引用

φ e ＝⟨ proposition-4 φ is-hom ⟩
e ∎

這就是說 $\varphi(e_G) = e_H$ ，因為前面證明過的事實 proposition-4 φ is-hom。