|
154
|
1 open import Category -- https://github.com/konn/category-agda
|
|
|
2 open import Level
|
|
|
3 open import HomReasoning
|
|
|
4 open import cat-utility
|
|
|
5
|
|
|
6 module free-monoid (c : Level ) where
|
|
|
7
|
|
|
8 postulate A : Set
|
|
|
9
|
|
|
10 postulate a : A
|
|
|
11 postulate b : A
|
|
|
12
|
|
|
13
|
|
|
14 infixr 40 _::_
|
|
|
15 data List (A : Set ) : Set where
|
|
|
16 [] : List A
|
|
|
17 _::_ : A -> List A -> List A
|
|
|
18
|
|
|
19
|
|
|
20 infixl 30 _++_
|
|
|
21 _++_ : {A : Set } -> List A -> List A -> List A
|
|
|
22 [] ++ ys = ys
|
|
|
23 (x :: xs) ++ ys = x :: (xs ++ ys)
|
|
|
24
|
|
|
25 data ListObj : Set where
|
|
|
26 * : ListObj
|
|
|
27
|
|
|
28 open import Relation.Binary.Core
|
|
|
29 open import Relation.Binary.PropositionalEquality
|
|
|
30
|
|
|
31 ≡-cong = Relation.Binary.PropositionalEquality.cong
|
|
|
32
|
|
|
33 isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_ _++_ []
|
|
|
34 isListCategory A = record { isEquivalence = isEquivalence1 {A}
|
|
|
35 ; identityL = list-id-l
|
|
|
36 ; identityR = list-id-r
|
|
|
37 ; o-resp-≈ = o-resp-≈ {A}
|
|
|
38 ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
|
|
|
39 }
|
|
|
40 where
|
|
|
41 list-id-l : { A : Set } -> { x : List A } -> [] ++ x ≡ x
|
|
|
42 list-id-l {_} {_} = refl
|
|
|
43 list-id-r : { A : Set } -> { x : List A } -> x ++ [] ≡ x
|
|
|
44 list-id-r {_} {[]} = refl
|
|
|
45 list-id-r {A} {x :: xs} = ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} )
|
|
|
46 list-assoc : {A : Set} -> { xs ys zs : List A } ->
|
|
|
47 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
|
|
|
48 list-assoc {_} {[]} {_} {_} = refl
|
|
|
49 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y )
|
|
|
50 ( list-assoc {A} {xs} {ys} {zs} )
|
|
|
51 o-resp-≈ : {A : Set} -> {f g : List A } → {h i : List A } →
|
|
|
52 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
|
|
|
53 o-resp-≈ {A} refl refl = refl
|
|
|
54 isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A } _≡_
|
|
|
55 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
|
|
|
56 record { refl = refl
|
|
|
57 ; sym = sym
|
|
|
58 ; trans = trans
|
|
|
59 }
|
|
|
60 ListCategory : (A : Set) -> Category _ _ _
|
|
|
61 ListCategory A =
|
|
|
62 record { Obj = ListObj
|
|
|
63 ; Hom = \a b -> List A
|
|
|
64 ; _o_ = _++_
|
|
|
65 ; _≈_ = _≡_
|
|
|
66 ; Id = []
|
|
|
67 ; isCategory = ( isListCategory A )
|
|
|
68 }
|
|
|
69
|
|
|
70 open import Algebra.Structures
|
|
|
71 open import Algebra.FunctionProperties using (Op₁; Op₂)
|
|
|
72
|
|
|
73 data MonoidObj : Set c where
|
|
|
74 ! : MonoidObj
|
|
|
75
|
|
|
76 record ≡-Monoid c : Set (suc c) where
|
|
|
77 infixl 7 _∙_
|
|
|
78 field
|
|
|
79 Carrier : Set c
|
|
|
80 _∙_ : Op₂ Carrier
|
|
|
81 ε : Carrier
|
|
|
82 isMonoid : IsMonoid _≡_ _∙_ ε
|
|
|
83
|
|
|
84 open ≡-Monoid
|
|
|
85 open import Data.Product
|
|
|
86
|
|
|
87 isMonoidCategory : (M : ≡-Monoid c) -> IsCategory MonoidObj (\a b -> Carrier M ) _≡_ (_∙_ M) (ε M)
|
|
|
88 isMonoidCategory M = record { isEquivalence = isEquivalence1 {M}
|
|
|
89 ; identityL = \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
|
|
|
90 ; identityR = \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
|
|
|
91 ; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
|
|
|
92 ; o-resp-≈ = o-resp-≈ {M}
|
|
|
93 }
|
|
|
94 where
|
|
|
95 o-resp-≈ : {M : ≡-Monoid c} -> {f g : Carrier M } → {h i : Carrier M } →
|
|
|
96 f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g)
|
|
|
97 o-resp-≈ {A} refl refl = refl
|
|
|
98 isEquivalence1 : {M : ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M } _≡_
|
|
|
99 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
|
|
|
100 record { refl = refl
|
|
|
101 ; sym = sym
|
|
|
102 ; trans = trans
|
|
|
103 }
|
|
|
104 MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
|
|
|
105 MonoidCategory M =
|
|
|
106 record { Obj = MonoidObj
|
|
|
107 ; Hom = \a b -> Carrier M
|
|
|
108 ; _o_ = _∙_ M
|
|
|
109 ; _≈_ = _≡_
|
|
|
110 ; Id = ε M
|
|
|
111 ; isCategory = ( isMonoidCategory M )
|
|
|
112 }
|
|
|
113
|
|
|
114
|
|
|
115
|
