[Agda] equality on Integer

[Serge D. Mechveliani]

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

-------------------------------------------------     
module Data.Integer.Addition.Properties
...
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