[Agda] how to run and test the basic function in agda

[Mandy Martino]

after googled  mazzo.li – blag – Agda by Example_ Sorting.html
is there  a complete  example about  which  library  should be imported,
and how to test the  basic  function below ?
i am  research the usage  of  many other combination of  equivalence relations using fst and snd.
Rel : Set → Set₁Rel X = X → X → Set
Decidable : ∀ {X} → Rel X → SetDecidable R = ∀ x y → Either (R x y) (¬ (R x y))
record Equivalence {X} (_≈_ : Rel X) : Set₁ where  field    refl  : ∀ {x}     → x ≈ x    sym   : ∀ {x y}   → x ≈ y → y ≈ x    trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

Regards,
Martin  		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151208/7558945e/attachment.html