--- a/freyd1.agda	Sun Mar 12 14:48:14 2017 +0900
+++ b/freyd1.agda	Sun Mar 12 19:46:07 2017 +0900
@@ -21,6 +21,7 @@
 open CommaObj
 open CommaHom
 open Limit
+open IsLimit
 
 --  F : A → C
 --  G : A → C
@@ -42,138 +43,42 @@
              id1 A  (obj (FObj Γ x))     
          ∎
 
-NIA : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
-     (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )  → NTrans I A ( K A I (obj c) )  (FIA Γ)
-NIA  {I} Γ c ta = record {
-        TMap = λ x → arrow (TMap ta x )
-        ; isNTrans = record { commute = comm1 }
-    }  where
-        comm1 : {a b : Obj I} {f : Hom I a b} → 
-             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
-                 ∎
-               } }
-
 FICG : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
 FICG {I} Γ = G  ○  (FIA Γ)
 
 FICF : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
 FICF {I} Γ = F  ○  (FIA Γ)
 
-FINAT : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory ) → NTrans I C (FICF Γ) (FICG Γ)
-FINAT {I} Γ = record {
-       TMap = λ i → tmap i
-     ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } 
-   } where
-        tmap :  (i : Obj I ) → Hom C (FObj (FICF Γ) i) (FObj (FICG Γ) i)
-        tmap i = hom (FObj Γ i )
-        commute : {a b : Obj I} → {f : Hom I a b} → C [ C [ FMap (FICG Γ) f o tmap a ] ≈ C [ tmap b o FMap (FICF Γ) f ] ]
-        commute {a} {b} {f} = comm ( FMap Γ f )
-
-revΓ : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I CommaCategory 
-revΓ {I} Γ = record {
-  FObj = λ x → record {
-          obj = obj ( FObj Γ x )
-        ; hom = TMap (FINAT Γ) x
-     }
-  ; FMap = λ {a} {b} f →  record {
-            arrow = arrow ( FMap Γ f )
-          ; comm = IsNTrans.commute ( isNTrans (FINAT Γ) )
-      }
-  ; isFunctor = record {
-             identity = IsFunctor.identity ( isFunctor Γ )
-             ; distr = IsFunctor.distr ( isFunctor Γ )
-             ; ≈-cong = IsFunctor.≈-cong ( isFunctor Γ )
-          }} where
-
-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 = tb A I (FIA Γ) (obj c) ta G
+open LimitPreserve
 
 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
-    → ( glimit :  ( Γ : Functor I A ) 
-         → ( limita : Limit A I Γ  ) → Limit C I (G ○ Γ) ) 
     → ( Γ : Functor I CommaCategory ) 
+    → ( glimit :  LimitPreserve A I  C G )
     → Limit C I (FICG Γ) 
