Mercurial > hg > Members > kono > Proof > category

changeset 421:06ffcad985ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix free-monoid
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 12:07:32 +0900
parents 3e44951b9bdb
children 3a4a99a8edbe
files free-monoid.agda
diffstat 1 files changed, 27 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Thu Mar 24 11:31:14 2016 +0900
+++ b/free-monoid.agda	Thu Mar 24 12:07:32 2016 +0900
@@ -73,7 +73,7 @@
 
 infixr 9 _<_∙_>
 
-record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
+record Monomorph ( a b : ≡-Monoid )  : Set c where
   field
       morph : Carrier a → Carrier b  
       identity     :  morph (ε a)  ≡  ε b
@@ -110,6 +110,10 @@
 _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c 
 _==_  f g =  morph f ≡ morph g
 
+-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
+-- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
+postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c 
+
 isMonoids : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
 isMonoids  = record  { isEquivalence =  isEquivalence1 
                     ; identityL =  refl
@@ -124,9 +128,29 @@
              ; sym   = sym
              ; trans = trans
              } 
-        o-resp-≈ :  {a b c :  ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → 
+        o-resp-≈ :  {a b c :  ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c }  → 
                           f ==  g → h ==  i → (h + f) ==  (i + g)
-        o-resp-≈ refl refl = refl
+        o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i =  let open ≡-Reasoning in begin
+             morph ( h + f )
+         ≡⟨ ≡-cong ( λ  g → ( ( λ (x : Carrier a ) →  g x ) )) (extensionality {Carrier a} lemma11) ⟩
+             morph ( i + g )
+         ∎  
+             where
+                lemma11 : (x : Carrier a) → morph (h + f) x ≡ morph (i + g) x
+                lemma11 x =   let open ≡-Reasoning in begin
+                          morph ( h + f ) x
+                     ≡⟨⟩
+                          morph h ( ( morph f ) x )
+                     ≡⟨  ≡-cong ( \y -> morph h ( y x ) )  f==g ⟩
+                          morph h ( morph g x )
+                     ≡⟨  ≡-cong ( \y -> y ( morph g  x ) )  h==i ⟩
+                          morph i ( morph g x )
+                     ≡⟨⟩
+                          morph ( i + g ) x
+                     ∎
+
+
+
 
 Monoids : Category _ _ _
 Monoids  =
@@ -212,10 +236,6 @@
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
 eta  a = λ ( x : a ) →  x :: []
 
--- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
--- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
-postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c 
-
 FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
 FreeMonoidUniveralMapping = 
     record {