# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1457189777 -32400
# Node ID b18585089d2e336ec990d30ed19305a8034995c1
# Parent  e9e14eec739146b39512a6d782c08565f1b382a6
add more parameter to nat in lim-to-equ

diff -r e9e14eec7391 -r b18585089d2e limit-to.agda
--- a/limit-to.agda	Sat Mar 05 16:08:32 2016 +0900
+++ b/limit-to.agda	Sat Mar 05 23:56:17 2016 +0900
@@ -88,36 +88,33 @@
          nmap x d h with (obj→  two x)
          ... | t0 = h
          ... | t1 = A [ f  o  h ]
-         commute : {x y : Obj Two}  {f : Hom Two x y} (d : Obj A) (h : Hom A d a ) -> TwoObject -> TwoObject 
-                 → A [ A [ FMap Γ f o nmap x d h ] ≈ A [ nmap y d h o FMap (K A Two d) f ] ]
-         commute  {x} {y} {f} d h t0 t0 =   let open ≈-Reasoning (A) in 
+         commute1 : {x y : Obj Two}  {f' : Hom Two x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] -> TwoObject -> TwoObject 
+                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A Two d) f' ] ]
+         commute1  {x} {y} {f'} d h fh=gh t0 t0 =   let open ≈-Reasoning (A) in 
               begin
-                  FMap Γ f o nmap x d h
+                  FMap Γ f' o nmap x d h
               ≈⟨ {!!} ⟩
-                  {!!}
-              ≈⟨⟩
                   nmap y d h 
               ≈↑⟨ idR ⟩
                   nmap y d h o id1 A d
               ≈⟨⟩
-                  nmap y d h o FMap (K A Two d) f 
+                  nmap y d h o FMap (K A Two d) f' 
               ∎
-         commute  {x} {y} {f} d h t0 t1 =   let open ≈-Reasoning (A) in 
+         commute1  {x} {y} {f'} d h fh=gh t0 t1 =   let open ≈-Reasoning (A) in 
               begin
-                  FMap Γ f o nmap x d h
-              ≈⟨⟩
-                  FMap Γ f o h
+                  FMap Γ f' o nmap x d h
               ≈⟨ {!!} ⟩
-                  nmap y d h o FMap (K A Two d) f 
+                  nmap y d h o FMap (K A Two d) f'
               ∎
-         commute  {x} {y} {f} d h t1 t0 =  {!!}
-         commute  {x} {y} {f} d h t1 t1 =  {!!}
-         nat : (d : Obj A) → (h : Hom A d a ) → NTrans Two A (K A Two d) Γ
-         nat d h = record {
+         commute1  {x} {y} {f'} d h fh=gh t1 t0 =  {!!}
+         commute1  {x} {y} {f'} d h fh=gh t1 t1 =  {!!}
+         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans Two A (K A Two d) Γ
+         nat d h fh=gh = record {
             TMap = λ x → nmap x d h ; 
             isNTrans = record {
-                commute = λ {x} {y} {f} -> commute d h (obj→ two x) (obj→ two y)
+                commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh (obj→ two x) (obj→ two y)
             }
           }
          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
-         k {d} h fh=gh  = limit (lim Two Γ  {c} {nat c e }) d (nat d h ) 
+         k {d} h fh=gh  = limit (lim Two Γ  {c} {nat c e fe=ge }) d (nat d h fh=gh )
+