<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><div>Hi,</div><div><br></div><div><div>No binding for builtin thing IO, use {-# BUILTIN IO name #-} to</div><div>bind it to 'name'</div></div><div><br></div><div>module PropositionalEquality where</div><div><br></div><div>data Empty : Set where</div><div>absurd : {X : Set} → Empty → X</div><div>absurd ()</div><div><br></div><div>infix 3 ¬_</div><div>¬_ : Set → Set</div><div>¬ X = X → Empty</div><div><br></div><div>Rel : Set → Set₁</div><div>Rel X = X → X → Set</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><div><br></div><div>data _≡_ {X} : Rel X where</div><div> refl : ∀ {x} → x ≡ x</div><div><br></div><div>sym : ∀ {X} {x y : X} → x ≡ y → y ≡ x</div><div>sym refl = refl</div><div><br></div><div>trans : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ z</div><div>trans refl refl = refl</div><div><br></div><div>equivalence : ∀ {X} → Equivalence {X} _≡_</div><div>equivalence = record { refl = refl; sym = sym; trans = trans }</div><div><br></div><div>cong : ∀ {X} {x y : X} → (f : X → X) → x ≡ y → f x ≡ f y</div><div>cong _ refl = refl</div><div><br></div><div>main = Empty</div><div><br></div><div>Regards,</div><div><br></div><div>Martin</div> </div></body>
</html>