# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1380112780 -32400
# Node ID 61669ac03e7d337aa42ee466d05bae90aade7892
# Parent  537570f6a44fb4e5b33375778e561832438b75af
fix

diff -r 537570f6a44f -r 61669ac03e7d pullback.agda
--- a/pullback.agda	Wed Sep 25 21:12:29 2013 +0900
+++ b/pullback.agda	Wed Sep 25 21:39:40 2013 +0900
@@ -237,6 +237,12 @@
 
 ---------
 --
+--   Limit    Constancy Functor F : A → A^I     has right adjoint
+--
+--   we are going to prove universal mapping
+
+---------
+--
 -- limit gives co universal mapping ( i.e. adjunction )
 --
 --     F = KI I : Functor A (A ^ I)
@@ -320,6 +326,7 @@
       product : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
       pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( product qi ) ] ≈  (qi i) ]
       -- special case of product ( qi = pi ) ( should b proved from pif=q )
+      --   we cannot prove this because qi/pi cannot be interleaved , should be the way to prove
       pif=q1 :   { i : I } → { qi :  Hom A p (ai i) } → A [ pi i ≈  qi ]
       ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
       ip-cong : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
@@ -546,7 +553,7 @@
                ≈⟨⟩
                  FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a  
                ≈⟨ car ( fcong U (limit-uniqueness limitb ( λ {i} →  lemma1 i) )) ⟩
-                 FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a  
+                 FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a   -- Universal mapping 
                ≈⟨ car (distr U ) ⟩
                  ( (FMap U (TMap ε lim))  o (FMap U ( FMap F f )) ) o TMap η a
                ≈⟨ sym assoc ⟩