Mercurial > hg > Members > kono > Proof > category

changeset 163:bc47179e3c9c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
uniqueness continue...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 13:28:08 +0900
parents 18ab1be1ebb5
children ab186f0e7b7a
files free-monoid.agda
diffstat 1 files changed, 9 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Mon Aug 19 12:34:08 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 13:28:08 2013 +0900
@@ -225,5 +225,13 @@
                         lemma-ext1 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x)
         uniquness :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
              { g :  Hom B (Generator a) b } → (FMap U g) o (eta a )  ≡ f  → B [ solution a b f ≈ g ]
-        uniquness = {!!}
+        uniquness {a} {b} {f} {g} eq =  
+                     Extensionarity  ( lemma-ext2 ) where
+                        lemma-ext3 : (morph g) [] ≡  ε b
+                        lemma-ext3 = {!!}
+                        lemma-ext2 : ( ∀{ x : List a } -> (morph ( solution a b f)) x  ≡ (morph g) x  )
+                        -- (morph ( solution a b f)) []  ≡ (morph g) []  )
+                        lemma-ext2 {[]}       = trans (identity (solution a b f)) (sym lemma-ext3 )
+                        lemma-ext2 {x :: xs}  = {!!}
+