comparison free-monoid.agda @ 154:744be443e232

on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Aug 2013 19:55:05 +0900 (2013-08-18)
parents
children d9cbaa749be6
comparison
equal deleted inserted replaced
153:3249aaddc405 154:744be443e232
1 open import Category -- https://github.com/konn/category-agda
2 open import Level
3 module free-monoid { c c₁ c₂ ℓ : Level } where
4
5 open import Category.Sets
6 open import Category.Cat
7 open import HomReasoning
8 open import cat-utility
9 open import Relation.Binary.Core
10 open import Relation.Binary.PropositionalEquality
11
12
13 A = Sets {c₁}
14 B = CAT
15
16 infixr 40 _::_
17 data List (A : Set ) : Set where
18 [] : List A
19 _::_ : A -> List A -> List A
20
21
22 infixl 30 _++_
23 _++_ : {A : Set } -> List A -> List A -> List A
24 [] ++ ys = ys
25 (x :: xs) ++ ys = x :: (xs ++ ys)
26
27 data ListObj : Set where
28 * : ListObj
29
30 ≡-cong = Relation.Binary.PropositionalEquality.cong
31
32 isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_ _++_ []
33 isListCategory A = record { isEquivalence = isEquivalence1 {A}
34 ; identityL = list-id-l
35 ; identityR = list-id-r
36 ; o-resp-≈ = o-resp-≈ {A}
37 ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
38 }
39 where
40 list-id-l : { A : Set } -> { x : List A } -> [] ++ x ≡ x
41 list-id-l {_} {_} = refl
42 list-id-r : { A : Set } -> { x : List A } -> x ++ [] ≡ x
43 list-id-r {_} {[]} = refl
44 list-id-r {A} {x :: xs} = ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} )
45 list-assoc : {A : Set} -> { xs ys zs : List A } ->
46 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
47 list-assoc {_} {[]} {_} {_} = refl
48 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y )
49 ( list-assoc {A} {xs} {ys} {zs} )
50 o-resp-≈ : {A : Set} -> {f g : List A } → {h i : List A } →
51 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
52 o-resp-≈ {A} refl refl = refl
53 isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A } _≡_
54 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
55 record { refl = refl
56 ; sym = sym
57 ; trans = trans
58 }
59 ListCategory : (A : Set) -> Category _ _ _
60 ListCategory A =
61 record { Obj = ListObj
62 ; Hom = \a b -> List A
63 ; _o_ = _++_
64 ; _≈_ = _≡_
65 ; Id = []
66 ; isCategory = ( isListCategory A )
67 }
68
69 open import Algebra.FunctionProperties using (Op₁; Op₂)
70
71 open import Algebra.Structures
72
73 record ≡-Monoid : Set (suc c) where
74 infixl 7 _∙_
75 field
76 Carrier : Set c
77 _∙_ : Op₂ Carrier
78 ε : Carrier
79 isMonoid : IsMonoid _≡_ _∙_ ε
80
81 open ≡-Monoid
82
83 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where
84 field
85 morph : Carrier a -> Carrier b
86 identity : morph (ε a) ≡ ε b
87 mdistr : ∀{x y} -> morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) )
88
89 open Monomorph
90
91 _*_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
92 _*_ {a} {b} {c} f g = record {
93 morph = \x -> morph f ( morph g x ) ;
94 identity = identity1 ;
95 mdistr = mdistr1
96 } where
97 identity1 : morph f ( morph g (ε a) ) ≡ ε c
98 -- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b
99 -- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c
100 identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f )
101 mdistr1 : ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) )
102 -- ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) )
103 -- ∀{x y} -> morph f ( ( _∙_ c (morph g x )) (morph g y) ) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) )
104 mdistr1 = trans (≡-cong (morph f ) ( mdistr g) ) ( mdistr f )
105
106
107 --isMonoidCategory : IsCategory ≡-Monoid Monomorph _≡_ (_*_ M) (M-id)
108 --isMonoidCategory = ? -- record { isEquivalence = isEquivalence1 {M}
109 -- ; identityL = \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
110 -- ; identityR = \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
111 -- ; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
112 -- ; o-resp-≈ = o-resp-≈ {M}
113 -- }
114 -- where
115 -- o-resp-≈ : {M : ≡-Monoid c} -> {f g : Carrier M } → {h i : Carrier M } →
116 -- f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g)
117 -- o-resp-≈ {A} refl refl = refl
118 -- isEquivalence1 : {M : ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M } _≡_
119 -- isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
120 -- record { refl = refl
121 -- ; sym = sym
122 -- ; trans = trans
123 -- }
124 -- MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
125 -- MonoidCategory M =
126 -- record { Obj = MonoidObj
127 -- ; Hom = \a b -> Carrier M
128 -- ; _o_ = _∙_ M
129 -- ; _≈_ = _≡_
130 -- ; Id = ε M
131 -- ; isCategory = ( isMonoidCategory M )
132 -- }
133
134
135
136
137 -- open Functor
138
139 -- U : Functor B A
140 -- U = record {
141 -- FObj = \c -> Obj c ;
142 -- FMap = \f -> (\x -> FMap f x) ;
143 -- isFunctor = record {
144 -- ≈-cong = ≈-cong
145 -- ; identity = identity1
146 -- ; distr = distr1
147 -- }
148 -- } where
149 -- identity1 : {a : Obj B} → A [ FMap identityFunctor ≈ ( \x -> x ) ]
150 -- identity1 {a} = _≡_.refl
151 -- ≈-cong : {a b : Obj B} {f g : Hom B a b} → B [ f ≈ g ] → ?
152 -- ≈-cong {a} {b} {f} {g} = ?
153 -- distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → A [ ( FMap ( g ○ f )) ≈ ( \x -> FMap g (FMap f x )) ]
154 -- distr1 {a} {b} {c} {f} {g} = ?
155