--- a/freyd1.agda	Sat Mar 11 16:38:08 2017 +0900
+++ b/freyd1.agda	Sat Mar 11 18:58:21 2017 +0900
@@ -66,54 +66,92 @@
                  ∎
                } }
 
-FIC : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
-FIC {I} Γ = G  ○  (FIA Γ)
+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
+
+revF : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I A )  → Functor I CommaCategory 
+revF = {!!}
+
 
 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
 
 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 Γ))
+    → ( glimit :  ( Γ : Functor I A ) 
+         → ( limita : Limit A I Γ  ) → Limit C I (G ○ Γ) ) 
+    → ( Γ : Functor I CommaCategory ) 
+    → Limit C I (FICG Γ) 
+LimitC  {I} comp glimit Γ = glimit (FIA Γ) (isLimit comp (FIA Γ))
 
-commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  →  Obj CommaCategory
-commaLimit {I} comp Γ = record {
+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Γ Γ )))
+
+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
+commaLimit {I} comp Γ glimit = record {
       obj = limit-c  comp (FIA Γ)
       ; hom = limitHom
    } where
-       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) (NIA Γ {!!} {!!} )) 
+       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 {!!} ]
+            ; isNTrans = {!!}
+          }
        limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom = {!!}
+       limitHom = C [   {!!} o limit (revLimitC comp glimit Γ) (FObj F (limit-c  comp (FIA (revΓ Γ)))) tu ] 
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
-     → (c : Obj CommaCategory )
-     → ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )
-     → NTrans I CommaCategory (K CommaCategory I c) Γ
-commaNat {I} comp  Γ c ta = record {
-       TMap = λ x → tmap x
+     → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
+     → NTrans I CommaCategory (K CommaCategory I {!!}) Γ
+commaNat {I} comp  Γ gilmit = record {
+       TMap = λ x → {!!}
        ; isNTrans = record { commute = {!!} }
     } 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 ) ] ]
-              ; comm = {!!}
-          }
-        commute : {a b : Obj I} {f : Hom I a b} → 
-              CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I c) f ] ]
-        commute {a} {b} {f} = {!!}
 
 
 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
-    → ( G-preserve-limit :  ( Γ : Functor I A ) 
-       ( lim : Obj A ) ( ta : NTrans I A ( K A I lim ) Γ ) → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G  ) )
-    → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I (commaLimit comp Γ) ) Γ ) 
-    → Limit CommaCategory I Γ (commaLimit comp Γ ) ( commaNat comp  Γ (commaLimit comp Γ) ta ) 
-hasLimit {I} comp gpresrve Γ ta  = record {
+    → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
+    → ( Γ : Functor I CommaCategory ) 
+    → Limit CommaCategory I Γ 
+hasLimit {I} comp glimit Γ = record {
+     a0 = {!!} ;
+     t0 = {!!} ;
      limit = λ a t → {!!} ;
      t0f=t = λ {a t i } →  {!!} ;
      limit-uniqueness =  λ {a} {t} f t=f →  {!!}