Mercurial > hg > Members > kono > Proof > category

changeset 371:3a125d05ae0f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit-to nat will be done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Mar 2016 01:56:32 +0900
parents 93540deafde7
children b4855a3ebd34
files limit-to.agda
diffstat 1 files changed, 48 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 06 01:05:03 2016 +0900
+++ b/limit-to.agda	Sun Mar 06 01:56:32 2016 +0900
@@ -20,9 +20,13 @@
 ---                     f
 ---          e       ------>
 ---     c ------>  a         b
----     ^    . /     ------>
----     |k . h          g
----     d /  
+---     ^      /     ------>
+---     |k   h          g
+---     |   / 
+---     |  / 
+---     | /  
+---     |/  
+---     d  
 
 
 data TwoObject   : Set where
@@ -33,6 +37,9 @@
     field
          obj→ : Obj A  -> TwoObject 
          hom→ : {a b : Obj A} -> Hom A a b -> TwoObject
+         f-rev : Hom A b a
+         feq : A [ A [ f-rev o  f ] ≈  id1 A a ]
+         geq : A [ A [ f-rev o  g ] ≈  id1 A a ]
     fobj : Obj A -> Obj A
     fobj x with  obj→ x
     ... | t0 = a
@@ -44,9 +51,9 @@
 open TwoCat
 
 indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-        ( a b : Obj A ) ( f g : Hom A a b ) ( f-rev : Hom A b a ) -> (two : TwoCat A a b f g ) 
+        ( a b : Obj A ) ( f g : Hom A a b )  -> (two : TwoCat A a b f g ) 
             -> Functor A A
-indexFunctor A a b f g f-rev two = record {
+indexFunctor A a b f g two = record {
          FObj = λ a → fobj two a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
@@ -58,7 +65,7 @@
           fmap :  {x y : Obj A } -> Hom A x y -> Hom A (fobj two x) (fobj two y)
           fmap {x} {y} f' with obj→ two x | obj→ two y 
           ... | t0 | t0 = id1 A a
-          ... | t1 | t0 = f-rev
+          ... | t1 | t0 = f-rev two
           ... | t1 | t1 = id1 A b
           ... | t0 | t1  = fmap' two (hom→ two f')
 
@@ -66,48 +73,62 @@
 
 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
       (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
-        →  {a b c : Obj A}  (f-rev : Hom A b a ) (f g : Hom A  a b ) (two : TwoCat A a b f g ) 
+        →  {a b c : Obj A}   (f g : Hom A  a b ) (two : TwoCat A a b f g ) 
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ A lim {a} {b} {c} f-rev f g two e fe=ge = record {
+lim-to-equ A lim {a} {b} {c}  f g two e fe=ge = record {
         fe=ge =  fe=ge
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → {!!}
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
-         Γ = indexFunctor A a b f g f-rev two
+         Γ = indexFunctor A a b f g two
          nmap :  (x : Obj A) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A A d) x) (FObj Γ x)
          nmap x d h with (obj→  two x)
          ... | t0 = h
          ... | t1 = A [ fmap' two (obj→  two x) o  h ]
-         commute1 : {x y : Obj A}  {f' : Hom A x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] -> TwoObject -> TwoObject 
+         lemma1 :  {x y : Obj A}  {f' : Hom A x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ]
+                 →  A [ A [ fmap' two (hom→ two f') o h ] ≈ A [ fmap' two (obj→ two y)  o h ] ]
+         lemma1 {x} {y} {f'} d h fh=gh with  (hom→ two f') |  (obj→ two y)
+         ... | t0 | t0 = let open ≈-Reasoning (A) in refl-hom
+         ... | t0 | t1 = fh=gh
+         ... | t1 | t0 = let open ≈-Reasoning (A) in sym fh=gh
+         ... | t1 | t1 =  let open ≈-Reasoning (A) in refl-hom
+         commute1 : {x y : Obj A}  {f' : Hom A x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] 
                  → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A A d) f' ] ]
-         commute1  {x} {y} {f'} d h fh=gh t0 t0 =   let open ≈-Reasoning (A) in 
+         commute1  {x} {y} {f'} d h fh=gh with (obj→ two x) | (obj→ two y)
+         ... | t0 | t0 = let open ≈-Reasoning (A) in 
               begin
-                  FMap Γ f' o nmap x d h
+                  id1 A a  o h
+              ≈⟨ idL ⟩
+                  h 
+              ≈↑⟨ idR ⟩
+                  h o id1 A d
+              ∎ 
+         ... | t0 | t1 = let open ≈-Reasoning (A) in 
+              begin
+                fmap' two (hom→ two f')  o h
+              ≈⟨ lemma1 {x} {y} {f'} d h fh=gh ⟩
+                fmap' two (obj→  two y) o  h 
+              ≈↑⟨ idR ⟩
+                (fmap' two (obj→  two y) o  h )  o id1 A d
+              ∎ 
+         ... | t1 | t0 =   let open ≈-Reasoning (A) in
+              begin
+                 f-rev two  o ( fmap' two (obj→  two x) o  h )
               ≈⟨ {!!} ⟩
-                  nmap y d h 
-              ≈↑⟨ idR ⟩
-                  nmap y d h o id1 A d
-              ≈⟨⟩
-                  nmap y d h o FMap (K A A d) f' 
+                  h o id1 A d
               ∎
-         commute1  {x} {y} {f'} d h fh=gh t0 t1 =   let open ≈-Reasoning (A) in 
+         ... | t1 | t1 =   let open ≈-Reasoning (A) in
               begin
-                  FMap Γ f' o nmap x d h
+                 id1 A b  o ( fmap' two (obj→  two x) o  h )
               ≈⟨ {!!} ⟩
-                  nmap y d h 
-              ≈↑⟨ idR ⟩
-                  nmap y d h o id1 A d
-              ≈⟨⟩
-                  nmap y d h o FMap (K A A d) f'
+                 (fmap' two (obj→  two y) o  h ) o id1 A d
               ∎
-         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 A A (K A A d) Γ
          nat d h fh=gh = record {
             TMap = λ x → nmap x d h ; 
             isNTrans = record {
-                commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh (obj→ two x) (obj→ two y)
+                commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh 
             }
           }
          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c