Mercurial > hg > Members > kono > Proof > category

changeset 239:08afb6ad80c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 08 Sep 2013 06:43:20 +0900
parents c8db99cdf72a
children 964e258e08fb
files equalizer.agda
diffstat 1 files changed, 13 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sun Sep 08 06:31:01 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 06:43:20 2013 +0900
@@ -323,6 +323,16 @@
       ek=h1 {d} {h} {eq} =  let open ≈-Reasoning (A) in
              begin
                  α bur f g o k1 h eq 
+             ≈⟨⟩
+                 α bur f g o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h) )
+             ≈⟨ assoc ⟩
+                 ( α bur f g o  γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} {id1 A d} (f o h) 
+             ≈⟨ car (b2 bur) ⟩
+                  ( h o ( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) 
+             ≈↑⟨ assoc ⟩
+                   h o ((( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h)  )
+             ≈⟨ cdr {!!} ⟩
+                   h o id1 A d
              ≈⟨ {!!}  ⟩
                  h 
              ∎
@@ -331,7 +341,9 @@
       uniqueness1 {d} {h} {eq} {k'} ek=h =   let open ≈-Reasoning (A) in
              begin
                  k1 {d} h eq
-             ≈⟨ {!!}  ⟩
+             ≈⟨⟩
+                 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h)
+             ≈⟨ ? ⟩
                  k'
              ∎