# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489369267 -32400
# Node ID 04da2c458d44b7a5f2ebce79272ee2780020d955
# Parent  1a42f06e7ae15d14ec30c19631bd311efd04913d
comma-a0 commuativity remains

diff -r 1a42f06e7ae1 -r 04da2c458d44 freyd1.agda
--- a/freyd1.agda	Mon Mar 13 09:51:44 2017 +0900
+++ b/freyd1.agda	Mon Mar 13 10:41:07 2017 +0900
@@ -43,31 +43,39 @@
              id1 A  (obj (FObj Γ x))     
          ∎
 
-FICG : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
-FICG {I} Γ = G  ○  (FIA Γ)
+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 )
+
 
 open LimitPreserve
 
 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
     → ( Γ : Functor I CommaCategory ) 
     → ( glimit :  LimitPreserve A I  C G )
-    → Limit C I (FICG Γ) 
+    → Limit C I (G  ○  (FIA Γ)) 
 LimitC  {I} comp Γ glimit  = plimit glimit (FIA Γ) (climit comp (FIA Γ))
 
 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 Γ)
+    →   NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G  ○  (FIA Γ))
 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 [ FMap (G  ○  (FIA Γ)) 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  ○  (FIA Γ)) 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 ⟩
@@ -139,6 +147,43 @@
               TMap (limit-u comp (FIA Γ)) b  o FMap (K A I (limit-c comp (FIA Γ))) f 
          ∎
 
+comma-a0 :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
+     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit)
+comma-a0  {I} comp Γ glimit a t = record {
+       arrow  = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
+     ; comm = comm1
+   } where
+      comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ]
+        ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ]
+      comm1 =  let  open ≈-Reasoning (C) in begin
+            FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a 
+         ≈⟨ {!!} ⟩
+            limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )  o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
+         ≈⟨⟩
+            hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
+         ∎
+
+comma-t0f=t :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
+     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) (i : Obj I )
+     →   CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ]
+comma-t0f=t  {I} comp Γ glimit a t i = let  open ≈-Reasoning (A) in begin
+             TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
+         ≈⟨ t0f=t (isLimit ( climit comp (FIA Γ) ) )  ⟩
+             TMap (NIA  {I} Γ a t ) i
+         ∎
+
+
+comma-uniqueness :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
+     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) 
+     →  ( f :  Hom CommaCategory a  (commaLimit comp Γ glimit)) 
+     →   ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat {  I} comp Γ glimit ) i o  f ]  ≈ TMap t i ] )
+     → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ]
+comma-uniqueness  {I} comp Γ glimit a t f t=f    = let  open ≈-Reasoning (A) in begin
+             limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
+         ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) (arrow f)  t=f ⟩
+             arrow f
+         ∎
+
 
 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
     → ( glimit :   LimitPreserve A I C G )
@@ -148,8 +193,8 @@
      a0 = commaLimit {I} comp Γ glimit ;
      t0 = commaNat {  I} comp Γ glimit  ;
      isLimit = record {
-             limit = λ a t → {!!} ;
-             t0f=t = λ {a t i } →  {!!} ;
-             limit-uniqueness =  λ {a} {t} f t=f →  {!!}
+             limit = λ a t → comma-a0 comp Γ glimit a t ;
+             t0f=t = λ {a t i } →  comma-t0f=t  comp Γ glimit a t i ;
+             limit-uniqueness =  λ {a} {t} f t=f →  comma-uniqueness  {I} comp Γ glimit a t f t=f
      }
    }