--- a/pullback.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/pullback.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -235,9 +235,12 @@
 
 limit2couniv :
      ( lim : ( Γ : Functor I A ) → Limit A I Γ )
-     →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ( lim b) )  ( λ b → t0 (lim b)  )
-limit2couniv lim  = record {  -- F             U                            ε
-       _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; -- η
+     →  coUniversalMapping A ( A ^ I ) 
+limit2couniv lim  = record {  
+       F =  KI I ;
+       U =  λ b → a0 ( lim b) ;
+       ε = λ b → t0 (lim b) ;
+       _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
            couniquness = couniquness2
@@ -263,43 +266,59 @@
 
 open import Category.Cat
 
-
-open coUniversalMapping
-
 univ2limit :
-     ( U : Obj (A ^ I ) → Obj A )
-     ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b )
-     ( univ :  coUniversalMapping A (A ^ I) (KI I) U ε ) →
+     ( univ :  coUniversalMapping A (A ^ I) ) →
      ( Γ : Functor I A ) →   Limit A I Γ 
-univ2limit U ε univ Γ = record {
+univ2limit univ Γ = record {
      a0 = U Γ ;
-     t0 = ε Γ ;
+     t0 = ε ;
      isLimit = record {
              limit = λ a t → limit1 a t ;
              t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
  } where
+     F : Functor A  (A ^ I)
+     F = coUniversalMapping.F univ
+     U : Obj (A ^ I ) → Obj A 
+     U = coUniversalMapping.U univ
+     η : (i : Obj I) → Hom A (U Γ) (FObj (FObj F (U Γ)) i)
+     η i = {!!}
+     ε :  NTrans I A (K A I (U Γ)) Γ 
+     ε  = record {
+         TMap = λ (i : Obj I) → A [ TMap ( coUniversalMapping.ε univ Γ ) i o η i ] ;
+         isNTrans = record { commute = {!!} }
+       }
+     ε' : ( b : Obj (A ^ I ) ) → NTrans I A (FObj F (U b)) b
+     ε' b = coUniversalMapping.ε univ b
+     limit1' :  (a : Obj A) → NTrans I A (FObj F a) Γ → Hom A a (U Γ)
+     limit1' a t = coUniversalMapping._*' univ {_} {a} t
      limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
-     limit1 a t = _*' univ {_} {a} t
+     limit1 a t = coUniversalMapping._*' univ {_} {a} (record {
+          TMap = λ (i : Obj I) → A [ TMap t i o {!!} ] ;
+          isNTrans = record { commute = {!!}
+        } } )
      t0f=t1 :   {a : Obj A} {t : NTrans I A (K A I a) Γ}  {i : Obj I} →
-                A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap ε i o limit1 a t ] ≈ TMap t i ]
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
-            TMap (ε Γ) i o limit1 a t
+            TMap ε i o limit1 a t
         ≈⟨⟩
-            TMap (ε Γ) i o _*' univ {Γ} {a} t
-        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
+            TMap ε i o coUniversalMapping._*' univ {Γ} {a} {!!}
+        -- ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {?} {?} ⟩
+        ≈⟨ {!!} ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)}
-         → ( ∀ { i : Obj I } → A [ A [ TMap  (ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
+         → ( ∀ { i : Obj I } → A [ A [ TMap  ε i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
      limit-uniqueness1 {a} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
-            _*' univ t
-        ≈⟨  ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t  ⟩
+            coUniversalMapping._*' univ {!!}
+        ≈⟨ {!!} ⟩
+        -- ≈⟨  ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t  ⟩
             f
         ∎
 
 
+
 -- another form of uniqueness of a product
 lemma-p0 :   (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : IsProduct A a b ab π1 π2 ) →
       A [ _×_ prod π1 π2 ≈  id1 A ab  ]
@@ -517,11 +536,8 @@
  
 adjoint-preseve-limit :
      { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit B I Γ ) →
-         { U : Functor B A } { F : Functor A B }
-         { η : NTrans A A identityFunctor ( U ○ F ) }
-         { ε : NTrans B B  ( F ○  U ) identityFunctor } →
-       ( adj : Adjunction A B U F η ε  ) →  Limit A I (U ○ Γ) 
-adjoint-preseve-limit B Γ limitb {U} {F} {η} {ε} adj = record {
+       ( adj : Adjunction A B ) →  Limit A I (Adjunction.U adj ○ Γ) 
+adjoint-preseve-limit B Γ limitb adj = record {
      a0 = FObj U lim ;
      t0 = ta1 B Γ lim tb U ;
      isLimit = record {
@@ -530,6 +546,14 @@
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
     } where
+         U : Functor B A
+         U = Adjunction.U adj
+         F : Functor A B 
+         F = Adjunction.F adj
+         η : NTrans A A identityFunctor ( U ○ F ) 
+         η = Adjunction.η adj
+         ε : NTrans B B  ( F ○  U ) identityFunctor  
+         ε = Adjunction.ε adj
          ta = ta1 B Γ (a0 limitb) (t0 limitb) U
          tb = t0 limitb
          lim = a0 limitb