Mercurial > hg > Members > kono > Proof > category

changeset 213:f2faee0897c7

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 Tue, 03 Sep 2013 01:25:21 +0900
parents 8b3d3f69b725
children f8afdb9ed99a
files equalizer.agda
diffstat 1 files changed, 6 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Tue Sep 03 01:11:59 2013 +0900
+++ b/equalizer.agda	Tue Sep 03 01:25:21 2013 +0900
@@ -36,11 +36,11 @@
       α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  Hom A c a
       γ : {a b d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c d
       δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c 
-      b1 : A [ A [ f  o α  f g ] ≈ A [ g  o α f g ] ]
+      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 (γ f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) ] ]
-      b3 :  {e : Obj A} → A [ A [ α f f o δ f ] ≈ id1 A a ]
+      b3 :  A [ A [ α f f o δ {a} {b} {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 [ γ f g ( A [ α f g o  k ] ) o δ (A [ f o A [ α f g o  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 ] ] ) ] ≈ {!!} ]
    --  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 a d
 --   β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {d} f g h o δ (A [ f o h ]) ] 
@@ -53,7 +53,7 @@
 lemma-equ1  A {a} {b} {c} f g eqa = record {
       α = λ f g →  e (eqa f g ) ; -- Hom A c  a
       γ = λ {a} {b} {d} f g h → ( k (eqa f g ) ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h ) ) ;  -- Hom A c d
-      δ =  λ f → k (eqa f f) (id1 A (Category.dom A f))  (lemma-equ2 f); -- Hom A a c
+      δ =  λ {a} f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
       b1 = ef=eg (eqa f g) ;
       b2 = lemma-equ5 ;
       b3 = lemma-equ3 ;
@@ -61,8 +61,8 @@
  } 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
+     lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
+     lemma-equ3 = 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) ⟩