Mercurial > hg > Members > kono > Proof > category

changeset 957:e29b6488b179

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
b4
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Feb 2021 12:57:05 +0900
parents 468288f3dfe5
children 9089540fe89d
files src/equalizer.agda
diffstat 1 files changed, 27 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/equalizer.agda	Sun Feb 21 10:26:00 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 12:57:05 2021 +0900
@@ -297,21 +297,35 @@
                      (lemma-equ4 {a} {b} {d} f g (A [ equalizer (eqa f g) o j ])) 
                  o    k (ieqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) (id1 A _)
                      (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))] ≈ j ]
-     lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
+     --   h = equalizer (eqa f g) o j 
+     lemma-b4 {d} {j} = 
              begin
-                 k (ieqa 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 ) ))) ))
-                            (lemma-equ4 {a} {b} {d} f g (( equalizer (eqa f g) o j )))
-                 o    k (ieqa (f o ( equalizer (eqa f g) o j )) ( g o (equalizer (eqa f g) o j ))) (id1 A _)
-                     (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
-             ≈⟨ car (uniqueness (ieqa f g) {!!}) ⟩
-                 {!!} o {!!}
-             ≈⟨ cdr (uniqueness (ieqa (f o ( equalizer (eqa f g) o j )) ( g o (equalizer (eqa f g) o j ))) {!!}) ⟩
-                 {!!} o {!!}
-             ≈⟨ {!!} ⟩
+                 k (ieqa f g) (( h o equalizer (eqa (( f o h )) (( g o h ))) )) (lemma-equ4 {a} {b} {d} f g (h))
+                 o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+             ≈↑⟨ uniqueness (ieqa f g) ( begin
+                  equalizer (eqa f g) o ( k (ieqa f g) (( h o equalizer (eqa ( f o h ) ( g o h )) )) (lemma-equ4 {a} {b} {d} f g h)
+                   o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _)) )
+                ≈⟨ assoc ⟩
+                 (equalizer (eqa f g) o ( k (ieqa f g) (( h o equalizer (eqa ( f o h ) ( g o h )) )) (lemma-equ4 {a} {b} {d} f g h)))
+                   o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+                ≈⟨ car (ek=h (ieqa f g) ) ⟩
+                 (( h o equalizer (eqa ( f o h ) ( g o h )) ))
+                   o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+                ≈↑⟨ assoc ⟩
+                 h o (equalizer (eqa ( f o h ) ( g o h )) o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _)))
+                ≈⟨ cdr (ek=h  (ieqa (f o h) ( g o h))) ⟩
+                 h o id1 A _
+                ≈⟨ idR ⟩
+                 h
+                ∎ 
+             ) ⟩
+                 k (ieqa f g) h (f1=gh (fe=ge (ieqa f g)) )
+             ≈⟨ uniqueness (ieqa f g) refl-hom ⟩
                  j
-             ∎ 
-
-
+             ∎  where
+               open ≈-Reasoning A
+               h : Hom A d a
+               h = equalizer (eqa f g) o j
 
 
 --------------------------------