# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374518396 -32400
# Node ID 0124e3c971e50362289df998088ca290f82045ee
# Parent  5d1b0fd2ad213a3cb934fd679dd4905abaf1994c
F is Functor proved.

diff -r 5d1b0fd2ad21 -r 0124e3c971e5 universal-mapping.agda
--- a/universal-mapping.agda	Tue Jul 23 02:57:11 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 03:39:56 2013 +0900
@@ -177,10 +177,34 @@
               a (F b) (A [ η b  o  f ])  ((_* um) (A [ η b  o  g ])) ( lemma-cong2 a b f g eq )
     lemma-cong :  {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ]
     lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq
+    lemma-distr2 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → 
+            A [ A [ FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ])  o  η a ] ≈ (A [ η c o A [ g o f ] ]) ]
+    lemma-distr2 a b c f g = let open ≈-Reasoning (A) in
+       begin
+           ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] ) )  o  η a 
+       ≈⟨ car (IsFunctor.distr ( isFunctor U ))  ⟩
+           (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b  o f ])))) )   o  η a 
+       ≈⟨ sym assoc ⟩
+           ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b  o f ]))))   o  η a )
+       ≈⟨ cdr ( ( IsUniversalMapping.universalMapping ( isUniversalMapping um )) a (F b)) ⟩
+           ( FMap U ((_* um) (A [ η c o g ])) o ( η b  o f) )
+       ≈⟨ assoc ⟩
+           ( FMap U ((_* um) (A [ η c o g ])) o  η b)  o f
+       ≈⟨ car (( IsUniversalMapping.universalMapping ( isUniversalMapping um )) b (F c)) ⟩
+           (  η c o g )  o f
+       ≈⟨ sym assoc  ⟩
+            η c o ( g o f )
+       ∎
+    lemma-distr1 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → 
+            B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] )]
+    lemma-distr1 a b c f g =  ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) a (F c)
+              (A [ η c o A [ g o f ] ]) ((B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] )) ) (lemma-distr2 a b c f g )
+    lemma-distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )]
+    lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g 
     myIsFunctor : IsFunctor A B F myFMap
     myIsFunctor =
       record { ≈-cong   = lemma-cong
              ; identity = lemma-id
-             ; distr    = {!!}
+             ; distr    = lemma-distr
              }