-LimitC  {I} comp glimit Γ = glimit (FIA Γ) (isLimit comp (FIA Γ))
-
-revLimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
-    → ( glimit :  ( Γ : Functor I A ) 
-         → ( limita : Limit A I Γ  ) → Limit C I (G ○ Γ) ) 
-    → ( Γ : Functor I CommaCategory ) 
-    → Limit C I ( G  ○ (FIA (revΓ Γ) )) 
-revLimitC  {I} comp glimit Γ = glimit (FIA (revΓ Γ)) (isLimit comp (FIA (revΓ Γ )))
-
-
-a0F : ( I : Category c₁ c₂ ℓ ) →  (a1 : Obj A) → Functor I A 
-a0F  I a1 =  record {
-  FObj = λ x →  a1
-  ; FMap = λ {a} {b} f →  id1 A a1
-  ; isFunctor = record {
-             identity = let  open ≈-Reasoning (A) in refl-hom
-             ; distr =  let  open ≈-Reasoning (A) in ( sym idL )
-             ; ≈-cong = λ _ →  let  open ≈-Reasoning (A) in refl-hom
-          }} where
-
-t0F :  ( I : Category c₁ c₂ ℓ ) →  (a1 : Obj A ) 
-    → NTrans I A (K A I a1 ) (a0F I a1 )
-t0F  I a1  = record {
-     TMap = λ i → id1 A a1 
-     ; isNTrans = record { commute = λ {a b f} → commute {a} {b} {f} }
-  } where
-      commute : {a b : Obj I} {f : Hom I a b} → A [
-        A [ FMap (a0F I a1  ) f o id1 A a1 ] ≈
-        A [ id1 A a1 o FMap (K A I a1) f ] ]
-      commute {a} {b} {f} =   let  open ≈-Reasoning (A) in begin
-              FMap (a0F I a1 ) f o id1 A a1
-         ≈⟨ idR ⟩
-              FMap (a0F I a1  ) f 
-         ≈⟨⟩
-              id1 A a1
-         ≈⟨⟩
-              FMap (K A I a1) f 
-         ≈↑⟨ idL ⟩
-              id1 A a1 o FMap (K A I a1) f 
-         ∎
-
-hoge :  ( a : Obj A ) →   ( I : Category c₁ c₂ ℓ ) → (comp : Complete A I ) → ∀ { i : Obj I } →  
-     A [ A [ TMap ( limit-u comp (a0F I a)) i o  limit (isLimit comp (a0F I a)) a (t0F I a) ]  ≈ id1 A a ]
-hoge a I comp {i} = t0f=t (isLimit comp (a0F I a)) 
-
+LimitC  {I} comp Γ glimit  = plimit glimit (FIA Γ) (climit comp (FIA Γ))
 
 commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  
-     → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
-     →  Obj CommaCategory
+    → ( glimit :  LimitPreserve A I C G )
+    →  Obj CommaCategory
 commaLimit {I} comp Γ glimit = record {
       obj = limit-c  comp (FIA Γ)
       ; hom = limitHom
    } where
        frev : {i : Obj I } → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
-       frev {i} = TMap (t0 ( isLimit comp (FIA Γ)))  i
+       frev {i} = TMap (t0 ( climit comp (FIA Γ)))  i
+       commute : {a b : Obj I} {f : Hom I a b} →
+              C [ C [ FMap (FICG Γ) f o C [ hom (FObj Γ a) o FMap F frev ] ] 
+            ≈ C [ C [ hom (FObj Γ b) o FMap F frev ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ]
+       commute  {a} {b} {f} = ?
        tu : NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ)
        tu  = record {
               TMap  = λ i →  C [ hom ( FObj Γ i ) o  FMap F frev ]
-            ; isNTrans = {!!}
+            ; isNTrans = record { commute = λ {a} {b} {f}→ commute {a} {b} {f} }
           }
-       forward :  Hom C  (FObj G (limit-c comp (FIA Γ))) (a0 (LimitC comp glimit Γ))
-       forward = limit (LimitC comp glimit Γ) (FObj G (limit-c  comp (FIA Γ))) 
-            ( record { TMap = λ i →  C [ FMap G frev  o {!!} ]  ; isNTrans = {!!} } ) 
-       rev :  Hom C (a0 (LimitC comp glimit Γ)) (FObj G (limit-c comp (FIA Γ)))
-       rev = C [ FMap G {!!} o TMap (t0 (LimitC comp glimit Γ)) {!!} ]
+       uHomF :  Hom C  ( FObj F ( limit-c  comp (FIA Γ) )  ) (FObj G ( (a0 (climit comp (FIA Γ) ))))
+       uHomF  =  limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) tu
        limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom = C [  rev o limit (LimitC comp glimit Γ) (FObj F (limit-c  comp (FIA Γ))) tu ] 
+       limitHom = uHomF
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
@@ -192,7 +97,9 @@
 hasLimit {I} comp glimit Γ = record {
      a0 = {!!} ;
      t0 = {!!} ;
-     limit = λ a t → {!!} ;
-     t0f=t = λ {a t i } →  {!!} ;
-     limit-uniqueness =  λ {a} {t} f t=f →  {!!}
+     isLimit = record {
+             limit = λ a t → {!!} ;
+             t0f=t = λ {a t i } →  {!!} ;
+             limit-uniqueness =  λ {a} {t} f t=f →  {!!}
+     }
    }