# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489324254 -32400
# Node ID 75a60ceb55af717c9328416cecf6f684fd8a8c7d
# Parent  016087cfa75a276db53dc7db62f603e634a72817
on going ..

diff -r 016087cfa75a -r 75a60ceb55af freyd1.agda
--- a/freyd1.agda	Sun Mar 12 20:58:06 2017 +0900
+++ b/freyd1.agda	Sun Mar 12 22:10:54 2017 +0900
@@ -57,20 +57,20 @@
     → Limit C I (FICG Γ) 
 LimitC  {I} comp Γ glimit  = plimit glimit (FIA Γ) (climit comp (FIA Γ))
 
-commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I 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 ( 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} =  let  open ≈-Reasoning (C) in begin
-             FMap (FICG Γ) f o ( hom (FObj Γ a) o FMap F frev )
+frev :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory ) (i : Obj I ) → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
+frev comp Γ i = TMap (t0 ( climit comp (FIA Γ)))  i
+
+tu :  { I : Category c₁ c₂ ℓ } →  ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
+    →   NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ)
+tu {I} comp Γ = record {
+      TMap  = λ i →  C [ hom ( FObj Γ i ) o  FMap F (frev comp Γ i) ]
+    ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
+  } where
+        commute : {a b : Obj I} {f : Hom I a b}   →
+              C [ C [ FMap (FICG Γ) f o C [ hom (FObj Γ a) o FMap F (frev comp Γ a) ] ] 
+            ≈ C [ C [ hom (FObj Γ b) o FMap F (frev comp Γ b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ]
+        commute  {a} {b} {f} =  let  open ≈-Reasoning (C) in begin
+             FMap (FICG Γ) f o ( hom (FObj Γ a) o FMap F (frev comp Γ a) )
          ≈⟨⟩
              FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a ))
          ≈⟨ assoc ⟩
@@ -92,15 +92,19 @@
          ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩
               hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ))))
          ≈⟨ assoc ⟩
-             ( hom (FObj Γ b) o FMap F frev ) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f
+             ( hom (FObj Γ b) o FMap F (frev comp Γ b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) 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 = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
-          }
-       limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom = limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) tu
+limitHom :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory )
+    → ( glimit :  LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
+limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )
+
+commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  
+    → ( glimit :  LimitPreserve A I C G )
+    →  Obj CommaCategory
+commaLimit {I} comp Γ glimit = record {
+      obj = limit-c  comp (FIA Γ)
+      ; hom = limitHom comp Γ glimit
+   } 
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
@@ -109,17 +113,34 @@
 commaNat {I} comp  Γ glimit = record {
        TMap = λ x → record {
               arrow =  TMap ( limit-u comp (FIA Γ ) ) x 
-            ; comm  =  comm1 x
+            ; comm  = comm1 x
           } 
-       ; isNTrans = record { commute = {!!} }
+       ; isNTrans = record { commute = comm2 }
     } where
        comm1 : (x : Obj I )  →
               C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] 
             ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] 
        comm1 x =  let  open ≈-Reasoning (C) in begin
-             ?
-         ≈⟨ ? ⟩
-             ?
+              FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x)
+         ≈⟨⟩
+              FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) 
+         ≈⟨⟩
+              FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )
+         ≈⟨⟩
+              TMap (t0 ( LimitC comp Γ glimit )) x  o limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )
+         ≈⟨ t0f=t ( isLimit (  LimitC comp Γ glimit ) ) ⟩
+              TMap (tu comp Γ) x 
+         ≈⟨⟩
+              hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x)
+         ∎
+       comm2 : {a b : Obj I} {f : Hom I a b} →
+          CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ]
+          ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ]
+       comm2 {a} {b} {f} =  let  open ≈-Reasoning (CommaCategory) in begin
+             FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } 
+         ≈⟨ {!!} ⟩
+             record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f 
+         ∎
 
 
 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )