Mercurial > hg > Members > kono > Proof > category

changeset 516:327dc7372729

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
yellow remains ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Mar 2017 13:42:08 +0900
parents 221dd46ded35
children 6f7630a255e4
files SetsCompleteness.agda
diffstat 1 files changed, 19 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 21 13:18:52 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 13:42:08 2017 +0900
@@ -122,10 +122,18 @@
            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 :  (x : a  ) → { fx=gx :  f x ≡ g x  } →  sequ a b  f g 
-           fuga  x { fx=gx } = elem  x fx=gx
-           hoge : sequ a b f g →   sequ a b f g
-           hoge ( elem x eq ) =   elem  x eq
+           xequ :  (x : a  ) → { fx=gx :  f x ≡ g x  } →  sequ a b  f g 
+           xequ  x { fx=gx } = elem  x fx=gx
+           equ→equ : sequ a b f g →   sequ a b f g
+           equ→equ ( elem x eq ) =   elem  x eq
+           lemma1 :  ( e : sequ a b f g ) →  ( z : sequ a b f g ) → elem (equ z) (fe=ge0 z) ≡ equ→equ z
+           lemma1 ( elem x eq ) (elem x' eq' ) =  refl
+           lemma2 :  { e : sequ a b f g } →   ( λ e → elem  (equ e) (fe=ge0 e ) ) ≡ equ→equ
+           lemma2 {e} =  extensionality Sets  ( λ z → lemma1 e z )
+           lemma4 :  ( e : sequ a b f g ) →  ( z : sequ a b f g ) → equ→equ z ≡ z
+           lemma4 ( elem x eq ) (elem x' eq' ) =  refl
+           lemma3 :  { e : sequ a b f g } →    equ→equ   ≡  ( λ e → e )
+           lemma3 {e}  =  extensionality Sets  ( λ z → lemma4  e z )
            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 = 
@@ -134,16 +142,16 @@
               ≡⟨⟩
                  elem  (h y) (fhy=ghy d h y fh=gh )
               ≡⟨⟩
-                 fuga  (h y ) {fhy=ghy d h y fh=gh }
-              ≡⟨ sym ( Category.cong (λ f → fuga (f y )  ) ek'=h )  ⟩
-                 fuga ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
+                 xequ  (h y ) {fhy=ghy d h y fh=gh }
+              ≡⟨ sym ( Category.cong (λ f → xequ (f y )  ) ek'=h )  ⟩
+                 xequ ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
               ≡⟨⟩
-                 ( λ e → fuga ( equ e )) ( k' y ) 
+                 ( λ e → xequ ( equ e )) ( k' y ) 
               ≡⟨⟩
                  ( λ e → elem  (equ e) (fe=ge0 e )) ( k' y ) 
-              ≡⟨ {!!} ⟩
-                  hoge ( k' y ) 
-              ≡⟨ {!!} ⟩
+              ≡⟨ Category.cong ( λ f → f ( k' y ) )  lemma2  ⟩
+                  equ→equ ( k' y ) 
+              ≡⟨ Category.cong ( λ f → f ( k' y ) )  lemma3  ⟩
                  ( λ e → e ) ( k' y ) 
               ≡⟨⟩
                  k' y