|
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
|
|
|
11 _::_ : A -> List A -> List A
|
|
|
12
|
|
|
13
|
|
|
14 infixl 30 _++_
|
|
|
15 _++_ : {A : Set } -> List A -> List A -> List A
|
|
|
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
|
|
|
27 isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_ _++_ []
|
|
|
28 isListCategory A = record { isEquivalence = isEquivalence1 {A}
|
|
|
29 ; identityL = list-id-l
|
|
|
30 ; identityR = list-id-r
|
|
|
31 ; o-resp-≈ = o-resp-≈ {A}
|
|
|
32 ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
|
|
|
33 }
|
|
|
34 where
|
|
|
35 list-id-l : { A : Set } -> { x : List A } -> [] ++ x ≡ x
|
|
|
36 list-id-l {_} {_} = refl
|
|
|
37 list-id-r : { A : Set } -> { x : List A } -> x ++ [] ≡ x
|
|
|
38 list-id-r {_} {[]} = refl
|
|
|
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 } ->
|
|
|
41 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
|
|
|
42 list-assoc {_} {[]} {_} {_} = refl
|
|
|
43 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y )
|
|
|
44 ( list-assoc {A} {xs} {ys} {zs} )
|
|
|
45 o-resp-≈ : {A : Set} -> {f g : List A } → {h i : List A } →
|
|
|
46 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
|
|
|
47 o-resp-≈ {A} refl refl = refl
|
|
|
48 isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A } _≡_
|
|
|
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 }
|
|
|
54 ListCategory : (A : Set) -> Category _ _ _
|
|
|
55 ListCategory A =
|
|
|
56 record { Obj = ListObj
|
|
|
57 ; Hom = \a b -> List A
|
|
|
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
|
|
|
81 isMonoidCategory : (M : ≡-Monoid c) -> IsCategory MonoidObj (\a b -> Carrier M ) _≡_ (_∙_ M) (ε M)
|
|
|
82 isMonoidCategory M = record { isEquivalence = isEquivalence1 {M}
|
|
|
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 )
|
|
|
86 ; o-resp-≈ = o-resp-≈ {M}
|
|
|
87 }
|
|
|
88 where
|
|
|
89 o-resp-≈ : {M : ≡-Monoid c} -> {f g : Carrier M } → {h i : Carrier M } →
|
|
|
90 f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g)
|
|
|
91 o-resp-≈ {A} refl refl = refl
|
|
|
92 isEquivalence1 : {M : ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M } _≡_
|
|
|
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 }
|
|
|
98 MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
|
|
|
99 MonoidCategory M =
|
|
|
100 record { Obj = MonoidObj
|
|
|
101 ; Hom = \a b -> Carrier M
|
|
|
102 ; _o_ = _∙_ M
|
|
|
103 ; _≈_ = _≡_
|
|
|
104 ; Id = ε M
|
|
|
105 ; isCategory = ( isMonoidCategory M )
|
|
|
106 }
|
|
|
107
|
