Mercurial > hg > Members > kono > Proof > category

comparison HomReasoning.agda @ 948:dca4b29553cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mp-flatten
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Aug 2020 10:45:40 +0900
parents ca5eba647990
children
comparison
equal deleted inserted replaced
947:095fd0829ccf 948:dca4b29553cb
167 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y 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 168 _ ≈⟨⟩ x∼y = x∼y
169 169
170 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x 170 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
171 _∎ _ = relTo refl-hom 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 ∎
172 266
173 -- an example 267 -- an example
174 268
175 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → 269 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
176 { a : Obj A } ( b : Obj A ) → 270 { a : Obj A } ( b : Obj A ) →