Mercurial > hg > Members > kono > Proof > category

changeset 238:c8db99cdf72a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Burrnoi to Equalizer problem written
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 08 Sep 2013 06:31:01 +0900
parents 776cda2286c8
children 08afb6ad80c7
files equalizer.agda
diffstat 1 files changed, 33 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sun Sep 08 05:55:56 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 06:31:01 2013 +0900
@@ -38,15 +38,15 @@
       α : {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 } → {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} ] ]
+      b1 : A [ A [ f  o α {a} {b} {c}  f g {e} ] ≈ A [ g  o α {a} {b} {c} f g {e} ] ]
       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 {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 δ {d} {b} {d} {id1 A d} (A [ f o h ]) ]
+   β : { d a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A d c
+   β {d} {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
@@ -227,7 +227,7 @@
       α = λ {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} {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}) ;
+      b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
       b2 = lemma-b2 ;
       b3 = lemma-b3 ;
       b4 = lemma-b4
@@ -307,6 +307,35 @@
              ∎ 
 
 
+lemma-equ2 : {a b c : Obj A} (f g : Hom A a b)  (e : Hom A c a )
+         → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g) f g 
+lemma-equ2 {a} {b} {c} f g e bur = record {
+      fe=ge = fe=ge1 ;  
+      k = k1 ;
+      ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ;
+      uniqueness  = λ {d} {h} {eq} {k'} ek=h → uniqueness1  {d} {h} {eq} {k'} ek=h
+   } where
+      k1 :  {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
+      k1 {d} h fh=gh = β bur {d} {a} {b} f g h
+      fe=ge1 : A [ A [ f o (α bur f g) ] ≈ A [ g o (α bur f g) ] ]
+      fe=ge1 = b1 bur
+      ek=h1 : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  A [ A [ (α bur f g)  o k1 {d} h eq ] ≈ h ]
+      ek=h1 {d} {h} {eq} =  let open ≈-Reasoning (A) in
+             begin
+                 α bur f g o k1 h eq 
+             ≈⟨ {!!}  ⟩
+                 h 
+             ∎
+      uniqueness1 : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  {k' : Hom A d c } →
+              A [ A [ (α bur f g)  o k' ] ≈ h ] → A [ k1 {d} h eq  ≈ k' ]
+      uniqueness1 {d} {h} {eq} {k'} ek=h =   let open ≈-Reasoning (A) in
+             begin
+                 k1 {d} h eq
+             ≈⟨ {!!}  ⟩
+                 k'
+             ∎
+
+
 -- end