Mercurial > hg > Members > kono > Proof > category

changeset 244:d9317fe71ed6

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 Mon, 09 Sep 2013 10:22:09 +0900
parents 40ac16f69708
children 0d1f7bbea9bc
files equalizer.agda
diffstat 1 files changed, 4 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sun Sep 08 18:24:49 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 10:22:09 2013 +0900
@@ -237,7 +237,7 @@
       δ =  λ {a} {b} {c} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f); -- Hom A a c
       cong-α = cong-α1 ;
       cong-γ = cong-γ1 ;
-      cong-δ = cong-δ1  ;
+      cong-δ = λ {a b c f f'} f=f' → cong-δ1 {a} {b} {c} {f} {f'} f=f'  ;
       b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
       b2 = lemma-b2 ;
       b3 = lemma-b3 ;
@@ -323,7 +323,9 @@
                      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 :  {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)  ≈ 
+--  {a₁ b₁ c₃ : Obj A} {f₁ f' : Hom A a₁ b₁} → A [ f₁ ≈ f' ] →
+--     A [ k (eqa f₁ f₁) (id1 A a₁) (lemma-equ2 f₁) ≈ k (eqa f' f') (id1 A a₁) (lemma-equ2 f') ]
+     cong-δ1 : {a b c : Obj A} {f f' : Hom A a b} → A [ f ≈ f' ] →  { e : Hom A c a } → 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 =  {!!}