--- a/freyd1.agda	Sat Mar 11 10:51:12 2017 +0900
+++ b/freyd1.agda	Sat Mar 11 16:38:08 2017 +0900
@@ -17,20 +17,6 @@
 open NTrans
 
 
-tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B ) 
-     ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → 
-         ( U : Functor B C)  → NTrans I C ( K C I (FObj U lim) ) (U  ○  Γ)
-tb B I Γ lim tb U = record {
-               TMap  = TMap (Functor*Nat I C U tb) ; 
-               isNTrans = record { commute = λ {a} {b} {f} → let  open ≈-Reasoning (C) in begin
-                     FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a 
-                 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
-                     TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f 
-                 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
-                     TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
-                 ∎
-               } }
-
 open Complete
 open CommaObj
 open CommaHom
@@ -66,55 +52,42 @@
              A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ]
         comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
 
+tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B ) 
+     ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → 
+         ( U : Functor B C)  → NTrans I C ( K C I (FObj U lim) ) (U  ○  Γ)
+tb B I Γ lim tb U = record {
+               TMap  = TMap (Functor*Nat I C U tb) ; 
+               isNTrans = record { commute = λ {a} {b} {f} → let  open ≈-Reasoning (C) in begin
+                     FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a 
+                 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
+                     TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f 
+                 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
+                     TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
+                 ∎
+               } }
+
+FIC : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
+FIC {I} Γ = G  ○  (FIA Γ)
+
 NIC : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
      (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I C ( K C I (FObj G (obj c)) ) (G ○ ( FIA Γ) )
-NIC  {I} Γ c ta = record {
-        TMap = λ x → FMap G (TMap ta x )
-        ; isNTrans = record { commute = comm1 }
-    }  where
-          comm1 :  {a b : Obj I} {f : Hom I a b} → 
-                C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ] 
-          comm1 {a} {b} {f} = let  open ≈-Reasoning (C) in begin
-                 FMap (G ○ FIA Γ) f o FMap G (TMap ta a)
-              ≈↑⟨ distr G  ⟩
-                 FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] )
-              ≈⟨ fcong G  ( nat ta  ) ⟩
-                 FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] )
-              ≈⟨ distr G  ⟩
-                 FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f  )
-              ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩
-                 FMap G (TMap ta b) o id1 C (FObj G (obj c))
-              ≈⟨⟩
-                 FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f
-              ∎
+NIC  {I} Γ c ta = tb A I (FIA Γ) (obj c) ta G
 
-
-NIComma : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
-     (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I CommaCategory ( K CommaCategory I c )  Γ
-NIComma  {I} Γ c ta = record {
-        TMap = λ x → record {
-                 arrow =  TMap ta x
-              ;  comm =  comm1 x
-            }
-        ; isNTrans = record { commute = {!!} }
-    }  where
-        comm1 :  ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ] 
-        comm1 x = let  open ≈-Reasoning (C) in begin
-              FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x)
-           ≈⟨ {!!} ⟩
-              hom (FObj Γ x) o FMap F (TMap ta x) 
-           ∎
-
-
+LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
+    → ( Glimit :  ( Γ : Functor I A ) (lim  : Obj A )
+         → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G  ) )
+    → ( lim : Obj CommaCategory ) → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I ? ) Γ )
+    → Limit C I (FIC Γ) {!!} ( NIC Γ {!!} (NIA Γ {!!} ta) )
+LimitC  {I} comp Glimit lim Γ ta = Glimit (FIA Γ) {!!} (NIA Γ {!!} ta ) (isLimit comp (FIA Γ))
 
 commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  →  Obj CommaCategory
 commaLimit {I} comp Γ = record {
       obj = limit-c  comp (FIA Γ)
       ; hom = limitHom
    } where
-       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) {!!})
+       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) (NIA Γ {!!} {!!} )) 
        limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom = C [ FMap G ll   o C [ {!!} o FMap F ll ] ]
+       limitHom = {!!}
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
@@ -127,7 +100,7 @@
     } where
         tmap :  (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i)
         tmap i = record {
-              arrow = A [ arrow ( TMap ta i)  o  A [  {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
+              arrow = A [ arrow ( TMap ta i)  o  A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
               ; comm = {!!}
           }
         commute : {a b : Obj I} {f : Hom I a b} →