Mercurial > hg > Members > kono > Proof > category

changeset 250:a1e2228c2a6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer iso done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 15:56:34 +0900
parents bdeed843f8b1
children 40947f08bab6
files equalizer.agda
diffstat 1 files changed, 37 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 09 14:03:44 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 15:56:34 2013 +0900
@@ -150,7 +150,6 @@
 --     e' = h   o e
 --     e  = h'  o e'
 
-
 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } →  {e : Hom A c a } { e' : Hom A c' a }
        ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
       →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
@@ -174,7 +173,40 @@
      --                                           h =   j e f   -> j = j'
      --
 
---  e = c-iso-l o e' is assumed by equalizer's degree of freedom
+c-iso→' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
+      →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
+      →  A [ A [ e' o c-iso-l eqa eqa' keqa ]  ≈ e ]
+c-iso→' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
+                 e' o c-iso-l eqa eqa' keqa 
+              ≈⟨⟩
+                 e'  o k eqa' e (fe=ge eqa)
+              ≈⟨⟩
+                 equalizer eqa'  o k eqa' e (fe=ge eqa)
+              ≈⟨ ek=h eqa' ⟩
+                 e
+              ∎
+
+c-iso←' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
+      →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
+      →  A [ A [ e o c-iso-r eqa eqa' keqa ]  ≈ e' ]
+c-iso←' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
+                 e o c-iso-r eqa eqa' keqa 
+              ≈⟨⟩
+                 e  o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
+              ≈↑⟨ car  (ek=h eqa' ) ⟩
+                 ( equalizer eqa'  o k eqa' e (fe=ge eqa) ) o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
+              ≈⟨⟩
+                 ( e'  o k eqa' e (fe=ge eqa) ) o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
+              ≈↑⟨ assoc ⟩
+                 e'  o (( k eqa' e (fe=ge eqa) ) o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) )
+              ≈⟨⟩
+                 e'  o (equalizer keqa  o  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) )
+              ≈⟨ cdr ( ek=h keqa )  ⟩
+                 e'  o id1 A c'
+              ≈⟨ idR ⟩
+                 e'
+              ∎
+
 c-iso→ : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
       →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       →  A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ]  ≈ id1 A c' ]
@@ -189,10 +221,8 @@
 c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
       →  ( keqa :  Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ])  (A [ g o e' ]) )
       →  ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ])   (A [ g o e ]) )
-      --  e' = c-iso-r o e is assumed by equalizer's degree of freedom
-      →  { e'->e : A [ e'  ≈  A [ e  o equalizer keqa' ] ] } -- implicit assumption , which should be refl
       →  A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ]  ≈ id1 A c ]
-c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin
+c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa'  = let open ≈-Reasoning (A) in begin
                  c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa
               ≈⟨⟩
                  k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa )
@@ -202,7 +232,7 @@
                      k eqa' e (fe=ge eqa )
                    ≈⟨ uniqueness eqa' ( begin
                        e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
-                   ≈⟨ car e'->e ⟩
+                   ≈↑⟨ car (c-iso←' eqa eqa' keqa ) ⟩
                         ( e  o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
                    ≈↑⟨ assoc ⟩
                          e  o ( equalizer keqa'  o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)))
@@ -213,8 +243,7 @@
                    ∎ )⟩
                      k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) )
               ∎ )⟩
-                 equalizer keqa'  o k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) )
-              ≈⟨ ek=h keqa' ⟩
+                 equalizer keqa'  o k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) ≈⟨ ek=h keqa' ⟩
                  id1 A c
               ∎