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