# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489297694 -32400
# Node ID 56cf6581c5f6707a9253d666279e251efc4709b3
# Parent  da4486523f7353d9751d9bba234a48c835b798de
add some lemma but no use

diff -r da4486523f73 -r 56cf6581c5f6 freyd1.agda
--- a/freyd1.agda	Sat Mar 11 18:58:21 2017 +0900
+++ b/freyd1.agda	Sun Mar 12 14:48:14 2017 +0900
@@ -98,10 +98,6 @@
              ; ≈-cong = IsFunctor.≈-cong ( isFunctor Γ )
           }} where
 
-revF : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I A )  → Functor I CommaCategory 
-revF = {!!}
-
-
 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 = tb A I (FIA Γ) (obj c) ta G
@@ -120,6 +116,43 @@
     → Limit C I ( G  ○ (FIA (revΓ Γ) )) 
 revLimitC  {I} comp glimit Γ = glimit (FIA (revΓ Γ)) (isLimit comp (FIA (revΓ Γ )))
 
+
+a0F : ( I : Category c₁ c₂ ℓ ) →  (a1 : Obj A) → Functor I A 
+a0F  I a1 =  record {
+  FObj = λ x →  a1
+  ; FMap = λ {a} {b} f →  id1 A a1
+  ; isFunctor = record {
+             identity = let  open ≈-Reasoning (A) in refl-hom
+             ; distr =  let  open ≈-Reasoning (A) in ( sym idL )
+             ; ≈-cong = λ _ →  let  open ≈-Reasoning (A) in refl-hom
+          }} where
+
+t0F :  ( I : Category c₁ c₂ ℓ ) →  (a1 : Obj A ) 
+    → NTrans I A (K A I a1 ) (a0F I a1 )
+t0F  I a1  = record {
+     TMap = λ i → id1 A a1 
+     ; isNTrans = record { commute = λ {a b f} → commute {a} {b} {f} }
+  } where
+      commute : {a b : Obj I} {f : Hom I a b} → A [
+        A [ FMap (a0F I a1  ) f o id1 A a1 ] ≈
+        A [ id1 A a1 o FMap (K A I a1) f ] ]
+      commute {a} {b} {f} =   let  open ≈-Reasoning (A) in begin
+              FMap (a0F I a1 ) f o id1 A a1
+         ≈⟨ idR ⟩
+              FMap (a0F I a1  ) f 
+         ≈⟨⟩
+              id1 A a1
+         ≈⟨⟩
+              FMap (K A I a1) f 
+         ≈↑⟨ idL ⟩
+              id1 A a1 o FMap (K A I a1) f 
+         ∎
+
+hoge :  ( a : Obj A ) →   ( I : Category c₁ c₂ ℓ ) → (comp : Complete A I ) → ∀ { i : Obj I } →  
+     A [ A [ TMap ( limit-u comp (a0F I a)) i o  limit (isLimit comp (a0F I a)) a (t0F I a) ]  ≈ id1 A a ]
+hoge a I comp {i} = t0f=t (isLimit comp (a0F I a)) 
+
+
 commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  
      → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
      →  Obj CommaCategory
@@ -127,13 +160,20 @@
       obj = limit-c  comp (FIA Γ)
       ; hom = limitHom
    } where
+       frev : {i : Obj I } → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
+       frev {i} = TMap (t0 ( isLimit comp (FIA Γ)))  i
        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 {!!} ]
+              TMap  = λ i →  C [ hom ( FObj Γ i ) o  FMap F frev ]
             ; isNTrans = {!!}
           }
+       forward :  Hom C  (FObj G (limit-c comp (FIA Γ))) (a0 (LimitC comp glimit Γ))
+       forward = limit (LimitC comp glimit Γ) (FObj G (limit-c  comp (FIA Γ))) 
+            ( record { TMap = λ i →  C [ FMap G frev  o {!!} ]  ; isNTrans = {!!} } ) 
+       rev :  Hom C (a0 (LimitC comp glimit Γ)) (FObj G (limit-c comp (FIA Γ)))
+       rev = C [ FMap G {!!} o TMap (t0 (LimitC comp glimit Γ)) {!!} ]
        limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom = C [   {!!} o limit (revLimitC comp glimit Γ) (FObj F (limit-c  comp (FIA (revΓ Γ)))) tu ] 
+       limitHom = C [  rev o limit (LimitC comp glimit Γ) (FObj F (limit-c  comp (FIA Γ))) tu ] 
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )