Mercurial > hg > Members > kono > Proof > category

changeset 368:b18585089d2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add more parameter to nat in lim-to-equ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 05 Mar 2016 23:56:17 +0900
parents e9e14eec7391
children a8ac736d73ff
files limit-to.agda
diffstat 1 files changed, 15 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- 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 )
+