如何在Agda中声明公理?

Question

我在读《代数驱动设计》这本书;第二章开始设计一个简单的代数系统，如下:

data Tile
haskell :: Tile
sandy :: Tile
cw :: Tile -> Tile
∀ (t :: Tile).
cw (cw (cw (cw t))) = t

然后它就开始形成了。所以我想如果我能有一个校对助手来跟进的话会很好。

我看到有人在这里用Coq这样做，我想肯定在Agda中也可以这样做，但我不知道如何定义一个公理，就像它在Coq示例(Axiom cw : Tile -> Tile.)中定义的那样。

请记住，我对实际实现这里的函数不感兴趣，我只需要基于一些公理做代数。

Answer 1

Axiom的Agda等效是postulate，其工作原理基本相同。