Mercurial > hg > Members > kono > Proof > category

changeset 221:ea0407fb8f02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2013 20:35:43 +0900
parents 5d96be63053f
children 0bc85361b7d0
files equalizer.agda
diffstat 1 files changed, 39 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Wed Sep 04 18:45:17 2013 +0900
+++ b/equalizer.agda	Wed Sep 04 20:35:43 2013 +0900
@@ -23,7 +23,7 @@
 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
       e : Hom A c a 
-      ef=eg : A [ A [ f o e ] ≈ A [ g o e ] ]
+      fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
       k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
       ek=h : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  A [ A [ e  o k {d} h eq ] ≈ h ]
       uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  {k' : Hom A d c } → 
@@ -48,30 +48,6 @@
 open Equalizer
 open EqEqualizer
 
--- Equalizer is unique up to iso
-
-equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
-      → Hom A c c'   --- != id1 A c
-equalizer-iso  {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa)
-
-equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) → {eff : Equalizer A {c} f f} 
-      → A [ A [ equalizer-iso eqa eqa' o  equalizer-iso eqa' eqa ] ≈  id1 A c' ]
-equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' {eff} =  let open ≈-Reasoning (A) in
-             begin
-                 equalizer-iso eqa eqa' o  equalizer-iso eqa' eqa 
-             ≈⟨⟩
-                 k eqa' (e eqa) (ef=eg eqa)  o k eqa (e eqa') (ef=eg eqa')
-             ≈⟨ car (uniqueness eqa' {!!}) ⟩
-                 {!!} o k eqa (e eqa') (ef=eg eqa')
-             ≈⟨ {!!} ⟩
-                 id1 A c'
-             ∎
-
--- ke = e' k'e' = e  → k k' = 1 , k' k = 1
---     ke  = e'
---     k'ke  = k'e' = e   kk' = 1
-
---     x e = e -> x = id?
 
 f1=g1 : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → A [ A [ f o id1 A a ] ≈ A [ g o id1 A a ]  ]
 f1=g1 eq = let open ≈-Reasoning (A) in (resp refl-hom eq )
@@ -106,7 +82,7 @@
            → Equalizer A {c} (A [ f o h ])  (A [ g o h ] ) 
 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 ;
+      fe=ge = fe=ge1 ;
       k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
       ek=h = ek=h1 ; 
       uniqueness = uniqueness1
@@ -124,15 +100,15 @@
              ≈↑⟨ assoc ⟩
                   g o ( h  o j )
              ∎
-      ef=eg1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
-      ef=eg1 = let open ≈-Reasoning (A) in 
+      fe=ge1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
+      fe=ge1 = let open ≈-Reasoning (A) in 
              begin
                    ( f o h ) o i
              ≈↑⟨ assoc  ⟩
                    f o (h  o i )
              ≈⟨ cdr eq ⟩
                    f o (e eqa)
-             ≈⟨ ef=eg eqa ⟩
+             ≈⟨ fe=ge eqa ⟩
                    g o (e eqa)
              ≈↑⟨ cdr eq ⟩
                    g o (h  o i )
@@ -185,7 +161,7 @@
            → 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 ; 
+      fe=ge = fe=ge1 ; 
       k = λ j eq' → k eqa j (fj=gj j eq') ;
       ek=h = ek=h1 ; 
       uniqueness = uniqueness1
@@ -213,13 +189,13 @@
              ≈⟨ 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
+      fe=ge1 :  A [ A [ A [ h o f ] o e eqa ] ≈ A [ A [ h o g ] o e eqa ] ]
+      fe=ge1 =  let open ≈-Reasoning (A) in
              begin
                 ( h o f ) o e eqa
              ≈↑⟨ assoc  ⟩
                 h o (f  o e eqa )
-             ≈⟨ cdr (ef=eg eqa)  ⟩
+             ≈⟨ cdr (fe=ge eqa)  ⟩
                 h o (g  o e eqa )
              ≈⟨ assoc ⟩
                 ( h o g ) o e eqa 
@@ -235,7 +211,7 @@
            → Equalizer A {c} (A [ f o e eqa ])  (A [ g o e eqa ] ) 
 eefeg {a} {b} {c} {d} {f} {g} eqa =  record {
       e = id1 A c ; -- i  ; -- A [ h-1 o e eqa ]  ;       -- Hom A a d
-      ef=eg = ef=eg1 ;
+      fe=ge = fe=ge1 ;
       k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
       ek=h = ek=h1 ; 
       uniqueness = uniqueness1
@@ -255,11 +231,11 @@
              ≈↑⟨ assoc ⟩
                   g o ( h  o j )
              ∎
-      ef=eg1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
-      ef=eg1 = let open ≈-Reasoning (A) in 
+      fe=ge1 :  A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
+      fe=ge1 = let open ≈-Reasoning (A) in 
              begin
                    ( f o h ) o i
-             ≈⟨ car ( ef=eg eqa ) ⟩
+             ≈⟨ car ( fe=ge eqa ) ⟩
                    ( g o h ) o i
              ∎
       ek=h1 :  {d' : Obj A} {k' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} →
@@ -287,8 +263,31 @@
                    k'
              ∎
 
-      
+-- Equalizer is unique up to iso
+
+equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      → Hom A c c'   --- != id1 A c
+equalizer-iso  {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa)
 
+--
+--        
+--           e eqa f g        f
+--         c ----------> a ------->b
+--
+equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      → A [ A [ equalizer-iso eqa eqa' o   equalizer-iso eqa' eqa ] ≈  id1 A c' ]
+equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' =  let open ≈-Reasoning (A) in
+             begin
+                  k eqa' (e eqa) (fe=ge eqa)  o  k eqa (e eqa' ) (fe=ge eqa' )
+             ≈⟨ {!!} ⟩
+                 id1 A c'
+             ∎
+
+-- ke = e' k'e' = e  → k k' = 1 , k' k = 1
+--     ke  = e'
+--     k'ke  = k'e' = e   kk' = 1
+
+--     x e = e -> x = id?
 
 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
@@ -296,7 +295,7 @@
       α = λ f g →  e (eqa f g ) ; -- Hom A c a
       γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
       δ =  λ {a} f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
-      b1 = ef=eg (eqa f g) ;
+      b1 = fe=ge (eqa f g) ;
       b2 = lemma-equ5 ;
       b3 = lemma-equ3 ;
       b4 = lemma-equ6 
@@ -329,7 +328,7 @@
                    f o ( h o e (eqa (f o h) ( g o h )))
              ≈⟨ assoc ⟩
                    (f o h) o e (eqa (f o h) ( g o h ))
-             ≈⟨ ef=eg (eqa (A [ f o h ]) (A [ g o h ])) ⟩
+             ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩
                    (g o h) o e (eqa (f o h) ( g o h ))
              ≈↑⟨ assoc ⟩
                    g o ( h o e (eqa (f o h) ( g o h )))