# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489378960 -32400
# Node ID c7b8017bcd4d2e3264a3a8f73112d689ddc529b8
# Parent  04da2c458d44b7a5f2ebce79272ee2780020d955
on going..

diff -r 04da2c458d44 -r c7b8017bcd4d Comma.agda
--- a/Comma.agda	Mon Mar 13 10:41:07 2017 +0900
+++ b/Comma.agda	Mon Mar 13 13:22:40 2017 +0900
@@ -39,6 +39,7 @@
 _∙_ :  {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c
 _∙_ {a} {b} {c} f g = record { 
          arrow = A [ arrow f o arrow g ] ;
+         arrowg = B [ arrowg f o arrowg g ] ;
          comm  = comm1
      } where
         comm1 :  C [ C [ FMap G (B [ arrowg f o arrowg g ] ) o hom a ]  ≈ C [ hom c  o  FMap F (A [ arrow f o arrow g ]) ]  ]
@@ -61,7 +62,7 @@
            ∎ 
 
 CommaId : { a : CommaObj } → CommaHom a a
-CommaId {a} = record {  arrow = id1 A ( obj a ) ;  
+CommaId {a} = record {  arrow = id1 A ( obj a ) ;  arrowg = id1 B ( objb a ) ;  
       comm = comm2 } where
         comm2 :  C [ C [ FMap G (id1 B (objb a)) o hom a ]  ≈ C [ hom a  o  FMap F (id1 A (obj a)) ]  ]
         comm2 =  let open ≈-Reasoning C in begin
diff -r 04da2c458d44 -r c7b8017bcd4d cat-utility.agda
--- a/cat-utility.agda	Mon Mar 13 10:41:07 2017 +0900
+++ b/cat-utility.agda	Mon Mar 13 13:22:40 2017 +0900
@@ -341,8 +341,8 @@
           field
              preserve :  ( Γ : Functor I A ) → ( limita : Limit A I Γ  ) → 
                    IsLimit C I (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat A I C Γ (a0 limita ) (t0 limita) G )
-          plimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ  ) →  Limit C I (G  ○ Γ  )
-          plimit Γ limita =  record { a0 = (FObj G (a0 limita ))
+          plimit :  { Γ : Functor I A } → ( limita : Limit A I Γ  ) →  Limit C I (G  ○ Γ  )
+          plimit {Γ} limita =  record { a0 = (FObj G (a0 limita ))
              ; t0 =  LimitNat A I C Γ (a0 limita ) (t0 limita) G
              ; isLimit = preserve Γ limita }
 
diff -r 04da2c458d44 -r c7b8017bcd4d freyd1.agda
--- a/freyd1.agda	Mon Mar 13 10:41:07 2017 +0900
+++ b/freyd1.agda	Mon Mar 13 13:22:40 2017 +0900
@@ -6,17 +6,13 @@
 
 open import cat-utility
 open import HomReasoning
-open import Relation.Binary.Core
 open Functor
 
 open import Comma1 F G
-open import freyd CommaCategory
-
-open import Category.Cat
+-- open import freyd CommaCategory  -- we don't need this yet
 
+open import Category.Cat  -- Functor composition
 open NTrans
-
-
 open Complete
 open CommaObj
 open CommaHom
@@ -60,7 +56,7 @@
     → ( Γ : Functor I CommaCategory ) 
     → ( glimit :  LimitPreserve A I  C G )
     → Limit C I (G  ○  (FIA Γ)) 
-LimitC  {I} comp Γ glimit  = plimit glimit (FIA Γ) (climit comp (FIA Γ))
+LimitC  {I} comp Γ glimit  = plimit glimit (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
@@ -158,6 +154,10 @@
       comm1 =  let  open ≈-Reasoning (C) in begin
             FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a 
          ≈⟨ {!!} ⟩
+            FMap G ((limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o ( {!!}  o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) 
+         ≈⟨ assoc ⟩
+             (FMap G ((limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o {!!} ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) 
+         ≈↑⟨ car (  limit-uniqueness  (isLimit  (LimitC comp Γ glimit  )) {!!} {!!} ) ⟩
             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))
@@ -172,7 +172,6 @@
              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)) 
@@ -184,7 +183,6 @@
              arrow f
          ∎
 
-
 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
     → ( glimit :   LimitPreserve A I C G )
     → ( Γ : Functor I CommaCategory )