Mercurial > hg > Members > kono > Proof > category

changeset 243:40ac16f69708

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 18:24:49 +0900
parents 5d1ecfec6f41
children d9317fe71ed6
files equalizer.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sun Sep 08 17:47:04 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 18:24:49 2013 +0900
@@ -41,9 +41,8 @@
       cong-α : {a b c :  Obj A } → { e : Hom A c a }
           → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ α f g {e} ≈ α f g' {e} ] 
       cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] 
-         →  { γ γ' :  {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A d c }
-         → A [ γ f g h ≈ γ' f g h' ] 
-      cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ] 
+         → A [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ] 
+      cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ δ f ≈ δ f' ] 
       b1 : A [ A [ f  o α {a} {b} {c}  f g {e} ] ≈ A [ g  o α {a} {b} {c} f g {e} ] ]
       b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g {e} ) o (γ {a} {b} {c} f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]){id1 A d} ] ]
       b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f {h} o δ {a} {b} {d} {h} f ] ≈ id1 A a ]
@@ -324,7 +323,8 @@
                      A [  k (eqa f g ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 
                        ≈  k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )  ]
      cong-γ1 = {!!} 
-     cong-δ1 :  {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ]
+     cong-δ1 :  {e : Hom A c a} {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f)  ≈ 
+                                                                            k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (lemma-equ2 f') ]
      cong-δ1 =  {!!}