Mercurial > hg > Members > kono > Proof > category

changeset 247:f6e8d6d04af8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 12:47:53 +0900
parents 80d9ef47566b
children efa2fd0e91ee
files equalizer.agda
diffstat 1 files changed, 14 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 09 12:35:56 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 12:47:53 2013 +0900
@@ -236,7 +236,7 @@
                             (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
       δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f); -- Hom A a c
       cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
-      cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a} {_} {c} {d} {f} {g} {h} {h'} eq  ;
+      cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a}  {c} {d} {f} {g} {h} {h'} eq  ;
       cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f'  ;
       b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
       b2 = lemma-b2 ;
@@ -279,10 +279,10 @@
      cong-α1 : {a b c :  Obj A } → { e : Hom A c a }
           → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ equalizer (eqa {a} {b} {c} f g {e} )≈ equalizer (eqa {a} {b} {c} f g' {e} ) ] 
      cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom 
-     cong-γ1 :  {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] →  { e : Hom A c a} →
+     cong-γ1 :  {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] →  { e : Hom A c a} →
                      A [  k (eqa f g {e} ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 
                        ≈  k (eqa f g {e} ) {d} ( A [ h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )  ]
-     cong-γ1 {a} {_} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin
+     cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin
                  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 )
              ≈⟨ uniqueness (eqa f g) ( begin
                  e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o  h)
@@ -317,7 +317,17 @@
              ∎
      cong-δ1 : {a b c : Obj A} {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 =  {!!} 
+     cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' =  let open ≈-Reasoning (A) in
+             begin
+                 k (eqa {a} {b} {c} f  f  {e} ) (id1 A a)  (lemma-equ2 f) 
+             ≈⟨  uniqueness (eqa f f) ( begin
+                 e o k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (lemma-equ2 f') 
+             ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩
+                 id1 A a
+             ∎ )⟩
+                 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (lemma-equ2 f') 
+             ∎
+
      lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
                       A [ equalizer (eqa f g) o k (eqa f g) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
                     ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ]