Mercurial > hg > Members > kono > Proof > category

changeset 236:e20b81102eee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Burroni equational equalizer definition done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 08 Sep 2013 05:54:27 +0900
parents 8835015a3e1a
children 776cda2286c8
files equalizer.agda
diffstat 1 files changed, 26 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sun Sep 08 04:55:01 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 05:54:27 2013 +0900
@@ -33,19 +33,20 @@
 --
 -- Flat Equational Definition of Equalizer
 --
-record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
-      α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  Hom A c a
+      α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  {e : Hom A c a } → Hom A c a
       γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A d c
-      δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c
-      b1 : A [ A [ f  o α {a} {b} {a}  f g ] ≈ A [ g  o α f g ] ]
-      b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g) o (γ {a} {b} {c} f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) ] ]
-      b3 :  A [ A [ α f f o δ {a} {b} {a} f ] ≈ id1 A a ]
+      δ : {a b c : Obj A } → {e : Hom A c a } → (f : Hom A a b) → Hom A a c
+      b1 : A [ A [ f  o α {a} {b} {a}  f g {id1 A a} ] ≈ A [ g  o α {a} {b} {a} f g {id1 A a} ] ]
+      b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g {e} ) o (γ {a} {b} {c} f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]){id1 A d} ] ]
+      b3 :  A [ A [ α {a} {b} {a} f f {id1 A a} o δ {a} {b} {a} {id1 A a} f ] ≈ id1 A a ]
       -- b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
-      b4 :  {d : Obj A } {k : Hom A d c} → A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g o k ] ) o δ (A [ f o A [ α f g o  k ] ] ) ] ≈ k ]
+      b4 :  {d : Obj A } {k : Hom A d c} → 
+           A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g {e} o k ] ) o ( δ {d} {b} {d} {id1 A d} (A [ f o A [ α {a} {b} {c} f g {e} o  k ] ] )  )] ≈ k ]
    --  A [ α f g o β f g h ] ≈ h
    β : { d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A d c
-   β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ]
+   β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ {d} {b} {d} {id1 A d} (A [ f o h ]) ]
 
 open Equalizer
 open Burroni
@@ -219,14 +220,14 @@
 --    b4 is not yet done
 ----
 
-lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  →
-         ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a } { fe=ge1 : A [ A [ f o e ] ≈ A [ g o e ] ] } → Equalizer A e f g ) 
-              → Burroni A {c} f g
-lemma-equ1  {a} {b} {c} f g eqa = record {
-      α = λ f g →  equalizer (eqa f g ) ; -- Hom A c a
+lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) →
+         ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g ) 
+              → Burroni A {c} {a} {b} f g e
+lemma-equ1  {a} {b} {c} f g e eqa  = record {
+      α = λ {a} {b} {c}  f g {e}  →  equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
       γ = λ {a} {b} {c} {d} f g h → 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 ) ;  -- Hom A c d
-      δ =  λ {a} f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
-      b1 = fe=ge (eqa f g) ;
+      δ =  λ {a} {b} {c} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f); -- Hom A a c
+      b1 = fe=ge (eqa {a} {b} {a} f g {id1 A a}) ;
       b2 = lemma-b2 ;
       b3 = lemma-b3 ;
       b4 = lemma-b4
@@ -282,29 +283,32 @@
      -------                    α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j)       =                  α(f,g)j
      -------                           γ(f,g,α(f,g)j) δ(fα(f,g)j)       =                        j
 
-     eefg : {a b c : Obj A} (f g : Hom A a b) {e : Hom A c a} →  Equalizer A e ( A [ f  o  equalizer (eqa f g) ]  ) (A [ g  o  equalizer (eqa f g) ] ) 
+     eefg : {a b c : Obj A} (f g : Hom A a b) {e : Hom A c a} →  Equalizer A e ( A [ f o  equalizer (eqa f g {id1 A a}) ] ) (A [ g  o  equalizer (eqa f g {id1 A a}) ] ) 
      eefg f g {e} = eqa  ( A [ f  o  equalizer (eqa f g) ]  ) (A [ g  o  equalizer (eqa f g) ] ) 
      lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
-          A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) ])
+              A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o 
+                 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
                      (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
               k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
               ≈ j ]
      lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
              begin
-                     ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g) o j ) )) (( g o ( equalizer (eqa f g) o j ) ))) ))
+                ( k (eqa f g) (( ( 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 ) ))) ))
                             (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o 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 ) ))) )
+                   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 ) ))) )
              ≈⟨ car ((uniqueness (eqa f g) ( begin
                          equalizer (eqa f g) o j 
                 ≈↑⟨ idR  ⟩
                          (equalizer (eqa f g) o j )  o id1 A d
                 ≈⟨⟩
-                        ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g) o j) (g o equalizer (eqa f g) o j)))
+                        ((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 ) ))) 
              ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin
-                     equalizer (eqa (f o equalizer (eqa f g) o j) (f o equalizer (eqa f g) o j))
-                ≈⟨ {!!} ⟩
+                     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))  
+                ≈⟨⟩
                     id1 A d
              ∎ ))) ⟩
                     j o id1 A d