# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489163706 -32400
# Node ID fd752ad25ac0e569f7cca1b85a290220d10c00c1
# Parent  65e6906782bba8484fd1931d7d7b01f2a9b247cb
on going ...

diff -r 65e6906782bb -r fd752ad25ac0 freyd1.agda
--- a/freyd1.agda	Fri Mar 10 23:57:49 2017 +0900
+++ b/freyd1.agda	Sat Mar 11 01:35:06 2017 +0900
@@ -39,37 +39,56 @@
 
 FIA : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I A
 FIA {I} Γ = record {
-        FObj = λ x → obj (FObj Γ x ) ;
-        FMap = λ {a} {b} f →  arrow (FMap Γ f )  ;
-        isFunctor = record {
-             identity = λ{x} → {!!}
-             ; distr = λ {a} {b} {c} {f} {g}   → {!!} 
-             ; ≈-cong = λ {a} {b} {c} {f}   → {!!}
-          }}
+  FObj = λ x → obj (FObj Γ x ) ;
+  FMap = λ {a} {b} f →  arrow (FMap Γ f )  ;
+  isFunctor = record {
+             identity = identity
+             ; distr = IsFunctor.distr (isFunctor Γ) 
+             ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ) 
+          }} where
+      identity :  {x : Obj I } → A [ arrow (FMap Γ (id1 I x)) ≈ id1 A  (obj (FObj Γ x)) ]
+      identity {x} = let  open ≈-Reasoning (A) in begin
+             arrow (FMap Γ (id1 I x)) 
+         ≈⟨ IsFunctor.identity (isFunctor Γ)   ⟩
+             id1 A  (obj (FObj Γ x))     
+         ∎
 
-commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  → Obj CommaCategory
+
+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 )
+
+commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  →  Obj CommaCategory
 commaLimit {I} comp Γ = record {
       obj = limit-c  comp (FIA Γ)
       ; hom = limitHom
    } where
+       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) {!!})
        limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom =  C [ FMap G ( limit (isLimit comp (FIA Γ)) {!!} {!!} )   o  {!!}   ]
+       limitHom = C [ FMap G ll   o C [ {!!} o FMap F ll ] ]
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
-     → ( ta : NTrans I CommaCategory ( K CommaCategory I (commaLimit comp Γ) ) Γ )
-     → NTrans I CommaCategory (K CommaCategory I (commaLimit comp Γ)) Γ
-commaNat {I} comp  Γ ta = record {
+     → (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
        ; isNTrans = record { commute = {!!} }
     } where
-        tmap :  (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I (commaLimit comp Γ)) i) (FObj Γ i)
+        tmap :  (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i)
         tmap i = record {
-              arrow = A [ {!!} o  limit ( isLimit comp (FIA Γ ) ) {!!} {!!} ]
+              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 (commaLimit comp Γ)) f ] ]
+              CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I c) f ] ]
         commute {a} {b} {f} = {!!}
 
 
@@ -77,7 +96,7 @@
     → ( 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  Γ ta ) 
+    → Limit CommaCategory I Γ (commaLimit comp Γ ) ( commaNat comp  Γ (commaLimit comp Γ) ta ) 
 hasLimit {I} comp gpresrve Γ ta  = record {
      limit = λ a t → {!!} ;
      t0f=t = λ {a t i } →  {!!} ;