Mercurial > hg > Members > kono > Proof > category

comparison src/list-monoid-cat.agda @ 1124:f683d96fbc93 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2024 22:28:50 +0900
parents 5620d4a85069
children
comparison
equal deleted inserted replaced
1123:b6ab443f7a43 1124:f683d96fbc93
2 2
3 open import Category -- https://github.com/konn/category-agda 3 open import Category -- https://github.com/konn/category-agda
4 open import Level 4 open import Level
5 open import HomReasoning 5 open import HomReasoning
6 open import Definitions 6 open import Definitions
7 open import Relation.Binary
8
7 9
8 module list-monoid-cat (c : Level ) where 10 module list-monoid-cat (c : Level ) where
9 11
10 infixr 40 _::_ 12 infixr 40 _::_
11 data List (A : Set ) : Set where 13 data List (A : Set ) : Set where
45 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y ) 47 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λ y → x :: y )
46 ( list-assoc {A} {xs} {ys} {zs} ) 48 ( list-assoc {A} {xs} {ys} {zs} )
47 o-resp-≈ : {A : Set} → {f g : List A } → {h i : List A } → 49 o-resp-≈ : {A : Set} → {f g : List A } → {h i : List A } →
48 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) 50 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
49 o-resp-≈ {A} refl refl = refl 51 o-resp-≈ {A} refl refl = refl
50 isEquivalence1 : {A : Set} → ? -- IsEquivalence {_} {_} {List A } _≡_ 52 isEquivalence1 : {A : Set} → IsEquivalence {_} {_} {List A } _≡_
51 isEquivalence1 {A} = ? -- this is the same function as A's equivalence but has different types 53 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
52 -- record { refl = refl 54 record { refl = refl
53 -- ; sym = sym 55 ; sym = sym
54 -- ; trans = trans 56 ; trans = trans
55 -- } 57 }
56 ListCategory : (A : Set) → Category _ _ _ 58 ListCategory : (A : Set) → Category _ _ _
57 ListCategory A = 59 ListCategory A =
58 record { Obj = ListObj 60 record { Obj = ListObj
59 ; Hom = λ a b → List A 61 ; Hom = λ a b → List A
60 ; _o_ = _++_ 62 ; _o_ = _++_
89 } 91 }
90 where 92 where
91 o-resp-≈ : {M : ≡-Monoid c} → {f g : Carrier M } → {h i : Carrier M } → 93 o-resp-≈ : {M : ≡-Monoid c} → {f g : Carrier M } → {h i : Carrier M } →
92 f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g) 94 f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g)
93 o-resp-≈ {A} refl refl = refl 95 o-resp-≈ {A} refl refl = refl
94 isEquivalence1 : {M : ≡-Monoid c} → ? -- IsEquivalence {_} {_} {Carrier M } _≡_ 96 isEquivalence1 : {M : ≡-Monoid c} → IsEquivalence {_} {_} {Carrier M } _≡_
95 isEquivalence1 {A} = ? -- this is the same function as A's equivalence but has different types 97 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
96 -- record { refl = refl 98 record { refl = refl
97 -- ; sym = sym 99 ; sym = sym
98 -- ; trans = trans 100 ; trans = trans
99 -- } 101 }
100 MonoidCategory : (M : ≡-Monoid c) → Category _ _ _ 102 MonoidCategory : (M : ≡-Monoid c) → Category _ _ _
101 MonoidCategory M = 103 MonoidCategory M =
102 record { Obj = MonoidObj 104 record { Obj = MonoidObj
103 ; Hom = λ a b → Carrier M 105 ; Hom = λ a b → Carrier M
104 ; _o_ = _∙_ M 106 ; _o_ = _∙_ M