annotate list-monoid-cat.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents d6a6dd305da2
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import HomReasoning
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import cat-utility
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
168
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
6 module list-monoid-cat (c : Level ) where
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 infixr 40 _::_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 data List (A : Set ) : Set where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 [] : List A
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
11 _::_ : A → List A → List A
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 infixl 30 _++_
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
15 _++_ : {A : Set } → List A → List A → List A
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 [] ++ ys = ys
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 (x :: xs) ++ ys = x :: (xs ++ ys)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 data ListObj : Set where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * : ListObj
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open import Relation.Binary.Core
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open import Relation.Binary.PropositionalEquality
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 ≡-cong = Relation.Binary.PropositionalEquality.cong
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
27 isListCategory : (A : Set) → IsCategory ListObj (λ a b → List A) _≡_ _++_ []
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 isListCategory A = record { isEquivalence = isEquivalence1 {A}
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 ; identityL = list-id-l
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 ; identityR = list-id-r
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 ; o-resp-≈ = o-resp-≈ {A}
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
32 ; associative = λ {a} {b} {c} {d} {x} {y} {z} → list-assoc {A} {x} {y} {z}
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 where
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
35 list-id-l : { A : Set } → { x : List A } → [] ++ x ≡ x
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 list-id-l {_} {_} = refl
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
37 list-id-r : { A : Set } → { x : List A } → x ++ [] ≡ x
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 list-id-r {_} {[]} = refl
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
39 list-id-r {A} {x :: xs} = ≡-cong ( λ y → x :: y ) ( list-id-r {A} {xs} )
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
40 list-assoc : {A : Set} → { xs ys zs : List A } →
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 list-assoc {_} {[]} {_} {_} = refl
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
43 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y )
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 ( list-assoc {A} {xs} {ys} {zs} )
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
45 o-resp-≈ : {A : Set} → {f g : List A } → {h i : List A } →
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 o-resp-≈ {A} refl refl = refl
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
48 isEquivalence1 : {A : Set} → IsEquivalence {_} {_} {List A } _≡_
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 record { refl = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 ; sym = sym
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 ; trans = trans
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 }
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
54 ListCategory : (A : Set) → Category _ _ _
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 ListCategory A =
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 record { Obj = ListObj
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
57 ; Hom = λ a b → List A
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 ; _o_ = _++_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ; _≈_ = _≡_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ; Id = []
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ; isCategory = ( isListCategory A )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 open import Algebra.Structures
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 open import Algebra.FunctionProperties using (Op₁; Op₂)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 data MonoidObj : Set c where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 ! : MonoidObj
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 record ≡-Monoid c : Set (suc c) where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 infixl 7 _∙_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 field
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 Carrier : Set c
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 _∙_ : Op₂ Carrier
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ε : Carrier
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 isMonoid : IsMonoid _≡_ _∙_ ε
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 open ≡-Monoid
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 open import Data.Product
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
81 isMonoidCategory : (M : ≡-Monoid c) → IsCategory MonoidObj (λ a b → Carrier M ) _≡_ (_∙_ M) (ε M)
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 isMonoidCategory M = record { isEquivalence = isEquivalence1 {M}
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
83 ; identityL = λ {_} {_} {x} → (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
84 ; identityR = λ {_} {_} {x} → (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
85 ; associative = λ {a} {b} {c} {d} {x} {y} {z} → sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 ; o-resp-≈ = o-resp-≈ {M}
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 where
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
89 o-resp-≈ : {M : ≡-Monoid c} → {f g : Carrier M } → {h i : Carrier M } →
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 o-resp-≈ {A} refl refl = refl
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
92 isEquivalence1 : {M : ≡-Monoid c} → IsEquivalence {_} {_} {Carrier M } _≡_
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 record { refl = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ; sym = sym
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 ; trans = trans
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 }
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
98 MonoidCategory : (M : ≡-Monoid c) → Category _ _ _
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 MonoidCategory M =
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 record { Obj = MonoidObj
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 168
diff changeset
101 ; Hom = λ a b → Carrier M
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 ; _o_ = _∙_ M
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 ; _≈_ = _≡_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 ; Id = ε M
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 ; isCategory = ( isMonoidCategory M )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107