<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font color="#000000"><div><div>after googled mazzo.li – blag – Agda by Example_ Sorting.html</div><div><br></div><div>is there a complete example about which library should be imported,</div><div><br></div><div>and how to test the basic function below ?</div><div><br></div><div>i am research the usage of many other combination of equivalence relations using fst and snd.</div><div><br></div><div>Rel : Set → Set₁</div><div>Rel X = X → X → Set</div></div><div><br></div><div><div>Decidable : ∀ {X} → Rel X → Set</div><div>Decidable R = ∀ x y → Either (R x y) (¬ (R x y))</div></div><div><br></div><div>record Equivalence {X} (_≈_ : Rel X) : Set₁ where</div><div> field</div><div> refl : ∀ {x} → x ≈ x</div><div> sym : ∀ {x y} → x ≈ y → y ≈ x</div><div> trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z</div></font><br><br><div>Regards,</div><div><br></div><div>Martin </div> </div></body>
</html>