1. 17
    1. 3

      Hey, thanks for posting! I’m the author of the article and would be happy to answer any questions.

      1. 1

        As someone who hasn’t touched Agda, what does an “instance” of this look like in practice? Wondering in particular about those equational relations

        1. 1

          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.