Mercurial > hg > Members > kono > Proof > category

changeset 367:e9e14eec7391

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit-to dead end... too complex TwoCat and Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 05 Mar 2016 16:08:32 +0900
parents e07b7578d2e7
children b18585089d2e
files limit-to.agda
diffstat 1 files changed, 39 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sat Mar 05 14:52:49 2016 +0900
+++ b/limit-to.agda	Sat Mar 05 16:08:32 2016 +0900
@@ -17,23 +17,12 @@
 ---     0         1
 ---       ------>
 ---          g
----          
----          
----          
----          f
----       ------>
----     a         b
----       ------>
----     ^    g
----     |    
----     |e     
----     |    
----     c    
----     ^    
----     |    
----     |k   
----     |    
----     d    
+---                     f
+---          e       ------>
+---     c ------>  a         b
+---     ^    . /     ------>
+---     |k . h          g
+---     d /  
 
 
 data TwoObject   : Set where
@@ -95,16 +84,40 @@
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
          Γ = indexFunctor A Two two a b f g f-rev
-         nmap :  (x : Obj Two) ( d : Obj A ) -> Hom A (FObj (K A Two d) x) (FObj Γ x)
-         nmap x d with (obj→  two x)
-         ... | t0 = ?
-         ... | t1 = {!!}
-         nat : (d : Obj A) → NTrans Two A (K A Two d) Γ
-         nat d = record {
-            TMap = λ x → nmap x d ; 
+         nmap :  (x : Obj Two) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A Two d) x) (FObj Γ x)
+         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 
+              begin
+                  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 
+              ∎
+         commute  {x} {y} {f} d h t0 t1 =   let open ≈-Reasoning (A) in 
+              begin
+                  FMap Γ f o nmap x d h
+              ≈⟨⟩
+                  FMap Γ f o h
+              ≈⟨ {!!} ⟩
+                  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 {
+            TMap = λ x → nmap x d h ; 
             isNTrans = record {
-                commute = {!!}
+                commute = λ {x} {y} {f} -> commute d h (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}) d (nat d) 
+         k {d} h fh=gh  = limit (lim Two Γ  {c} {nat c e }) d (nat d h )