changeset 513:e73c3e73a87b

on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Mar 2017 09:38:57 +0900
parents f19dab948e39
children 1fca61019bdf
files SetsCompleteness.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Mar 20 12:50:21 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 09:38:57 2017 +0900
@@ -122,14 +122,22 @@
            ek=h {d} {h} {eq} = refl 
            fhy=ghy : (d : Obj Sets ) ( h : Hom Sets d a ) (y : d ) →  (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ])  → f (h y) ≡ g (h y)
            fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh
+           fuga : {d : Obj Sets} { y : d } { k' : Hom Sets d (sequ a b f g)}  →  Hom Sets a {!!}
+           fuga = {!!}
            repl :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → ( y : d ) →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → k h fh=gh y ≡ k' y
            repl {d} {h} {fh=gh} {k'} y ek'=h = 
               begin
                  k h fh=gh y
               ≡⟨⟩
-                  elem  (h y) (fhy=ghy d h y fh=gh )
-              ≡⟨ ? ⟩
+                 elem  (h y) (fhy=ghy d h y fh=gh )
+              ≡⟨ {!!} ⟩
+                 fuga (h y )
+              ≡⟨ sym ( Category.cong (λ f → fuga (f y ) ) ek'=h )  ⟩
+                 fuga ( ( λ e → equ e ) ( k' y ) )
+              ≡⟨⟩
+                 ( λ e → fuga ( equ e )) ( k' y ) 
+              ≡⟨ {!!} ⟩
                  k' y

               where