Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 27:d9c2386a18a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jul 2013 22:17:23 +0900
parents ad62c87659ef
children 5289c46d8eef
comparison
equal deleted inserted replaced
26:ad62c87659ef 27:d9c2386a18a8
179 179
180 infixr 2 _∎ 180 infixr 2 _∎
181 infixr 2 _≈⟨_⟩_ 181 infixr 2 _≈⟨_⟩_
182 infix 1 begin_ 182 infix 1 begin_
183 183
184 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
185 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } -> A [ x ≈ y ] -> x ≡ y
186 -- ≈-to-≡ refl-hom = refl
184 187
185 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : 188 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
186 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where 189 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
187 relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y 190 relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
188 191
288 join k d h ( A [ Trans μ c o A [ FMap T g o f ] ] ) 291 join k d h ( A [ Trans μ c o A [ FMap T g o f ] ] )
289 ≈⟨ refl-hom ⟩ 292 ≈⟨ refl-hom ⟩
290 A [ Trans μ d o A [ FMap T h o A [ Trans μ c o A [ FMap T g o f ] ] ] ] 293 A [ Trans μ d o A [ FMap T h o A [ Trans μ c o A [ FMap T g o f ] ] ] ]
291 ≈⟨ cdr-eq ( Trans μ d ) ( cdr-eq ( FMap T h ) ( assoc )) ⟩ 294 ≈⟨ cdr-eq ( Trans μ d ) ( cdr-eq ( FMap T h ) ( assoc )) ⟩
292 A [ Trans μ d o A [ FMap T h o A [ A [ Trans μ c o FMap T g ] o f ] ] ] 295 A [ Trans μ d o A [ FMap T h o A [ A [ Trans μ c o FMap T g ] o f ] ] ]
293 ≈⟨ assoc ⟩ --- A [ f x A [ g x h ] ] = A [ A [ f x g ] x h ] 296 ≈⟨ assoc ⟩ --- A [ f o A [ g o h ] ] = A [ A [ f o g ] o h ]
294 A [ A [ Trans μ d o FMap T h ] o A [ A [ Trans μ c o FMap T g ] o f ] ] 297 A [ A [ Trans μ d o FMap T h ] o A [ A [ Trans μ c o FMap T g ] o f ] ]
295 ≈⟨ assoc ⟩ 298 ≈⟨ assoc ⟩
296 A [ A [ A [ Trans μ d o FMap T h ] o A [ Trans μ c o FMap T g ] ] o f ] 299 A [ A [ A [ Trans μ d o FMap T h ] o A [ Trans μ c o FMap T g ] ] o f ]
297 ≈⟨ car-eq f (sym assoc) ⟩ 300 ≈⟨ car-eq f (sym assoc) ⟩
298 A [ A [ Trans μ d o A [ FMap T h o A [ Trans μ c o FMap T g ] ] ] o f ] 301 A [ A [ Trans μ d o A [ FMap T h o A [ Trans μ c o FMap T g ] ] ] o f ]
313 A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o A [ FMap T ( FMap T h ) o FMap T g ] ] ] o f ] 316 A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o A [ FMap T ( FMap T h ) o FMap T g ] ] ] o f ]
314 ≈⟨ car-eq f ( cdr-eq ( Trans μ d) (cdr-eq (Trans μ ( FObj T d) ) (sym (distr T )))) ⟩ 317 ≈⟨ car-eq f ( cdr-eq ( Trans μ d) (cdr-eq (Trans μ ( FObj T d) ) (sym (distr T )))) ⟩
315 A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( A [ FMap T h o g ] ) ] ] o f ] 318 A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( A [ FMap T h o g ] ) ] ] o f ]
316 ≈⟨ car-eq f assoc ⟩ 319 ≈⟨ car-eq f assoc ⟩
317 A [ A [ A [ Trans μ d o Trans μ ( FObj T d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] 320 A [ A [ A [ Trans μ d o Trans μ ( FObj T d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ]
318 ≈⟨ car-eq f ( car-eq (FMap T ( A [ FMap T h o g ] )) ( IsMonad.assoc ( isMonad m ))) ⟩ 321 ≈⟨ car-eq f ( car-eq (FMap T ( A [ FMap T h o g ] )) (
322 begin
323 A [ Trans μ d o Trans μ (FObj T d) ]
324 ≈⟨ IsMonad.assoc ( isMonad m) ⟩
325 A [ Trans μ d o FMap T (Trans μ d) ]
326 ∎
327 )) ⟩
319 A [ A [ A [ Trans μ d o FMap T ( Trans μ d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] 328 A [ A [ A [ Trans μ d o FMap T ( Trans μ d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ]
320 ≈⟨ car-eq f (sym assoc) ⟩ 329 ≈⟨ car-eq f (sym assoc) ⟩
321 A [ A [ Trans μ d o A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] ] o f ] 330 A [ A [ Trans μ d o A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] ] o f ]
322 ≈⟨ sym assoc ⟩ 331 ≈⟨ sym assoc ⟩
323 A [ Trans μ d o A [ A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] o f ] ] 332 A [ Trans μ d o A [ A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] o f ] ]