Mercurial > hg > Members > kono > Proof > category

changeset 62:c5277284919e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
assoc proved.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2013 11:43:51 +0900
parents af7ddd9f9122
children 97eb12318048
files nat.agda
diffstat 1 files changed, 17 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Wed Jul 24 23:23:56 2013 +0900
+++ b/nat.agda	Thu Jul 25 11:43:51 2013 +0900
@@ -288,8 +288,24 @@
            T = U  ○ F
            μ : NTrans A A ( T ○ T ) T
            μ = UεF A B U F ε
+           lemma-assoc1 : (b : Obj B) → B [ B [ TMap ε b o TMap ε ( FObj F ( FObj U b)) ] ≈ 
+                                            B [ TMap ε b o FMap F  (FMap U (TMap ε b)) ] ] 
+           lemma-assoc1 b =  IsNTrans.naturality ( isNTrans ε )
            assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-           assoc1 = {!!}
+           assoc1 {a} = let open ≈-Reasoning (A) in
+             begin
+                TMap μ a o TMap μ ( FObj T a )
+             ≈⟨⟩
+                (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F  a )))))
+             ≈⟨ sym (IsFunctor.distr (isFunctor U)) ⟩
+                FMap U (B [ TMap ε ( FObj F a )  o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
+             ≈⟨  (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( FObj F a )) ⟩
+                FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
+             ≈⟨ IsFunctor.distr (isFunctor U) ⟩
+                (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
+             ≈⟨⟩
+                TMap μ a o FMap T (TMap μ a) 
+             ∎
            unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
            unity1 {a} = let open ≈-Reasoning (A) in
              begin