The pattern crops up everywhere in the Agda standard library. Here’s one example: IsCommutativeMagma (a magma is just a type with a binary operation). In Agda all the definitions are in terms of other definitions, so it’s less obvious, but Commutative ∙ unfolds to:
∀ x y → (x ∙ y) ≈ (y ∙ x)
So there’s that equational relation. As for where this is used, it’s less obvious; one difficult aspect of the Agda standard library is that names are re-bound and re-bound again, and all that aliasing buries the references to a particular instance. However, I found a proof term that states that + on natural numbers forms a magma, called +-isMagma. I assumed this is used for various proofs about natural numbers, but finding them is a bit difficult.
Hey, thanks for posting! I’m the author of the article and would be happy to answer any questions.
As someone who hasn’t touched Agda, what does an “instance” of this look like in practice? Wondering in particular about those equational relations
The pattern crops up everywhere in the Agda standard library. Here’s one example:
IsCommutativeMagma(a magma is just a type with a binary operation). In Agda all the definitions are in terms of other definitions, so it’s less obvious, butCommutative ∙unfolds to:So there’s that equational relation. As for where this is used, it’s less obvious; one difficult aspect of the Agda standard library is that names are re-bound and re-bound again, and all that aliasing buries the references to a particular instance. However, I found a proof term that states that
+on natural numbers forms a magma, called+-isMagma. I assumed this is used for various proofs about natural numbers, but finding them is a bit difficult.