Mercurial > hg > Members > kono > Proof > category

comparison src/HomReasoning.agda @ 949:ac53803b3b2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganization for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 16:40:15 +0900
parents HomReasoning.agda@dca4b29553cb
children 270f0ba65b88
comparison
equal deleted inserted replaced
948:dca4b29553cb 949:ac53803b3b2a
1 module HomReasoning where
2
3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
4
5 open import Category -- https://github.com/konn/category-agda
6 open import Level
7 open Functor
8
9 -- F(f)
10 -- F(a) ---→ F(b)
11 -- | |
12 -- |t(a) |t(b) G(f)t(a) = t(b)F(f)
13 -- | |
14 -- v v
15 -- G(a) ---→ G(b)
16 -- G(f)
17
18 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
19 ( F G : Functor D C )
20 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
21 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
22 field
23 commute : {a b : Obj D} {f : Hom D a b}
24 → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ]
25
26 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′)
27 (F G : Functor domain codomain )
28 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
29 field
30 TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
31 isNTrans : IsNTrans domain codomain F G TMap
32
33
34 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
35 open import Relation.Binary
36
37 _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
38 x o y = A [ x o y ]
39
40 _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ
41 x ≈ y = A [ x ≈ y ]
42
43 infixr 9 _o_
44 infix 4 _≈_
45
46 refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x
47 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))
48
49 trans-hom : {a b : Obj A } { x y z : Hom A a b } →
50 x ≈ y → y ≈ z → x ≈ z
51 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c
52
53 -- some short cuts
54
55 car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
56 x ≈ y → ( x o f ) ≈ ( y o f )
57 car eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq
58
59 car1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
60 A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ]
61 car1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) eq
62
63 cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
64 x ≈ y → f o x ≈ f o y
65 cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom )
66
67 cdr1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
68 A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ]
69 cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) )
70
71 id : (a : Obj A ) → Hom A a a
72 id a = (Id {_} {_} {_} {A} a)
73
74 idL : {a b : Obj A } { f : Hom A a b } → id b o f ≈ f
75 idL = IsCategory.identityL (Category.isCategory A)
76
77 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f
78 idR = IsCategory.identityR (Category.isCategory A)
79
80 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f
81 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
82
83 sym-hom = sym
84
85 -- working on another cateogry
86 idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ]
87 idL1 A = IsCategory.identityL (Category.isCategory A)
88
89 idR1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } → A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f ]
90 idR1 A = IsCategory.identityR (Category.isCategory A)
91
92 open import Relation.Binary.PropositionalEquality using ( _≡_ )
93 ≈←≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y
94 ≈←≡ _≡_.refl = refl-hom
95
96 -- Ho← to prove this?
97 -- ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y
98 -- ≡←≈ x≈y = irr x≈y
99
100 ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } →
101 (f : Hom B x y → Hom A x' y' ) → a ≡ b → f a ≈ f b
102 ≡-cong f _≡_.refl = ≈←≡ _≡_.refl
103
104 -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } →
105 -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b
106 -- cong-≈ eq f = {!!}
107
108 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b}
109 → f o ( g o h ) ≈ ( f o g ) o h
110 assoc = IsCategory.associative (Category.isCategory A)
111
112 -- working on another cateogry
113 assoc1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b}
114 → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ]
115 assoc1 A = IsCategory.associative (Category.isCategory A)
116
117 distr : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
118 { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b }
119 → A [ FMap T ( D [ g o f ] ) ≈ A [ FMap T g o FMap T f ] ]
120 distr T = IsFunctor.distr ( isFunctor T )
121
122 resp : {a b c : Obj A} {f g : Hom A a b} {h i : Hom A b c} → f ≈ g → h ≈ i → (h o f) ≈ (i o g)
123 resp = IsCategory.o-resp-≈ (Category.isCategory A)
124
125 fcong : { c₁ c₂ ℓ : Level} {C : Category c₁ c₂ ℓ}
126 { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj C} {f g : Hom C a b} → (T : Functor C D) → C [ f ≈ g ] → D [ FMap T f ≈ FMap T g ]
127 fcong T = IsFunctor.≈-cong (isFunctor T)
128
129 open NTrans
130 nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′}
131 {a b : Obj D} {f : Hom D a b} {F G : Functor D A }
132 → (η : NTrans D A F G )
133 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ]
134 nat η = IsNTrans.commute ( isNTrans η )
135
136 nat1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′}
137 {a b : Obj D} {F G : Functor D A }
138 → (η : NTrans D A F G ) → (f : Hom D a b)
139 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ]
140 nat1 η f = IsNTrans.commute ( isNTrans η )
141
142 infix 3 _∎
143 infixr 2 _≈⟨_⟩_ _≈⟨⟩_
144 infixr 2 _≈↑⟨_⟩_
145 infix 1 begin_
146
147 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
148 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y
149 -- ≈-to-≡ refl-hom = refl
150
151 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
152 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
153 relTo : (x≈y : x ≈ y ) → x IsRelatedTo y
154
155 begin_ : { a b : Obj A } { x y : Hom A a b } →
156 x IsRelatedTo y → x ≈ y
157 begin relTo x≈y = x≈y
158
159 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } →
160 x ≈ y → y IsRelatedTo z → x IsRelatedTo z
161 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
162
163 _≈↑⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } →
164 y ≈ x → y IsRelatedTo z → x IsRelatedTo z
165 _ ≈↑⟨ y≈x ⟩ relTo y≈z = relTo (trans-hom ( sym y≈x ) y≈z)
166
167 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
168 _ ≈⟨⟩ x∼y = x∼y
169
170 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
171 _∎ _ = relTo refl-hom
172
173
174 ---
175 -- to avoid assoc storm, flatten composition according to the template
176 --
177
178 data MP : { a b : Obj A } ( x : Hom A a b ) → Set (c₁ ⊔ c₂ ⊔ ℓ ) where
179 am : { a b : Obj A } → (x : Hom A a b ) → MP x
180 _repl_by_ : { a b : Obj A } → (x y : Hom A a b ) → x ≈ y → MP y
181 _∙_ : { a b c : Obj A } {x : Hom A b c } { y : Hom A a b } → MP x → MP y → MP ( x o y )
182
183 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
184
185 mp-before : { a b : Obj A } { f : Hom A a b } → MP f → Hom A a b
186 mp-before (am x) = x
187 mp-before (x repl y by x₁) = x
188 mp-before (m ∙ m₁) = mp-before m o mp-before m₁
189
190 mp-after : { a b : Obj A } { f : Hom A a b } → MP f → Hom A a b
191 mp-after (am x) = x
192 mp-after (x repl y by x₁) = y
193 mp-after (m ∙ m₁) = mp-before m o mp-before m₁
194
195 mp≈ : { a b : Obj A } { f g : Hom A a b } → (m : MP f ) → mp-before m ≈ mp-after m
196 mp≈ {a} {b} {f} {g} (am x) = refl-hom
197 mp≈ {a} {b} {f} {g} (x repl y by x=y ) = x=y
198 mp≈ {a} {b} {f} {g} (m ∙ m₁) = resp refl-hom refl-hom
199
200 mpf : {a b c : Obj A } {y : Hom A b c } → (m : MP y ) → Hom A a b → Hom A a c
201 mpf (am x) y = x o y
202 mpf (x repl y by eq ) z = y o z
203 mpf (m ∙ m₁) y = mpf m ( mpf m₁ y )
204
205 mp-flatten : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → Hom A a b
206 mp-flatten m = mpf m (id _)
207
208 mpl1 : {a b c : Obj A } → Hom A b c → {y : Hom A a b } → MP y → Hom A a c
209 mpl1 x (am y) = x o y
210 mpl1 x (z repl y by eq ) = x o y
211 mpl1 x (y ∙ y1) = mpl1 ( mpl1 x y ) y1
212
213 mpl : {a b c : Obj A } {x : Hom A b c } {z : Hom A a b } → MP x → MP z → Hom A a c
214 mpl (am x) m = mpl1 x m
215 mpl (y repl x by eq ) m = mpl1 x m
216 mpl (m ∙ m1) m2 = mpl m (m1 ∙ m2)
217
218 mp-flattenl : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → Hom A a b
219 mp-flattenl m = mpl m (am (id _))
220
221 _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Set c₂
222 _⁻¹ {a} {b} f = Hom A b a
223
224 test1 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → Hom A c a
225 test1 f g _⁻¹ = mp-flattenl ((am (g ⁻¹) ∙ am (f ⁻¹) ) ∙ ( (am f ∙ am g) ∙ am ((f o g) ⁻¹ )))
226
227 test2 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → test1 f g _⁻¹ ≈ ((((g ⁻¹ o f ⁻¹ )o f ) o g ) o (f o g) ⁻¹ ) o id _
228 test2 f g _⁻¹ = refl-hom
229
230 test3 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → Hom A c a
231 test3 f g _⁻¹ = mp-flatten ((am (g ⁻¹) ∙ am (f ⁻¹) ) ∙ ( (am f ∙ am g) ∙ am ((f o g) ⁻¹ )))
232
233 test4 : {a b c : Obj A } ( f : Hom A b c ) ( g : Hom A a b ) → ( _⁻¹ : {a b : Obj A } ( f : Hom A a b ) → Hom A b a ) → test3 f g _⁻¹ ≈ g ⁻¹ o (f ⁻¹ o (f o (g o ((f o g) ⁻¹ o id _))))
234 test4 f g _⁻¹ = refl-hom
235
236 o-flatten : {a b : Obj A } {x : Hom A a b } → (m : MP x ) → x ≈ mp-flatten m
237 o-flatten (am y) = sym-hom (idR )
238 o-flatten (y repl x by eq) = sym-hom (idR )
239 o-flatten (am x ∙ q) = resp ( o-flatten q ) refl-hom
240 o-flatten ((y repl x by eq) ∙ q) = resp ( o-flatten q ) refl-hom
241 -- d <- c <- b <- a ( p ∙ q ) ∙ r , ( x o y ) o z
242 o-flatten {a} {d} (_∙_ {a} {b} {d} {xy} {z} (_∙_ {b} {c} {d} {x} {y} p q) r) =
243 lemma9 _ _ _ ( o-flatten {b} {d} {x o y } (p ∙ q )) ( o-flatten {a} {b} {z} r ) where
244 mp-cong : { a b c : Obj A } → {p : Hom A b c} {q r : Hom A a b} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r
245 mp-cong (am x) q=r = resp q=r refl-hom
246 mp-cong (y repl x by eq) q=r = resp q=r refl-hom
247 mp-cong (P ∙ P₁) q=r = mp-cong P ( mp-cong P₁ q=r )
248 mp-assoc : {a b c d : Obj A } {p : Hom A c d} {q : Hom A b c} {r : Hom A a b} → (P : MP p) → mpf P q o r ≈ mpf P (q o r )
249 mp-assoc (am x) = sym-hom assoc
250 mp-assoc (y repl x by eq ) = sym-hom assoc
251 mp-assoc {_} {_} {_} {_} {p} {q} {r} (P ∙ P₁) = begin
252 mpf P (mpf P₁ q) o r ≈⟨ mp-assoc P ⟩
253 mpf P (mpf P₁ q o r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q o r))
254 ∎
255 lemma9 : (x : Hom A c d) (y : Hom A b c) (z : Hom A a b) → x o y ≈ mpf p (mpf q (id _))
256 → z ≈ mpf r (id _)
257 → (x o y) o z ≈ mp-flatten ((p ∙ q) ∙ r)
258 lemma9 x y z t s = begin
259 (x o y) o z ≈⟨ resp refl-hom t ⟩
260 mpf p (mpf q (id _)) o z ≈⟨ mp-assoc p ⟩
261 mpf p (mpf q (id _) o z) ≈⟨ mp-cong p (mp-assoc q ) ⟩
262 mpf p (mpf q ((id _) o z)) ≈⟨ mp-cong p (mp-cong q idL) ⟩
263 mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩
264 mpf p (mpf q (mpf r (id _)))
265 ∎
266
267 -- an example
268
269 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
270 { a : Obj A } ( b : Obj A ) →
271 ( f : Hom A a b )
272 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ]
273 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c)
274 let open ≈-Reasoning (c) in begin
275 c [ ( Id {_} {_} {_} {c} b ) o g ]
276 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
277 g
278 ∎
279
280 Lemma62 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
281 { a b : Obj A } →
282 ( f g : Hom A a b )
283 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ A [ (Id {_} {_} {_} {A} b) o g ] ]
284 → A [ g ≈ f ]
285 Lemma62 A {a} {b} f g 1g=1f = let open ≈-Reasoning A in
286 begin
287 g
288 ≈↑⟨ idL ⟩
289 id b o g
290 ≈↑⟨ 1g=1f ⟩
291 id b o f
292 ≈⟨ idL ⟩
293 f
294 ∎