Mercurial > hg > Members > kono > Proof > category

changeset 211:8c738327df19

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
b3
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 02 Sep 2013 23:18:40 +0900
parents 51c57efe89b9
children 8b3d3f69b725
files equalizer.agda
diffstat 1 files changed, 20 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 02 22:21:51 2013 +0900
+++ b/equalizer.agda	Mon Sep 02 23:18:40 2013 +0900
@@ -15,7 +15,6 @@
 
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
-open import Category.Sets
 module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
 
 open import HomReasoning
@@ -36,10 +35,10 @@
    field
       α : (f : Hom A a b) → (g : Hom A a b ) →  Hom A c a
 --      γ : {d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c e 
---      δ : {a b : Obj A}  → (f : Hom A a b) → Hom A a c 
+      δ : (f : Hom A a b) → Hom A a c 
       b1 : {e : Obj A } →  A [ A [ f  o α  f g ] ≈ A [ g  o α f g ] ]
 --      b2 :  {e d : Obj A } → {h : Hom A d a } → A [ A [ α {e} f g o γ f g h ] ≈ A [ h  o α {c} (A [ f o h ]) (A [ g o h ]) ] ]
---      b3 :  {e : Obj A} → A [ A [ α f f o δ f ] ≈ id1 A a ]
+      b3 :  {e : Obj A} → A [ A [ α f f o δ 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 [ γ f g ( A [ α f g o  k ] ) o δ (A [ f o A [ α f g o  k ] ] ) ] ≈ k ]
    --  A [ α f g o β f g h ] ≈ h
@@ -49,13 +48,25 @@
 open Equalizer
 open EqEqualizer
 
-lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b c : Obj A} (f g : Hom A a b)  → Equalizer A {c} f g → EqEqualizer A {c} f g
+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
 lemma-equ1  A {a} {b} {c} f g eqa = record {
-      α = λ f g →  e eqa ; -- Hom A c  a
+      α = λ f g →  e (eqa f g ) ; -- Hom A c  a
 --      γ = λ {d} {e} {a} {b} f g h → {!!} ;  -- Hom A c e
---      δ =  λ {a} {b} f → {!!} ; -- Hom A a c
-      b1 = ef=eg eqa -- ;
+      δ =  λ f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
+      b1 = ef=eg (eqa f g) ;
 --      b2 = {!!} ;
---      b3 = {!!} ;
+      b3 = lemma-equ3 -- ;
 --      b4 = {!!} 
- }
+ } where
+     lemma-equ2 : {a b : Obj A} (f : Hom A a b)  → A [ A [ f o id1 A a ]  ≈ A [ f o id1 A a ] ]
+     lemma-equ2 f =   let open ≈-Reasoning (A) in refl-hom
+     lemma-equ3 : {e' : Obj A} → A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
+     lemma-equ3 {e'} = let open ≈-Reasoning (A) in
+             begin  
+                  e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
+             ≈⟨ ke=h (eqa f f ) (lemma-equ2 f) ⟩
+                  id1 A a
+             ∎
+
+