Mercurial > hg > Members > kono > Proof > category

changeset 241:9e4dc349831e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comments
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 08 Sep 2013 12:34:35 +0900
parents 964e258e08fb
children 5d1ecfec6f41
files equalizer.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sun Sep 08 11:54:06 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 12:34:35 2013 +0900
@@ -152,12 +152,12 @@
 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' ]) )
-      → Hom A c c'
+      → Hom A c c'         --  should be e' = c-sio-l o  e
 c-iso-l  {c} {c'} eqa eqa' keqa = equalizer keqa
 
 c-iso-r : { 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' ]) )
-      →  Hom A c' c
+      →  Hom A c' c         --  e = c-sio-r o  e'
 c-iso-r  {c} {c'} eqa eqa' keqa = k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
 
      --               e'          f
@@ -172,6 +172,7 @@
      --                                           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 [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ]  ≈ id1 A c' ]
@@ -186,7 +187,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'->e : A [ e'  ≈  A [ e  o equalizer keqa' ] ] } -- refl
+      --  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-r eqa eqa' keqa o c-iso-l eqa eqa' keqa
@@ -220,7 +222,7 @@
 --
 -- An equalizer satisfies Burroni equations
 --
---    b4 is not yet done
+--    congs are not yet done
 ----
 
 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) →
@@ -302,7 +304,7 @@
                          equalizer (eqa f g) o j 
                 ≈↑⟨ idR  ⟩
                          (equalizer (eqa f g) o j )  o id1 A d
-                ≈⟨⟩
+                ≈⟨⟩         -- here we decide e (fej) (gej)' is id1 A d
                         ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j)))
              ∎ ))) ⟩
                     j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) 
@@ -310,7 +312,7 @@
                      equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j))  o id1 A d
                 ≈⟨ idR ⟩
                      equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j))  
-                ≈⟨⟩
+                ≈⟨⟩         -- here we decide e (fej) (fej)' is id1 A d
                     id1 A d
              ∎ ))) ⟩
                     j o id1 A d