Mercurial > hg > Members > kono > Proof > category

changeset 159:0be3e0a49cca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mmmm
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 04:42:06 +0900
parents 9a5becd05681
children c9f29b84ca2f
files free-monoid.agda universal-mapping.agda
diffstat 2 files changed, 62 insertions(+), 80 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Mon Aug 19 00:19:25 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 04:42:06 2013 +0900
@@ -61,22 +61,6 @@
 
 open ≡-Monoid
 
-list  : (a : Set c) -> ≡-Monoid
-list a = record {
-    Carrier    =  List a
-    ; _∙_      = _++_
-    ; ε        = []
-    ; isMonoid = record {
-          identity = ( ( \x -> list-id-l {a}  ) , ( \x -> list-id-r {a} ) ) ;
-          isSemigroup = record {
-               assoc =  \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} )
-             ; isEquivalence = list-isEquivalence
-             ; ∙-cong = \x -> \y ->  list-o-resp-≈ y x
-          }
-      }
-    }
-
-
 record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
   field
       morph : Carrier a -> Carrier b  
@@ -152,6 +136,21 @@
 
 -- FObj 
 
+list  : (a : Set c) -> ≡-Monoid
+list a = record {
+    Carrier    =  List a
+    ; _∙_      = _++_
+    ; ε        = []
+    ; isMonoid = record {
+          identity = ( ( \x -> list-id-l {a}  ) , ( \x -> list-id-r {a} ) ) ;
+          isSemigroup = record {
+               assoc =  \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} )
+             ; isEquivalence = list-isEquivalence
+             ; ∙-cong = \x -> \y ->  list-o-resp-≈ y x
+          }
+      }
+    }
+
 Generator : Obj A -> Obj B
 Generator s =  list s
 
@@ -161,25 +160,53 @@
 
 -- solution
 
-solution : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
-solution = {!!}
-
-universalMapping :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → 
-                             _≈_ A  ( FMap U ( f * ) o  η a ]  ≈ f ]
-universalMapping =   ?
-uniquness :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g :  Hom B (F a) b } → 
-                             A [ A [ FMap U g o  η a ]  ≈ f ] → B [ f * ≈ g ]
-uniquness = ?
-
+open UniversalMapping
 
-FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta 
-FreeMonoidUniveralMapping = 
+FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
+FreeMonoidUniveralMapping  = 
     record {
-       _* = solution ; 
+       _* = \{a b f} solution a b f ; 
        isUniversalMapping = record {
-             universalMapping = universalMapping ; 
-             uniquness = uniquness
+             universalMapping = \{a b f} -> universalMapping {a} {b} {f} ; 
+             uniquness = \{a b f} uniquness {a} {b} {f}
        }
-    }
+    } where
+        Φ :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  List a -> Carrier b
+        Φ {a} {b} {f} [] = ε b
+        Φ {a} {b} {f} ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} {f} xs )
+        lemma-fm-1 :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  
+                 (x y : Carrier (Generator a)) → Φ {a} {b} {f} ((Generator a ∙ x) y) ≡ (b ∙ Φ {a} {b} {f} x) (Φ {a} {b} {f} y)
+        lemma-fm-1 {a} {b} {f} [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ {a} {b} {f} y))
+        lemma-fm-1 {a} {b} {f} (x :: xs) y = let open ≡-Reasoning in 
+             sym ( begin
+                _∙_ b  (Φ (x :: xs)) (Φ y)
+             ≡⟨⟩
+                _∙_ b ( _∙_ b (f x) (Φ xs)) (Φ y)
+             ≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
+                _∙_ b (f x) ( _∙_ b  (Φ xs) (Φ y) )
+             ≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (lemma-fm-1 {a} {b} {f} xs y )) ⟩
+                _∙_ b (f x) ( Φ ( xs ++ y ) )
+             ≡⟨⟩
+                Φ ( x :: ( xs ++ y ) )
+             ≡⟨⟩
+                Φ ( (x ::  xs) ++ y ) 
+             ≡⟨⟩
+                Φ ((Generator a ∙ x :: xs) y) 
+             ∎ )
+        solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
+        solution a b f = record {
+                 morph = \(l : List a) -> Φ l   ;
+                 identity = refl ;
+                 mdistr = \{x y} -> lemma-fm-1 x y 
+            }
+        universalMapping :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  FMap U ( solution  f  ) o eta a   ≡ f
+        universalMapping {a} {b} {f} = let open ≡-Reasoning in 
+                     begin
+                         FMap U ( solution f ) o eta a   
+                     ≡⟨ {!!} ⟩
+                         f
+                     ∎ 
+        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 f ≈ g ]
+        uniquness = {!!}
 
-
--- a/universal-mapping.agda	Mon Aug 19 00:19:25 2013 +0900
+++ b/universal-mapping.agda	Mon Aug 19 04:42:06 2013 +0900
@@ -5,56 +5,11 @@
 open import Category -- https://github.com/konn/category-agda
 open import Level
 open import HomReasoning
+open import cat-utility
+open import Category.Cat
 
 open Functor
-
-id1 :   ∀{c₁ c₂ ℓ  : Level} (A : Category c₁ c₂ ℓ)  (a  : Obj A ) →  Hom A a a
-id1 A a =  (Id {_} {_} {_} {A} a)
-
-record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Obj A → Obj B )
-                 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
-                 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b )
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-   field
-       universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → 
-                     A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
-       uniquness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (F a') b' } → 
-                     A [ A [ FMap U g o  η a' ]  ≈ f ] → B [ f * ≈ g ]
-
-record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Obj A → Obj B )
-                 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-    infixr 11 _*
-    field
-       _* :  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b 
-       isUniversalMapping : IsUniversalMapping A B U F η _*
-
 open NTrans
-open import Category.Cat
-record IsAdjunction  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Functor A B )
-                 ( η : NTrans A A identityFunctor ( U ○  F ) )
-                 ( ε : NTrans B B  ( F ○  U ) identityFunctor )
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-   field
-       adjoint1 :   { b' : Obj B } →
-                     A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ id1 A (FObj U b') ]
-       adjoint2 :   {a' : Obj A} →
-                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ id1 B (FObj F a') ]
-
-record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                 ( U : Functor B A )
-                 ( F : Functor A B )
-                 ( η : NTrans A A identityFunctor ( U ○  F ) )
-                 ( ε : NTrans B B  ( F ○  U ) identityFunctor )
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-    field
-       isAdjunction : IsAdjunction A B U F η ε
 
 --
 --   Adjunction yields solution of universal mapping