Mercurial > hg > Members > kono > Proof > category

changeset 517:6f7630a255e4

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, 21 Mar 2017 14:16:38 +0900
parents 327dc7372729
children 52d30ad7f652
files SetsCompleteness.agda
diffstat 1 files changed, 7 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 21 13:42:08 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 21 14:16:38 2017 +0900
@@ -124,34 +124,26 @@
            fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh
            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 :  ( e : sequ a b f g ) →  ( z : sequ a b f g ) →  elem (equ z) (fe=ge0 z) ≡ 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 : sequ a b f g } →   ( λ e → elem  (equ e) (fe=ge0 e ) ) ≡ ( λ e → e )
            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 ) →
+           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
-           repl {d} {h} {fh=gh} {k'} y ek'=h = 
+           uniquness1 {d} {h} {fh=gh} {k'} y ek'=h = 
               begin
                  k h fh=gh y
               ≡⟨⟩
                  elem  (h y) (fhy=ghy d h y fh=gh )
               ≡⟨⟩
                  xequ  (h y ) {fhy=ghy d h y fh=gh }
-              ≡⟨ sym ( Category.cong (λ f → xequ (f y )  ) ek'=h )  ⟩
+              ≡⟨ sym ( Category.cong (λ i → xequ (i y )  ) ek'=h )  ⟩
                  xequ ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
               ≡⟨⟩
-                 ( λ e → xequ ( equ e )) ( k' y ) 
+                 ( λ e → xequ ( equ e )  {fe=ge0 e } ) ( k' y ) 
               ≡⟨⟩
                  ( λ e → elem  (equ e) (fe=ge0 e )) ( 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
@@ -161,7 +153,7 @@
                   open ≡-Reasoning 
            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 →  repl {d} {h} {fh=gh}{k'}  y ek'=h   ) 
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets ( λ y →  uniquness1 {d} {h} {fh=gh}{k'}  y ek'=h   ) 
 
 
 open Functor