Mercurial > hg > Papers > 2015 > atton-osc
changeset 12:dfa919e8fb20
Fix definition sym
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 May 2014 10:41:20 +0900 |
| parents | 9876354c1c19 |
| children | 37a7b8c31a0c |
| files | slide.html slide.md |
| diffstat | 2 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- 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} -> x ≡ y -> y ≡ x</li> <li>cong : {A B : Set} {x y : A} -> (f : A -> B) -> x ≡ y -> f x ≡ f y</li> <li> <p>trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z</p>
--- 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