# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489197072 -32400
# Node ID 265f13adf93b304dccbada0df5dd0bd5ede121a1
# Parent  fd752ad25ac0e569f7cca1b85a290220d10c00c1
add NIC

diff -r fd752ad25ac0 -r 265f13adf93b freyd1.agda
--- a/freyd1.agda	Sat Mar 11 01:35:06 2017 +0900
+++ b/freyd1.agda	Sat Mar 11 10:51:12 2017 +0900
@@ -32,11 +32,14 @@
                } }
 
 open Complete
-
 open CommaObj
 open CommaHom
 open Limit
 
+--  F : A → C
+--  G : A → C
+-- 
+
 FIA : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I A
 FIA {I} Γ = record {
   FObj = λ x → obj (FObj Γ x ) ;
@@ -53,7 +56,6 @@
              id1 A  (obj (FObj Γ x))     
          ∎
 
-
 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 {
@@ -64,6 +66,47 @@
              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 )
 
+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 = record {
+        TMap = λ x → FMap G (TMap ta x )
+        ; isNTrans = record { commute = comm1 }
+    }  where
+          comm1 :  {a b : Obj I} {f : Hom I a b} → 
+                C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ] 
+          comm1 {a} {b} {f} = let  open ≈-Reasoning (C) in begin
+                 FMap (G ○ FIA Γ) f o FMap G (TMap ta a)
+              ≈↑⟨ distr G  ⟩
+                 FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] )
+              ≈⟨ fcong G  ( nat ta  ) ⟩
+                 FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] )
+              ≈⟨ distr G  ⟩
+                 FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f  )
+              ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩
+                 FMap G (TMap ta b) o id1 C (FObj G (obj c))
+              ≈⟨⟩
+                 FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f
+              ∎
+
+
+NIComma : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
+     (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I CommaCategory ( K CommaCategory I c )  Γ
+NIComma  {I} Γ c ta = record {
+        TMap = λ x → record {
+                 arrow =  TMap ta x
+              ;  comm =  comm1 x
+            }
+        ; isNTrans = record { commute = {!!} }
+    }  where
+        comm1 :  ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ] 
+        comm1 x = let  open ≈-Reasoning (C) in begin
+              FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x)
+           ≈⟨ {!!} ⟩
+              hom (FObj Γ x) o FMap F (TMap ta x) 
+           ∎
+
+
+
 commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  →  Obj CommaCategory
 commaLimit {I} comp Γ = record {
       obj = limit-c  comp (FIA Γ)