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