How to declare axioms in Agda?

Question

I was reading the book "Algebra driven design" and in the second chapter it starts designing a simple algebra system like this:

data Tile

haskell :: Tile
sandy :: Tile

cw :: Tile -> Tile

∀ (t :: Tile).
  cw (cw (cw (cw t))) = t

and it starts building up from there. So I thought it would be nice if I could use a proof assistant to follow along.

I saw someone do this with Coq here and I thought surely it's possible to do in Agda too, but I don't know how to define an axiom like it is defined in the Coq example (Axiom cw : Tile -> Tile.).

Keep in mind that I'm not interested in actually implementing the functions here, I just need to do algebra based on some axioms.

Answer 1

The Agda equivalent of Axiom is postulate, which should work basically the same way.