Mercurial > hg > Members > kono > Proof > category
comparison free-monoid.agda @ 154:744be443e232
on going
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 18 Aug 2013 19:55:05 +0900 (2013-08-18) |
parents | |
children | d9cbaa749be6 |
comparison
equal
deleted
inserted
replaced
153:3249aaddc405 | 154:744be443e232 |
---|---|
1 open import Category -- https://github.com/konn/category-agda | |
2 open import Level | |
3 module free-monoid { c c₁ c₂ ℓ : Level } where | |
4 | |
5 open import Category.Sets | |
6 open import Category.Cat | |
7 open import HomReasoning | |
8 open import cat-utility | |
9 open import Relation.Binary.Core | |
10 open import Relation.Binary.PropositionalEquality | |
11 | |
12 | |
13 A = Sets {c₁} | |
14 B = CAT | |
15 | |
16 infixr 40 _::_ | |
17 data List (A : Set ) : Set where | |
18 [] : List A | |
19 _::_ : A -> List A -> List A | |
20 | |
21 | |
22 infixl 30 _++_ | |
23 _++_ : {A : Set } -> List A -> List A -> List A | |
24 [] ++ ys = ys | |
25 (x :: xs) ++ ys = x :: (xs ++ ys) | |
26 | |
27 data ListObj : Set where | |
28 * : ListObj | |
29 | |
30 ≡-cong = Relation.Binary.PropositionalEquality.cong | |
31 | |
32 isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_ _++_ [] | |
33 isListCategory A = record { isEquivalence = isEquivalence1 {A} | |
34 ; identityL = list-id-l | |
35 ; identityR = list-id-r | |
36 ; o-resp-≈ = o-resp-≈ {A} | |
37 ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z} | |
38 } | |
39 where | |
40 list-id-l : { A : Set } -> { x : List A } -> [] ++ x ≡ x | |
41 list-id-l {_} {_} = refl | |
42 list-id-r : { A : Set } -> { x : List A } -> x ++ [] ≡ x | |
43 list-id-r {_} {[]} = refl | |
44 list-id-r {A} {x :: xs} = ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) | |
45 list-assoc : {A : Set} -> { xs ys zs : List A } -> | |
46 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs ) | |
47 list-assoc {_} {[]} {_} {_} = refl | |
48 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y ) | |
49 ( list-assoc {A} {xs} {ys} {zs} ) | |
50 o-resp-≈ : {A : Set} -> {f g : List A } → {h i : List A } → | |
51 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) | |
52 o-resp-≈ {A} refl refl = refl | |
53 isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A } _≡_ | |
54 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types | |
55 record { refl = refl | |
56 ; sym = sym | |
57 ; trans = trans | |
58 } | |
59 ListCategory : (A : Set) -> Category _ _ _ | |
60 ListCategory A = | |
61 record { Obj = ListObj | |
62 ; Hom = \a b -> List A | |
63 ; _o_ = _++_ | |
64 ; _≈_ = _≡_ | |
65 ; Id = [] | |
66 ; isCategory = ( isListCategory A ) | |
67 } | |
68 | |
69 open import Algebra.FunctionProperties using (Op₁; Op₂) | |
70 | |
71 open import Algebra.Structures | |
72 | |
73 record ≡-Monoid : Set (suc c) where | |
74 infixl 7 _∙_ | |
75 field | |
76 Carrier : Set c | |
77 _∙_ : Op₂ Carrier | |
78 ε : Carrier | |
79 isMonoid : IsMonoid _≡_ _∙_ ε | |
80 | |
81 open ≡-Monoid | |
82 | |
83 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where | |
84 field | |
85 morph : Carrier a -> Carrier b | |
86 identity : morph (ε a) ≡ ε b | |
87 mdistr : ∀{x y} -> morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) ) | |
88 | |
89 open Monomorph | |
90 | |
91 _*_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c | |
92 _*_ {a} {b} {c} f g = record { | |
93 morph = \x -> morph f ( morph g x ) ; | |
94 identity = identity1 ; | |
95 mdistr = mdistr1 | |
96 } where | |
97 identity1 : morph f ( morph g (ε a) ) ≡ ε c | |
98 -- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b | |
99 -- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c | |
100 identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f ) | |
101 mdistr1 : ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) | |
102 -- ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) ) | |
103 -- ∀{x y} -> morph f ( ( _∙_ c (morph g x )) (morph g y) ) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) ) | |
104 mdistr1 = trans (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) | |
105 | |
106 | |
107 --isMonoidCategory : IsCategory ≡-Monoid Monomorph _≡_ (_*_ M) (M-id) | |
108 --isMonoidCategory = ? -- record { isEquivalence = isEquivalence1 {M} | |
109 -- ; identityL = \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) | |
110 -- ; identityR = \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x ) | |
111 -- ; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z ) | |
112 -- ; o-resp-≈ = o-resp-≈ {M} | |
113 -- } | |
114 -- where | |
115 -- o-resp-≈ : {M : ≡-Monoid c} -> {f g : Carrier M } → {h i : Carrier M } → | |
116 -- f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g) | |
117 -- o-resp-≈ {A} refl refl = refl | |
118 -- isEquivalence1 : {M : ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M } _≡_ | |
119 -- isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types | |
120 -- record { refl = refl | |
121 -- ; sym = sym | |
122 -- ; trans = trans | |
123 -- } | |
124 -- MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _ | |
125 -- MonoidCategory M = | |
126 -- record { Obj = MonoidObj | |
127 -- ; Hom = \a b -> Carrier M | |
128 -- ; _o_ = _∙_ M | |
129 -- ; _≈_ = _≡_ | |
130 -- ; Id = ε M | |
131 -- ; isCategory = ( isMonoidCategory M ) | |
132 -- } | |
133 | |
134 | |
135 | |
136 | |
137 -- open Functor | |
138 | |
139 -- U : Functor B A | |
140 -- U = record { | |
141 -- FObj = \c -> Obj c ; | |
142 -- FMap = \f -> (\x -> FMap f x) ; | |
143 -- isFunctor = record { | |
144 -- ≈-cong = ≈-cong | |
145 -- ; identity = identity1 | |
146 -- ; distr = distr1 | |
147 -- } | |
148 -- } where | |
149 -- identity1 : {a : Obj B} → A [ FMap identityFunctor ≈ ( \x -> x ) ] | |
150 -- identity1 {a} = _≡_.refl | |
151 -- ≈-cong : {a b : Obj B} {f g : Hom B a b} → B [ f ≈ g ] → ? | |
152 -- ≈-cong {a} {b} {f} {g} = ? | |
153 -- distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → A [ ( FMap ( g ○ f )) ≈ ( \x -> FMap g (FMap f x )) ] | |
154 -- distr1 {a} {b} {c} {f} {g} = ? | |
155 |