# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400895680 -32400
# Node ID dfa919e8fb205d7caa68d25d53a50edf340bf822
# Parent  9876354c1c1958cb0ff8f6f1aea5837cf22986ac
Fix definition sym

diff -r 9876354c1c19 -r dfa919e8fb20 slide.html
--- a/slide.html	Fri May 23 21:08:41 2014 +0900
+++ b/slide.html	Sat May 24 10:41:20 2014 +0900
@@ -43,7 +43,7 @@
 			<!-- === begin markdown block ===
 
       generated by markdown 1.1.1 on Ruby 2.1.2 (2014-05-08) [x86_64-darwin13.0]
-                on 2014-05-23 21:08:27 +0900 with Markdown engine kramdown (1.3.3)
+                on 2014-05-24 10:41:10 +0900 with Markdown engine kramdown (1.3.3)
                   using options {}
   -->
 
@@ -423,7 +423,7 @@
 <p>等しさを保ったまま変換する関数を作ると良い</p>
 
 <ul>
-  <li>sym refl = refl</li>
+  <li>sym   : {A : Set} {x y : A} -&gt; x ≡ y -&gt; y ≡ x</li>
   <li>cong  : {A B : Set} {x y : A} -&gt; (f : A -&gt; B) -&gt; x ≡ y -&gt; f x ≡ f y</li>
   <li>
     <p>trans : {A : Set} {x y z : A} -&gt; x ≡ y -&gt; y ≡ z -&gt; x ≡ z</p>
diff -r 9876354c1c19 -r dfa919e8fb20 slide.md
--- a/slide.md	Fri May 23 21:08:41 2014 +0900
+++ b/slide.md	Sat May 24 10:41:20 2014 +0900
@@ -155,7 +155,7 @@
 # 等しさを保ったままできること
 等しさを保ったまま変換する関数を作ると良い
 
-* sym refl = refl
+* sym   : {A : Set} {x y : A} -> x ≡ y -> y ≡ x
 * cong  : {A B : Set} {x y : A} -> (f : A -> B) -> x ≡ y -> f x ≡ f y
 * trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z