# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489319886 -32400
# Node ID 016087cfa75a276db53dc7db62f603e634a72817
# Parent  c257347a27f33f4eaa2366962859a7b2566a2183
commaLimit done, commaNat trying..

diff -r c257347a27f3 -r 016087cfa75a freyd1.agda
--- a/freyd1.agda	Sun Mar 12 19:46:07 2017 +0900
+++ b/freyd1.agda	Sun Mar 12 20:58:06 2017 +0900
@@ -66,37 +66,69 @@
    } 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} →
+       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} = ?
+       commute  {a} {b} {f} =  let  open ≈-Reasoning (C) in begin
+             FMap (FICG Γ) f o ( hom (FObj Γ a) o FMap F frev )
+         ≈⟨⟩
+             FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a ))
+         ≈⟨ assoc ⟩
+             (FMap G (arrow (FMap Γ f ) ) o  hom (FObj Γ a)) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a )
+         ≈⟨ car ( comm (FMap Γ f))  ⟩
+              (hom (FObj Γ b) o FMap F (arrow (FMap Γ f)) ) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a )
+         ≈↑⟨ assoc ⟩
+              hom (FObj Γ b) o ( FMap F (arrow (FMap Γ f))  o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a ) )
+         ≈↑⟨  cdr (distr F)  ⟩
+              hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f)  o TMap (t0 ( climit comp (FIA Γ)))  a ] ) )
+         ≈⟨⟩
+              hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ)  f  o TMap (t0 ( climit comp (FIA Γ)))  a ] ) )
+         ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ)))  ))) ⟩
+              hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] ))
+         ≈⟨⟩
+              hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] ))
+         ≈⟨ cdr ( distr F ) ⟩
+              hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ))))
+         ≈⟨ 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
+         ∎
        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} }
+            ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
           }
-       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 = uHomF
+       limitHom = limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) tu
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
-     → ( 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 → {!!}
+     → ( glimit :   LimitPreserve A I C G )
+     → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit))  Γ
+commaNat {I} comp  Γ glimit = record {
+       TMap = λ x → record {
+              arrow =  TMap ( limit-u comp (FIA Γ ) ) x 
+            ; comm  =  comm1 x
+          } 
        ; isNTrans = record { commute = {!!} }
     } 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
+             ?
+         ≈⟨ ? ⟩
+             ?
 
 
 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
-    → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
+    → ( glimit :   LimitPreserve A I C G )
     → ( Γ : Functor I CommaCategory ) 
     → Limit CommaCategory I Γ 
 hasLimit {I} comp glimit Γ = record {
-     a0 = {!!} ;
-     t0 = {!!} ;
+     a0 = commaLimit {I} comp Γ glimit ;
+     t0 = commaNat {  I} comp Γ glimit  ;
      isLimit = record {
              limit = λ a t → {!!} ;
              t0f=t = λ {a t i } →  {!!} ;