Mercurial > hg > Members > kono > Proof > category

changeset 155:d9cbaa749be6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monoids done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Aug 2013 21:30:00 +0900
parents 744be443e232
children b15c1435cfcc
files free-monoid.agda
diffstat 1 files changed, 35 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/free-monoid.agda	Sun Aug 18 19:55:05 2013 +0900
+++ b/free-monoid.agda	Sun Aug 18 21:30:00 2013 +0900
@@ -1,3 +1,5 @@
+-- {-# OPTIONS --universe-polymorphism #-}
+
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 module free-monoid { c c₁ c₂ ℓ : Level }   where
@@ -88,8 +90,8 @@
 
 open Monomorph
 
-_*_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
-_*_ {a} {b} {c} f g =  record {
+_+_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
+_+_ {a} {b} {c} f g =  record {
       morph = \x ->  morph  f ( morph g x ) ;
       identity  = identity1 ;
       mdistr  = mdistr1 
@@ -103,33 +105,38 @@
       --  ∀{x y} -> morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
       mdistr1 = trans  (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) 
 
+M-id : { a : ≡-Monoid } -> Monomorph a a 
+M-id = record { morph = \x -> x  ; identity = refl ; mdistr = refl }
 
---isMonoidCategory : IsCategory ≡-Monoid Monomorph _≡_  (_*_  M) (M-id)
---isMonoidCategory  = ? -- record  { isEquivalence =  isEquivalence1 {M}
---                     ; identityL =   \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
---                     ; identityR =   \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
---                     ; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
---                     ; o-resp-≈ =    o-resp-≈ {M}
---                     }
---      where
---         o-resp-≈ :  {M :  ≡-Monoid c} ->  {f g : Carrier M } → {h i : Carrier M } → 
---                           f ≡  g → h ≡  i → (_∙_ M  h f) ≡  (_∙_ M i g)
---         o-resp-≈  {A} refl refl = refl
---         isEquivalence1 : {M :  ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M }  _≡_ 
---         isEquivalence1 {A} =      -- this is the same function as A's equivalence but has different types
---            record { refl  = refl
---              ; sym   = sym
---              ; trans = trans
---              } 
--- MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
--- MonoidCategory M =
---   record { Obj = MonoidObj
---          ; Hom = \a b -> Carrier M 
---          ; _o_ = _∙_  M
---          ; _≈_ = _≡_
---          ; Id  =  ε M
---          ; isCategory = ( isMonoidCategory M )
---           }
+_==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c 
+_==_  f g =  morph f ≡ morph g
+
+isMonoidCategory : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
+isMonoidCategory  = record  { isEquivalence =  isEquivalence1 
+                    ; identityL =  refl
+                    ; identityR =  refl
+                    ; associative = refl
+                    ; o-resp-≈ =    \{a} {b} {c} {f} {g} {h} {i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
+                    }
+     where
+        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-≈  {A} refl refl = refl
+        isEquivalence1 : { a b : ≡-Monoid } -> IsEquivalence {_} {_} {Monomorph a b}  _==_ 
+        isEquivalence1  =      -- this is the same function as A's equivalence but has different types
+           record { refl  = refl
+             ; sym   = sym
+             ; trans = trans
+             } 
+MonoidCategory : Category _ _ _
+MonoidCategory  =
+  record { Obj =  ≡-Monoid 
+         ; Hom = Monomorph
+         ; _o_ = _+_  
+         ; _≈_ = _==_
+         ; Id  =  M-id
+         ; isCategory = isMonoidCategory 
+           }