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