Mercurial > hg > Members > kono > Proof > category

changeset 218:749a1ecbc0b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add equalizers
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2013 14:51:36 +0900
parents 306f07bece85
children 2ae029454fb6
files equalizer.agda
diffstat 1 files changed, 83 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Wed Sep 04 12:13:27 2013 +0900
+++ b/equalizer.agda	Wed Sep 04 14:51:36 2013 +0900
@@ -56,14 +56,17 @@
 
 --           e eqa f g        f
 --         c ----------> a ------->b
---           ---> d ---> 
---            i      h
+--         ^ ---> d ---> 
+--         |  i      h
+--        j|    k' (d' → d)
+--         |    k  (d' → a)
+--         d'            
 
-equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) 
-           → A [ A [ h  o i ]  ≈ e eqa ]
+equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) → (h-1 : Hom A a d ) 
+           → A [ A [ h  o i ]  ≈ e eqa ] → A [ A [ h-1  o h ]  ≈ id1 A d ]
            → Equalizer A {c} (A [ f o h ])  (A [ g o h ] ) 
-equalizer+h  {a} {b} {c} {d} {f} {g} eqa i h eq =  record {
-      e = i  ;       -- Hom A a d
+equalizer+h  {a} {b} {c} {d} {f} {g} eqa i h h-1 eq h-1-id =  record {
+      e = i  ; -- A [ h-1 o e eqa ]  ;       -- Hom A a d
       ef=eg = ef=eg1 ;
       k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
       ek=h = ek=h1 ; 
@@ -97,13 +100,29 @@
              ≈⟨ assoc ⟩
                    ( g o h ) o i
              ∎
-      ek=h1 :  {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} →
-                A [ A [ i o k eqa (A [ h o h' ]) (fhj=ghj h' eq') ] ≈ h' ]
-      ek=h1 {d'} {h'} {eq'} = let open ≈-Reasoning (A) in
+      ek=h1 :  {d' : Obj A} {k' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} →
+                A [ A [ i o k eqa (A [ h o k' ]) (fhj=ghj k' eq') ] ≈ k' ]
+      ek=h1 {d'} {k'} {eq'} = let open ≈-Reasoning (A) in
              begin
-                   i o k eqa (h o h' ) (fhj=ghj h' eq')
-             ≈⟨ {!!}   ⟩
-                   h'
+                   i o k eqa (h o k' ) (fhj=ghj k' eq') --    h-1 (h o i ) o k eqa (h o k' ) = h-1 (h o k')
+             ≈↑⟨ idL  ⟩
+                   (id1 A d ) o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) 
+             ≈↑⟨ car h-1-id ⟩
+                   ( h-1 o h ) o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) 
+             ≈↑⟨ assoc  ⟩
+                    h-1 o ( h  o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) )
+             ≈⟨ cdr assoc  ⟩
+                    h-1 o ( (h  o  i ) o k eqa (h o k' ) (fhj=ghj k' eq'))
+             ≈⟨ cdr (car eq ) ⟩
+                    h-1 o ( (e eqa) o k eqa (h o k' ) (fhj=ghj k' eq'))
+             ≈⟨ cdr (ek=h eqa)  ⟩
+                    h-1 o ( h  o k' )
+             ≈⟨ assoc  ⟩
+                    ( h-1 o  h ) o k' 
+             ≈⟨ car h-1-id ⟩
+                    id1 A d o k' 
+             ≈⟨ idL ⟩
+                   k'
              ∎
       uniqueness1 :  {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} {k' : Hom A d' c} →
                 A [ A [ i o k' ] ≈ h' ] → A [ k eqa (A [ h o h' ]) (fhj=ghj h' eq') ≈ k' ]
@@ -122,6 +141,58 @@
                    k'
              ∎
 
+h+equalizer : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (h : Hom A b d ) 
+           → (h-1 : Hom A d b ) → A [ A [ h-1  o h ]  ≈ id1 A b ]
+           → Equalizer A {c} (A [ h o f ])  (A [ h o g ] ) 
+h+equalizer  {a} {b} {c} {d} {f} {g} eqa h h-1 h-1-id =  record {
+      e = e eqa  ;   
+      ef=eg = ef=eg1 ; 
+      k = λ j eq' → k eqa j (fj=gj j eq') ;
+      ek=h = ek=h1 ; 
+      uniqueness = uniqueness1
+   }  where
+      fj=gj : {e : Obj A} → (j : Hom A e a ) →  A [ A [ A [ h o f ] o  j ] ≈ A [ A [ h o g ] o j ] ] →  A [ A [ f o j ] ≈ A [ g o j ] ]
+      fj=gj j eq  = let open ≈-Reasoning (A) in
+             begin
+                f o j
+             ≈↑⟨ idL ⟩
+                id1 A b  o ( f o j )
+             ≈↑⟨ car h-1-id  ⟩
+                (h-1 o h )  o ( f o j )
+             ≈↑⟨ assoc  ⟩
+                h-1 o (h  o ( f o j ))
+             ≈⟨ cdr assoc  ⟩
+                h-1 o ((h  o  f) o j )
+             ≈⟨ cdr eq ⟩
+                h-1 o ((h  o  g) o j )
+             ≈↑⟨ cdr assoc  ⟩
+                h-1 o (h  o ( g o j ))
+             ≈⟨ assoc ⟩
+                (h-1 o h)  o ( g o j )
+             ≈⟨ car h-1-id  ⟩
+                id1 A b  o ( g o j )
+             ≈⟨ idL ⟩
+                g o j
+             ∎
+      ef=eg1 :  A [ A [ A [ h o f ] o e eqa ] ≈ A [ A [ h o g ] o e eqa ] ]
+      ef=eg1 =  let open ≈-Reasoning (A) in
+             begin
+                ( h o f ) o e eqa
+             ≈↑⟨ assoc  ⟩
+                h o (f  o e eqa )
+             ≈⟨ cdr (ef=eg eqa)  ⟩
+                h o (g  o e eqa )
+             ≈⟨ assoc ⟩
+                ( h o g ) o e eqa 
+             ∎
+      ek=h1 :   {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} →
+        A [ A [ e eqa o k eqa j (fj=gj j eq) ] ≈ j ]
+      ek=h1 {d₁} {j} {eq}  = ek=h eqa
+      uniqueness1 : {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} {k' : Hom A d₁ c} →
+        A [ A [ e eqa o k' ] ≈ j ] → A [ k eqa j (fj=gj j eq) ≈ k' ]
+      uniqueness1 = uniqueness eqa
+      
+
 lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b)  → 
          ( {a b c : Obj A} → (f g : Hom A a b)  → Equalizer A {c} f g ) → EqEqualizer A {c} f g
 lemma-equ1  A {a} {b} {c} f g eqa = record {