Mercurial > hg > Members > kono > Proof > category

changeset 518:52d30ad7f652

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Mar 2017 15:15:46 +0900
parents 6f7630a255e4
children 844328b49d5d
files SetsCompleteness.agda
diffstat 1 files changed, 18 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 21 14:16:38 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 15:15:46 2017 +0900
@@ -128,6 +128,8 @@
            lemma1 ( elem x eq ) (elem x' eq' ) =  refl
            lemma2 :  { e : sequ a b f g } →   ( λ e → elem  (equ e) (fe=ge0 e ) ) ≡ ( λ e → e )
            lemma2 {e} =  extensionality Sets  ( λ z → lemma1 e z )
+           lemma3 :  {d : Obj Sets} (  e : sequ a b f g → a  ) → ( y : d ) → (k' : Hom Sets d (sequ a b f g))   → f ( e (k' y) ) ≡ g ( e (k' y))
+           lemma3 {d} e y k' = {!!}
            uniquness1 :   {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
            uniquness1 {d} {h} {fh=gh} {k'} y ek'=h = 
@@ -137,7 +139,7 @@
                  elem  (h y) (fhy=ghy d h y fh=gh )
               ≡⟨⟩
                  xequ  (h y ) {fhy=ghy d h y fh=gh }
-              ≡⟨ sym ( Category.cong (λ i → xequ (i y )  ) ek'=h )  ⟩
+              ≡⟨ sym ( Category.cong (λ ek' → xequ (ek' y ) {{!!}} ) ek'=h )  ⟩
                  xequ ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
               ≡⟨⟩
                  ( λ e → xequ ( equ e )  {fe=ge0 e } ) ( k' y ) 
@@ -154,6 +156,21 @@
            uniqueness :   {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)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
            uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets ( λ y →  uniquness1 {d} {h} {fh=gh}{k'}  y ek'=h   ) 
+           uniqueness0 :   {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)} →
+                Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
+           uniqueness0  {d} {h} {fh=gh} {k'} ek'=h =  begin
+                 k h fh=gh
+              ≈⟨ {!!} ⟩
+                 k ( Sets [  (λ e → equ e)  o k' ]  ) {!!}
+              ≈⟨⟩
+                 Sets [ ( λ e → elem  (equ e) (fe=ge0 e ))  o  k'  ]
+              ≈⟨ {!!} ⟩
+                 Sets [ ( λ e → e ) o k'  ]
+              ≈⟨⟩
+                 k' 
+              ∎ where
+                  open ≈-Reasoning Sets
+
 
 
 open Functor