# [Agda] equality on Integer

Serge D. Mechveliani mechvel at botik.ru
Fri Aug 10 14:13:39 CEST 2012

```People,
I have a beginner question on  Agda + standard library (lib-0.6).

(I copy the math symbols, but under the  mutt  email program on a
certain distant machine, I see them as pseudo-graphic. I hope that
you will still see them correctly. But somewhere I write the comments
\Integer, \dashTriple  and such
).

I am looking at the definitions

-------------------------------------------------
...
open Algebra.FunctionProperties (_Б┴║_ {A = Б└╓})  -- \dashTriple \Integer
...
commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
{ Carrier             = Б└╓         -- \Integer
; _Б┴┬_                 = _Б┴║_     -- \tildaPair = \dashTriple
; _Б┬≥_                 = _+_
; н╣                   = + 0
; isCommutativeMonoid = isCommutativeMonoid
}
-------------------------------------------------

and trying to find:  what is this  _Б┴║_  (\dashTriple)
(a kind of an identity relation).

First, what is its intended meaning?
I suspect that it is
the literal equality on the set of representations of integer values
(because  `data \Integer'  defines the constructors for an unique
representation of an integer).
Is it?

Further, I am trying to trace this import of _Б┴║_ (\dashTriple).
The module
Algebra.FunctionProperties

has explicit parameters called  _Б┴┬_ (\tildaPair) and  A.
The import
open Algebra.FunctionProperties (_Б┴║_ {A = Б└╓})

says that the relation  _Б┴║_  (\dashTriple) is instantiated here for
these parameters with setting  \Integer  for  A.
But where this  _Б┴║_  (\dashTriple) comes from?

Digression on the export syntax: --------------------
Haskell  has the syntax of    module Foo (T(), f1, f2)  where ...

which means that _only_ the items  T(), f1, f2  are exported
(and the instances for T()).
If  Agda  had,  and the libraries used such an export construct,
would not it be easier to read and find the import trace?
Because in this case one can look only at the export part and skip the
rest module source. The Haskell library uses this approach, and this
helps a lot to understand the source.
-----------------------------------------------------

Let us continue the investigation:
module Relation.Binary.Core
has the part
---------------------
private
module Dummy where
infix 4 _Б┴║_ _Б┴╒_  -- \dashTriple ...
data _Б┴║_ {a} {A : Set a} (x : A) : A -> Set a where
-- \dashTriple
refl : x Б┴║ x
...
...
open Dummy public
---------------------

`Б┴║' (\dashTriple)  is under `private'. But it follows
`open Dummy public'
in the end.
Probably, this `open' still exports the relation domain  \dashTriple from
Relation.Binary.Core  -- even though its submodule is called Dummy.
Is this so?
So I suspect, that  Data.Integer.Addition.Properties  uses `Б┴║'
(\dashTriple) from  Relation.Binary.Core  with  A = \Integer.
Now, all this means that the field  `_Б┴┬_ = _Б┴║_'
(\tildaPair = \dashTriple)  in the above  commutativeMonoid
sets a fixed equivalence relation  \tildaPair  on  \Integer  as
denoting exactly all the pairs  (x, x),  where  x  is any representation
of a value in \Integer.
Is this so?

Thank you in advance for explanation,

-------
Sergei
```